cs.AIJul 15, 2026

EZSMT Version 3, Matured

Authors: Yuliya Lierler

Organizations: University of Nebraska Omaha, USA

Read PDF
Ask AI
Cite

Copy citation

DOINot available for this paper

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.

Explore similar work

CardsList
May 26, 2026cs.AI

2-ASP(Q) programs with weak constraints: Complexity and efficient implementation

ASP(Q) extends Answer Set Programming (ASP) with Quantifiers over answer sets. In this paper we focus on the class of ASP(Q) programs with two quantifiers and weak constraints, denoted as 2-ASP(Q)^w. 2-ASP(Q)^w is a practically relevant fragment of ASP(Q) that is expressive enough to capture optimization problems up to the class Delta_3^P. On the theoretical side, we provide a complete complexity characterization of the main computational tasks for 2-ASP(Q)^w programs, including tight completeness results and the analysis of nontrivial cases that have not been addressed in previous works. On the practical side, we introduce novel strategies for computing (optimal) quantified answer sets in the Casper system, that rely on a Counterexample-Guided Abstraction Refinement (CEGAR) technique tailored to ASP(Q). An experimental evaluation on hard benchmarks from different application domains shows that the proposed techniques are effective in practice.
Andrea Cuteri, Giuseppe Mazzotta, Francesco Ricca
Answer Set ProgrammingStructural ConstraintsQuantum Approximate Optimization AlgorithmCounterexample
AskPDF
Sep 1, 2020cs.AI

PyCSP3: Modeling Combinatorial Constrained Problems in Python

In this document, we introduce PyCSP33, a Python library that allows us to write models of combinatorial constrained problems in a declarative manner. Currently, with PyCSP33, you can write models of constraint satisfaction and optimization problems. More specifically, you can build CSP (Constraint Satisfaction Problem) and COP (Constraint Optimization Problem) models. Importantly, there is a complete separation between the modeling and solving phases: you write a model, you compile it (while providing some data) in order to generate an XCSP33 instance (file), and you solve that problem instance by means of a constraint solver. You can also directly pilot the solving procedure in PyCSP33, possibly conducting an incremental solving strategy. In this document, you will find all that you need to know about PyCSP33, with more than 50 illustrative models.
Christophe Lecoutre, Nicolas Szczepanski
Constraint Satisfaction
AskPDF
Apr 21, 2026cs.LO

Streamliners for Answer Set Programming

Streamliner constraints reduce the search space of combinatorial problems by ruling out portions of the solution space. We adapt the StreamLLM approach, which uses Large Language Models (LLMs) to generate streamliners for Constraint Programming, to Answer Set Programming (ASP). Given an ASP encoding and a few small training instances, we prompt multiple LLMs to propose candidate constraints. Candidates that cause syntax errors, render satisfiable instances unsatisfiable, or degrade performance on all training instances are discarded. The surviving streamliners are evaluated together with the original encoding, and we report results for a virtual best encoding (VBE) that, for each instance, selects the fastest among the original encoding and its streamlined variants. On three ASP Competition benchmarks (Partner Units Problem, Sokoban, Towers of Hanoi), the VBE achieves speedups of up to 4--5x over the original encoding. Different LLMs produce semantically diverse constraints, not mere syntactic variations, indicating that the approach captures genuine problem structure.
Florentina Voboril, Martin Gebser, Stefan Szeider +1
Answer Set ProgrammingStructural ConstraintsHarbor Environments
AskPDF