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, Z3, and Yices. EZSMT used EZCSP, Gringo, and CMODELS to perform its transformation procedures.
EZSMT version 2.0.0 is available for download here (under GPLv3):
README file is present within the download content. In copmairson to its earlier version, EZSMT version 2.0.0 is able to process non-tight programs, enumerate multiple solutions, process programs with linear and nonlinear constraints over mixed real and integer variables (Note that it is compatible with Gringo version 4.5.3).
EZSMT version 2.0.0 is also available as a zip file packaged in a containerized environment called Docker. An advantage of this package is that all of the dependencies can be set up with one command line. Additionally, Docker facilitates stronger limits on cpu and memory consumption for benchmarking purposes. The package, including a README file, is available here:
Theoretical and practical groundings for EZSMT version 2.0.0 can be found in:
- Da Shen and Yuliya Lierler. SMT-based Constraint Answer Set Solver EZSMT+ for Non-tight Programs (PDF). 16th International Conference on Principles of Knowledge Representation and Reasoning (KR), 2018. Benchmarks discussed in this paper are posted here. Complete table presenting results on all experimental analyses discussed in the paper is posted here.
- Da Shen and Yuliya Lierler. SMT-based Answer Set Solver CMODELS-DIFF (System Description) (PDF). 34th International Conference on Logic Programming (ICLP), 2018.
Earlier version of the system EZSMT version 1.0.0 is available for download here (under GPLv3):
Theoretical and practical groundings for EZSMT version 1.0.0 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.