Track papers across labs, topics, and trends.
Search papers, labs, and topics across Lattice.
This paper introduces EZSMTV3, an advanced framework for Constraint Answer Set Programming (CASP) that enhances the translational approach to CASP solving by integrating a more expressive input language and supporting optimization through weak constraints. By utilizing state-of-the-art SMT solvers like CVC5, YICES, and Z3, EZSMTV3 efficiently tackles complex combinatorial search problems without the need for custom search procedures. Benchmarking results demonstrate EZSMTV3's superior performance in handling mixed-domain constraints compared to existing CASP systems, positioning it as a robust platform for future research and development in the field.
EZSMTV3 outperforms traditional CASP systems by leveraging advanced SMT solvers, enabling more expressive problem formulations and efficient optimization.
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.