EZSMT Version 3, Matured
06:00 · July 16, 2026 · arXiv cs.AI RSS
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.
Summary
EZSMT version 3 is an extensible framework for constraint answer set programming that follows a translational approach. It converts CASP programs into formulas in the language of satisfiability modulo theories and delegates the actual reasoning to off-the-shelf SMT solvers such as CVC5, Yices and Z3 rather than implementing its own search procedures.
The system extends its predecessor, EZSMT+, with a more expressive input language that permits constraint atoms in both heads and bodies of rules. It also adds support for optimization through weak constraints, a capability absent from the earlier version. The architecture separates grounding, translation to SMT-LIB, and solving into distinct pipeline stages, making it straightforward to incorporate new constraint types without altering the core search mechanism.
Benchmarking shows that EZSMTV3 performs competitively with established CASP systems such as Clingcon, Clingo[DL] and Clingo[LP]. In addition, the framework can reason over mixed-domain constraints that combine integer and real variables, a feature not offered by the compared solvers. The design is presented as a stable platform for further language extensions and theoretical study in the CASP area.
Why it matters
This primary research is highly relevant for AI researchers in the Netherlands focusing on symbolic AI, automated reasoning, and formal methods. EZSMTV3 provides a transparent, logic-based approach to solving complex combinatorial problems, aligning well with the European push for explainable and verifiable AI systems.
