# EZSMT Version 3, Matured

arXiv: https://arxiv.org/abs/2607.13344 · HTML: https://mlsanity.com/paper/2607.13344/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 11 of its 49 references that are in the map.
- First posted on arXiv 15 Jul 2026.

## Builds on (most cited first, 11 of 11)

- [Multi-shot ASP solving with clingo](https://mlsanity.com/paper/1705.09811/) (2017)
- [ASP-Core-2 Input Language Format](https://mlsanity.com/paper/1911.04326/) (2019)
- [How to build your own ASP-based system?!](https://mlsanity.com/paper/2008.06692/) (2020)
- [Clingo goes Linear Constraints over Reals and Integers](https://mlsanity.com/paper/1707.04053/) (2017)
- [Clingcon: The Next Generation](https://mlsanity.com/paper/1705.04569/) (2017)
- [Predicate Logic as a Modelling Language: The IDP System](https://mlsanity.com/paper/1401.6312/) (2014)
- [Constraint Answer Set Programming: Integrational and Translational (or SMT-based) Approaches](https://mlsanity.com/paper/2107.08252/) (2021)
- [SMT-based Constraint Answer Set Solver EZSMT+](https://mlsanity.com/paper/1905.03334/) (2019)
- [On Relation between Constraint Answer Set Programming and Satisfiability Modulo Theories](https://mlsanity.com/paper/1702.07461/) (2017)
- [An Abstract View on Optimizations in Propositional Frameworks](https://mlsanity.com/paper/2206.06440/) (2022)
- [Unifying Framework for Optimizations in non-boolean Formalisms](https://mlsanity.com/paper/2206.07862/) (2022)

## Abstract (arXiv)

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.