EZSMT Version 3, Matured

Researchers released EZSMTV3, an extensible SMT-based Constraint Answer Set Programming framework that advances the translational approach to CASP solving by leveraging state-of-the-art SMT solvers like CVC5, YICES, and Z3. The system introduces a more expressive input language, supports optimization via weak constraints, and demonstrates competitive performance against peers such as CLINGCON, CLINGO[DL], and CLINGO[LP] in handling mixed-domain constraints.

arXiv:2607.13344v1 Announce Type: new Abstract: 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.