EZSMT Version 3, Matured

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

, an extensible SMT-based CASP framework that advances the translational approach to CASP solving. Building upon the foundation of the system, 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, leverages state-of-the-art SMT solvers, such as , , and to perform reasoning. The paper provides benchmarking results comparing with its CASP peers such as , , and , 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.