
## References

BEAME, P., KAUTZ, H., AND SABHARWAL, A. 2004. Towards understanding and harnessing the potential of clause learning. Journal of Artificial Intelligence Research 22, 319–351.

CLARK, K. 1978. Negation as failure. In Logic and Data Bases, H. Gallaire and J. Minker, Eds.

Plenum Press, New York, 293–322.

COOK, S. A., ROBERT, AND RECKHOW, A. 1979. The relative efficiency of propositional proof systems. Journal of Symbolic Logic 44, 36–50.

DAVIS, M., LOGEMANN, G., AND LOVELAND, D. 1962. A machine program for theorem proving.

Communications of the ACM 5(7), 394–397.

DENECKER, M. 2000. Extending classical logic with inductive definitions. In Proceedings of the 1st International Conference on Computational Logic, CL 2000. Lecture Notes in Computer Science, vol. 1861. Springer, Berlin, 703–717.

EITER, T., LEONE, N., MATEIS, C., PFEIFER, G., AND SCARCELLO, F. 1997. A deductive system for non-monotonic reasoning. In Proceedings of the 4th International Conference on Logic Programming and Nonmonotonic Reasoning, LPNMR 1997. Lecture Notes in Computer Science, vol. 1265. Springer, Berlin, 363–374.

FERRARIS, P. AND LIFSCHITZ, V. 2005. Weight constraints as nested expressions. Theory and Practice of Logic Programming 5, 45–74.

GEBSER, M., KAUFMANN, B., NEUMANN, A., AND SCHAUB, T. 2007. Conflict-driven answer set solving. In Proceedings of 20th International Joint Conference on Artificial Intelligence, IJCAI
2007. 386–392.

GEBSER, M. AND SCHAUB, T. 2006. Tableau calculi for answer set programming. In Proceedings of the 22nd International Conference on Logic Programming, ICLP 2006. Lecture Notes in Computer Science, vol. 4079. Springer, Berlin, 11–25.

GELFOND, M. AND LIFSCHITZ, V. 1988. The stable model semantics for logic programming. In Proceedings of the 5th International Logic Programming Conference and Symposium, R. Kowalski and K. Bowen, Eds. MIT Press, Cambridge, MA, 1070–1080.

GIUNCHIGLIA, E., LEONE, N., AND MARATEA, M. 2008. On the relation among answer set solvers. Annals of Mathematics and Artificial Intelligence 53, 1-4, 169–204.

GIUNCHIGLIA, E., LIERLER, Y., AND MARATEA, M. 2004. SAT-based answer set programming.

In Proceedings of the 19th National Conference on Artificial Intelligence, AAAI 2004. AAAI
Press, Menlo Park, CA, 61–66.

GIUNCHIGLIA, E. AND MARATEA, M. 2005. On the relation between answer set and SAT procedures (or, between smodels and cmodels). In Proceedings of the 21st International Conference on Logic Programming, ICLP 2005. Lecture Notes in Computer Science, vol. 3668. Springer, Berlin, 37–51.

LEE, J. 2005. A model-theoretic counterpart of loop formulas. In Proceedings of the 19th International Joint Conference on Artificial Intelligence, IJCAI 2005. Professional Book Center, 503–508.

LEONE, N., RULLO, P., AND SCARCELLO, F. 1997. Disjunctive stable models: Unfounded sets, fixpoint semantics, and computation. Information and Computation 135(2), 69–112.

LIERLER, Y. 2010. Sat-based answer set programming. Ph.D. thesis, University of Texas at Austin.

LIERLER, Y. 2011. Abstract answer set solvers with backjumping and learning. Theory and Practice of Logic Programming 11, 135–169.

LIFSCHITZ, V., TANG, L. R., AND TURNER, H. 1999. Nested expressions in logic programs. Annals of Mathematics and Artificial Intelligence 25, 369–389.

LIN, F. AND ZHAO, Y. 2004. ASSAT: Computing answer sets of a logic program by SAT solvers.

Artificial Intelligence 157, 115–137.

MAREK, V. AND TRUSZCZYNSKI ´ , M. 1999. Stable models and an alternative logic programming