SMT-Based Answer Set Solver CMODELS(DIFF) (System Description)
Many answer set solvers utilize Satisfiability solvers for search. Satisfiability Modulo Theory solvers extend Satisfiability solvers. This paper presents the CMODELS(DIFF) system that uses Satisfiability Modulo Theory solvers to find answer sets of a logic program. Its theoretical foundation is based on Niemala's characterization of answer sets of a logic program via so called level rankings. The comparative experimental analysis demonstrates that CMODELS(DIFF) is a viable answer set solver.
answer set programming
satisfiability modulo theories
constraint satisfaction processing
Computing methodologies~Logic programming and answer set programming
Software and its engineering~Constraint and logic languages
Theory of computation~Constraint and logic programming
11:1-11:15
System Description
Da
Shen
Da Shen
Department of Computer Science, University of Nebraska at Omaha, South 67th Street, Omaha, NE 68182, USA
Yuliya
Lierler
Yuliya Lierler
Department of Computer Science, University of Nebraska at Omaha, South 67th Street, Omaha, NE 68182, USA
https://orcid.org/0000-0002-6146-623X
10.4230/OASIcs.ICLP.2018.11
Clark Barrett, Pascal Fontaine, and Cesare Tinelli. The SMT-LIB Standard: Version 2.5. Technical report, Department of Computer Science, The University of Iowa, 2015.
Clark Barrett and Cesare Tinelli. Satisfiability Modulo Theories. In Edmund Clarke, Tom Henzinger, and Helmut Veith, editors, Handbook of Model Checking. Springer, 2014.
Keith Clark. Negation as failure. In Herve Gallaire and Jack Minker, editors, Logic and Data Bases, pages 293-322. Plenum Press, New York, 1978.
Esra Erdem and Vladimir Lifschitz. Fages' theorem for programs with nested expressions. In Proceedings of International Conference on Logic Programming (ICLP), pages 242-254, 2001.
François Fages. Consistency of Clark’s completion and existence of stable models. Journal of Methods of Logic in Computer Science, 1:51-60, 1994.
Paolo Ferraris and Vladimir Lifschitz. Weight constraints as nested expressions. Theory and Practice of Logic Programming, 5:45-74, 2005.
Martin Gebser, Roland Kaminski, Benjamin Kaufmann, Javier Romero, and Torsten Schaub. Progress in clasp Series 3. In Proceedings of the Thirteenth International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR'15), 2015.
Martin Gebser, Benjamin Kaufmann, André Neumann, and Torsten Schaub. Conflict-driven Answer Set Enumeration. In Proceedings of the 9th International Conference on Logic Programming and Nonmonotonic Reasoning, LPNMR'07, pages 136-148, Berlin, Heidelberg, 2007. Springer-Verlag. URL: http://dl.acm.org/citation.cfm?id=1758481.1758496.
http://dl.acm.org/citation.cfm?id=1758481.1758496
Carla P. Gomes, Henry Kautz, Ashish Sabharwal, and Bart Selman. Satisfiability Solvers. In Frank van Harmelen, Vladimir Lifschitz, and Bruce Porter, editors, Handbook of Knowledge Representation, pages 89-134. Elsevier, 2008.
Tomi Janhunen, Ilkka Niemelä, and Mark Sevalnev. Computing Stable Models via Reductions to Difference Logic. In Logic Programming and Nonmonotonic Reasoning, pages 142-154. Springer Berlin Heidelberg, 2009.
Yuliya Lierler. SAT-based Answer Set Programming. PhD thesis, University of Texas at Austin, 2010.
Yuliya Lierler. What is answer set programming to propositional satisfiability. Constraints, pages 1-31, 2016. URL: http://dx.doi.org/10.1007/s10601-016-9257-7.
http://dx.doi.org/10.1007/s10601-016-9257-7
Yuliya Lierler and Benjamin Susman. On relation between constraint answer set programming and satisfiability modulo theories. Theory and Practice of Logic Programming, 17(4):559-590, 2017.
Yuliya Lierler and Miroslaw Truszczyński. Transition Systems for Model Generators - A Unifying Approach. Theory and Practice of Logic Programming, 27th Int'l. Conference on Logic Programming (ICLP) Special Issue, 11(4-5):629-646, 2011.
Vladimir Lifschitz, Lappoon R. Tang, and Hudson Turner. Nested expressions in logic programs. Annals of Mathematics and Artificial Intelligence, 25:369-389, 1999.
Fangzhen Lin and Yuting Zhao. ASSAT: Computing answer sets of a logic program by SAT solvers. Artificial Intelligence, 157:115-137, 2004.
Kim Marriott and Peter J. Stuckey. Programming with Constraints: An Introduction. MIT Press, 1998.
N. Nethercote, P.J. Stuckey, R. Becket, S. Brand, G.J. Duck, , and G. Tack. MiniZinc: Towards a standard CP modelling language. In Proceedings of the 13th International Conference on Principles and Practice of Constraint Programming, page 529–543, 2007.
Ilkka Niemela. Stable models and difference logic. Annals of Mathematics and Artificial Intelligence, 53:313-329, 2008.
Ilkka Niemelä and Patrik Simons. Extending the Smodels System with Cardinality and Weight Constraints. In Jack Minker, editor, Logic-Based Artificial Intelligence, pages 491-521. Kluwer, 2000.
Benjamin Susman and Yuliya Lierler. SMT-Based Constraint Answer Set Solver EZSMT (System Description). In Technical Communications of the 32nd International Conference on Logic Programming (ICLP 2016), volume 52, pages 1:1-1:15, 2016.
Da Shen and Yuliya Lierler
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode