Document Open Access Logo

SMT-Based Answer Set Solver CMODELS(DIFF) (System Description)

Authors Da Shen, Yuliya Lierler

PDF

File

Thumbnail PDF
PDF
OASIcs.ICLP.2018.11.pdf
  • Filesize: 0.85 MB
  • 15 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Computing methodologies → Logic programming and answer set programming
  • Software and its engineering → Constraint and logic languages
  • Theory of computation → Constraint and logic programming
Keywords
  • answer set programming
  • satisfiability modulo theories
  • constraint satisfaction processing

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

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.

Cite As Get BibTex

Da Shen and Yuliya Lierler. SMT-Based Answer Set Solver CMODELS(DIFF) (System Description). In Technical Communications of the 34th International Conference on Logic Programming (ICLP 2018). Open Access Series in Informatics (OASIcs), Volume 64, pp. 11:1-11:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018) https://doi.org/10.4230/OASIcs.ICLP.2018.11

Author Details

Da Shen
  • Department of Computer Science, University of Nebraska at Omaha, South 67th Street, Omaha, NE 68182, USA
Yuliya Lierler
  • Department of Computer Science, University of Nebraska at Omaha, South 67th Street, Omaha, NE 68182, USA

References

  1. 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. Google Scholar
  2. Clark Barrett and Cesare Tinelli. Satisfiability Modulo Theories. In Edmund Clarke, Tom Henzinger, and Helmut Veith, editors, Handbook of Model Checking. Springer, 2014. Google Scholar
  3. Keith Clark. Negation as failure. In Herve Gallaire and Jack Minker, editors, Logic and Data Bases, pages 293-322. Plenum Press, New York, 1978. Google Scholar
  4. 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. Google Scholar
  5. 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. Google Scholar
  6. Paolo Ferraris and Vladimir Lifschitz. Weight constraints as nested expressions. Theory and Practice of Logic Programming, 5:45-74, 2005. Google Scholar
  7. 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. Google Scholar
  8. 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.
  9. 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. Google Scholar
  10. 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. Google Scholar
  11. Yuliya Lierler. SAT-based Answer Set Programming. PhD thesis, University of Texas at Austin, 2010. Google Scholar
  12. 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.
  13. 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. Google Scholar
  14. 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. Google Scholar
  15. Vladimir Lifschitz, Lappoon R. Tang, and Hudson Turner. Nested expressions in logic programs. Annals of Mathematics and Artificial Intelligence, 25:369-389, 1999. Google Scholar
  16. Fangzhen Lin and Yuting Zhao. ASSAT: Computing answer sets of a logic program by SAT solvers. Artificial Intelligence, 157:115-137, 2004. Google Scholar
  17. Kim Marriott and Peter J. Stuckey. Programming with Constraints: An Introduction. MIT Press, 1998. Google Scholar
  18. 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. Google Scholar
  19. Ilkka Niemela. Stable models and difference logic. Annals of Mathematics and Artificial Intelligence, 53:313-329, 2008. Google Scholar
  20. 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. Google Scholar
  21. 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. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact