2026-07-22T01:29:22Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:9877 2024-03-06T10:30:23Z ddc:004 open_access

SMT-Based Answer Set Solver CMODELS(DIFF) (System Description) Shen, Da Lierler, Yuliya answer set programming satisfiability modulo theories constraint satisfaction processing 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Da Shen and Yuliya Lierler 2018 Is Part Of OASIcs, Volume 64, Technical Communications of the 34th International Conference on Logic Programming (ICLP 2018) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/OASIcs.ICLP.2018.11 urn:nbn:de:0030-drops-98775 https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.ICLP.2018.11 eng https://creativecommons.org/licenses/by/3.0/legalcode