CMODELS(DIFF) is an answer set programming solver which takes an answer set program processed by Lparse or Gringo and produces an SMT-LIB compliant program. The resultant program is solved using a Satisfiability Modulo Theories solver such as CVC4, Z3, Yices.
CMODELS(DIFF) version 1.0.0 is available for download here (under GPLv3):
Theoretical and practical groundings for this work can be found in:
- Da Shen and Yuliya Lierler. SMT-based Answer Set Solver CMODELS(DIFF) (System Description). The 34th International Conference on Logic Programming (ICLP), 2018; Benchmarks discussed in this paper are posted here.
Our Campus. Otherwise Known as Omaha.
The University of Nebraska does not discriminate based on race, color, ethnicity, national origin, sex, pregnancy, sexual orientation, gender identity, religion, disability, age, genetic information, veteran status, marital status, and/or political affiliation in its programs, activities, or employment. Learn more about Equity, Access and Diversity.