EZSMT is a constraint answer set programming solver which takes a program written in EZCSP and produces an SMT-LIB compliant program. The resultant program can be run on Satisfiability Modulo Theories solvers such as CVC4 and Z3. EZSMT used EZCSP, Gringo, and CMODELS to perform its transformation procedure.
EZSMT version 1.0.0 is available for download here (under GPLv3):
Theoretical and practical groundings for this work can be found in:
- Benjamin Susman and Yuliya Lierler. System Description: SMT-based Constraint Answer Set Solver EZSMT (PDF). 32nd International Conference on Logic Programming (ICLP), 2016.
- Yuliya Lierler and Benjamin Susman. Constraint Answer Set Programming versus Satisfiability Modulo Theories (PDF). 25th International Joint Conference on Artificial Intelligence (IJCAI) , 2016.
- Benjamin Susman. The EZSMT Solver: Constraint Answer Set Solving meets SMT (PDF). Master Thesis, University of Nebraska Omaha, 2016.
- Yuliya Lierler and Benjamin Susman. Constraint Answer Set Programming versus Satisfiability Modulo Theories Or Constraints versus Theories (PDF). 3rd Workshop on Grounding, Transforming, and Modularizing Theories with Variables (GTTV 2015), 2015.
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.