![](https://d3ilqtpdwi981i.cloudfront.net/MzAUFi45lmz3M7SK9TCtmUMA_is=/425x550/smart/https://bepress-attached-resources.s3.amazonaws.com/uploads/90/02/80/900280e0-e57d-4dcf-b93a-4b2461d5a3bb/thumbnail_24d0d252-5b2b-471f-9336-1dfc0638ff3f.jpg)
Article
SMT-based Answer Set Solver CMODELS-DIFF (System Description)
34th International Conference on Logic Programming
(2018)
Abstract
Many answer set solvers utilize Satisfiability solvers for search. SMT solvers extend Satisfiability solvers. This paper presents the CMODELS-DIFF system that uses SMT 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.
Disciplines
Publication Date
July, 2018
Citation Information
Da Shen and Yuliya Lierler. "SMT-based Answer Set Solver CMODELS-DIFF (System Description)" 34th International Conference on Logic Programming (2018) Available at: http://works.bepress.com/yuliya_lierler/79/