EZSMT Version 3, Matured
For researchers in answer set programming and constraint solving, EZSMTV3 offers a flexible, extensible platform for CASP, but its improvements are incremental over the previous EZSMT+ system.
EZSMTV3 is an extensible SMT-based CASP framework that improves upon its predecessor with a more expressive input language, support for optimization via weak constraints, and easier integration of new constraint types. Benchmarking shows it competes with systems like CLINGCON and CLINGO[DL] while handling mixed-domain constraints.
Constraint Answer Set Programming (CASP) is a hybrid reasoning paradigm that combines Answer Set Programming (ASP) with Constraint Processing and Satisfiability Modulo Theories (SMT), enabling powerful declarative encodings of complex combinatorial search problems. This paper presents the design and implementation of EZSMTV3, an extensible SMT-based CASP framework that advances the translational approach to CASP solving. Building upon the foundation of the EZSMT+ system, EZSMTV3 introduces a more expressive input language, supports optimization via weak constraints, and offers foundations for streamlined integration of new constraint types. Rather than implementing custom search procedures, EZSMTV3 leverages state-of-the-art SMT solvers, such as CVC5, YICES, and Z3 to perform reasoning. The paper provides benchmarking results comparing EZSMTV3 with its CASP peers such as CLINGCON, CLINGO[DL], and CLINGO[LP], while showcasing its ability to handle mixed-domain constraints involving both integers and reals. The system provides a robust platform for future extensions and theoretical exploration within the CASP domain.