EZSMT Version 3, Matured

# EZSMT Version 3, Matured 1footnote 11footnote 1
Source: [https://arxiv.org/html/2607.13344](https://arxiv.org/html/2607.13344)
## EZSMT Version 3, Matured11footnotemark:1

###### 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 ofezsmtv3, an extensible SMT\-based CASP framework that advances the translational approach to CASP solving\. Building upon the foundation of theezsmt\+system,ezsmtv3introduces 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,ezsmtv3leverages state\-of\-the\-art SMT solvers, such ascvc5,yices, andz3to perform reasoning\. The paper provides benchmarking results comparingezsmtv3with its CASP peers such asclingcon,clingo\[DL\], andclingo\[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\. Under consideration in Theory and Practice of Logic Programming \(TPLP\)\.

###### keywords:

Constraint Answer Set Programming Satisfiability Modulo Theories

## 1Introduction

Constraint answer set programming \(CASP\) is a hybrid methodology in automated reasoning that integrates advancements from several research domains, namely answer set programming \([Niemelä](https://arxiv.org/html/2607.13344#bib.bib3),[1999](https://arxiv.org/html/2607.13344#bib.bib3);[Marek and Truszczyński](https://arxiv.org/html/2607.13344#bib.bib2),[1999](https://arxiv.org/html/2607.13344#bib.bib2);[Brewkaet al\.](https://arxiv.org/html/2607.13344#bib.bib1),[2011](https://arxiv.org/html/2607.13344#bib.bib1)\), constraint processing \([Rossiet al\.](https://arxiv.org/html/2607.13344#bib.bib68),[2008](https://arxiv.org/html/2607.13344#bib.bib68);[Jaffar and Maher](https://arxiv.org/html/2607.13344#bib.bib57),[1994](https://arxiv.org/html/2607.13344#bib.bib57)\), and satisfiability modulo theories \([Nieuwenhuiset al\.](https://arxiv.org/html/2607.13344#bib.bib91),[2006](https://arxiv.org/html/2607.13344#bib.bib91);[Barrettet al\.](https://arxiv.org/html/2607.13344#bib.bib67),[2008](https://arxiv.org/html/2607.13344#bib.bib67);[Barrett and Tinelli](https://arxiv.org/html/2607.13344#bib.bib40),[2014](https://arxiv.org/html/2607.13344#bib.bib40)\)\. Works by \([Elkabaniet al\.](https://arxiv.org/html/2607.13344#bib.bib480),[2004](https://arxiv.org/html/2607.13344#bib.bib480);[Mellarkodet al\.](https://arxiv.org/html/2607.13344#bib.bib1031),[2008](https://arxiv.org/html/2607.13344#bib.bib1031);[Lierler](https://arxiv.org/html/2607.13344#bib.bib71),[2014](https://arxiv.org/html/2607.13344#bib.bib71)\) are among earlier references to CASP\. It has shown significant potential, leading to the creation of numerous solvers such asacsolver\[Mellarkodet al\.,[2008](https://arxiv.org/html/2607.13344#bib.bib1031)\],clingcon\[Gebseret al\.,[2009b](https://arxiv.org/html/2607.13344#bib.bib74)\],ezcsp\[Balduccini and Lierler,[2017](https://arxiv.org/html/2607.13344#bib.bib27)\],idp\[Wittocxet al\.,[2008](https://arxiv.org/html/2607.13344#bib.bib1318)\],inca\[Drescher and Walsh,[2010](https://arxiv.org/html/2607.13344#bib.bib12)\],dingo\[Janhunenet al\.,[2011](https://arxiv.org/html/2607.13344#bib.bib60)\],mingo\[Liuet al\.,[2012](https://arxiv.org/html/2607.13344#bib.bib103)\],aspmt\[Bartholomew and Lee,[2014](https://arxiv.org/html/2607.13344#bib.bib363)\],clingo\[LP\]andclingo\[DL\]\[Janhunenet al\.,[2017](https://arxiv.org/html/2607.13344#bib.bib7)\], andezsmt\+\([Susman and Lierler](https://arxiv.org/html/2607.13344#bib.bib109),[2016a](https://arxiv.org/html/2607.13344#bib.bib109);[Shen and Lierler](https://arxiv.org/html/2607.13344#bib.bib137),[2018b](https://arxiv.org/html/2607.13344#bib.bib137)\)\. CASP opens up new possibilities for declarative programming, enabling it to tackle such complex tasks as train scheduling and product configurations\. Solvers for CASP can be broadly categorized based on their construction strategy into integrational and translational approaches\. This paper describes not just a solver that practices translational approach but an extensible CASP framework that is geared to ease the implementation of new systems in this field\.

This paper presents the design, development, and implementation of an extensible SMT\-based constraint answer set programming frameworkezsmtversion 3 \(ezsmtv3\)\. We build upon the initial vision outlined in our earlier work on theezsmt\+system \([Susman and Lierler](https://arxiv.org/html/2607.13344#bib.bib109),[2016a](https://arxiv.org/html/2607.13344#bib.bib109);[Shen and Lierler](https://arxiv.org/html/2607.13344#bib.bib137),[2018b](https://arxiv.org/html/2607.13344#bib.bib137)\)\. In particular, we continue championing the practice of so called translational approaches within the automated reasoning realm\. The work onezsmtv3turns preliminary ideas behind the CASPezsmt\+solver into mature extensible framework for CASP\. With that, not onlyezsmtv3is the solver itself, it is also designed to support extensions of this system to new kinds of constraints in a simple, streamlined manner\. In a nutshell, theezsmtv3system computes answer sets to constraint answer set \(CAS\) programs providing support for various kinds of constraints\. Yet, while doing so it does not implement native search procedures\. Instead, it translates a given logic program with constraint atoms into a formula within some dialect of satisfiability modulo theories \(SMT\)\. This formula is then processed by one of the off\-the\-shelf SMT solvers\. Historically, theezsmt\+language adopted the conventions of the CASP language developed for theezscpsystem\[Balduccini and Lierler,[2017](https://arxiv.org/html/2607.13344#bib.bib27)\]\. Thus, its constraint atoms \(marked by the keywordrequired\) were restricted to rule heads, making certain domains cumbersome to formalize\. While sufficient for bootstrapping a proof\-of\-concept system,ezcsp’s language features revealed the need for a more expressive and flexible alternative\.

In our work onezsmtv3, we found such an alternative\. In particular, it builds upon the developments in theclingo5 series \([Gebseret al\.](https://arxiv.org/html/2607.13344#bib.bib6),[2019](https://arxiv.org/html/2607.13344#bib.bib6);[Kaminskiet al\.](https://arxiv.org/html/2607.13344#bib.bib136),[2023](https://arxiv.org/html/2607.13344#bib.bib136)\) that promotes the extensibility philosophy\. Theclingo 5system provides means to elaborate the specifications for new kinds of constructs to be incorporated for processing within its grounding toolgringo\([Gebseret al\.](https://arxiv.org/html/2607.13344#bib.bib1288),[2009a](https://arxiv.org/html/2607.13344#bib.bib1288);[Gebser,Martinet al\.](https://arxiv.org/html/2607.13344#bib.bib119),[2015](https://arxiv.org/html/2607.13344#bib.bib119);[Kaminski](https://arxiv.org/html/2607.13344#bib.bib996),[2023](https://arxiv.org/html/2607.13344#bib.bib996)\)\. In addition,clingo 5provides means to incorporate custom propagators to ensure proper processing of newly incorporated syntactic language features\. In this work, we embrace the extensibility philosophy ofclingo 5\. Yet, we diverged from its provisions for the custom implementations of the search mechanisms\. We advocate the utilization of already existing state\-of\-the\-art automated reasoning tools, specifically, SMT solvers\. Thus, this work relies on a body of theoretical findings relating CASP and SMT as well as a body of sophisticated algorithmic developments within SMT solving resulting in such exemplary systems ascvc4\[Barrettet al\.,[2011](https://arxiv.org/html/2607.13344#bib.bib132)\],cvc5\[Barrettet al\.,[2021](https://arxiv.org/html/2607.13344#bib.bib133)\],z3\[De Moura and Bjørner,[2008](https://arxiv.org/html/2607.13344#bib.bib134)\], andyices\[Dutertre and De Moura,[2006](https://arxiv.org/html/2607.13344#bib.bib135)\]\. Instead, we focused on creating a streamlined interface to SMT technologies\. Our approach relies on an easily extensible component\-based architecture consisting of a grounding component, a translation component, and an SMT\-based solving component\. The system is designed as a multi\-stage processing pipeline, with the output of each component serving as the input for the next\. The grounding component is utilized in such a way that the system allows us to extend the existing language specifications\. The output of the grounding component is interpreted by the translation component to support translations from ASP to SMT—paving the way for future CASP dialects to be seamlessly integrated\. The SMT\-based solving component uses the translated SMT\-LIB program to return the answer sets of the original ASP program\. In addition,ezsmtv3implements support for optimization statements, namely, weak constraints\. This feature is new toezsmtv3and was missing from the CASPezsmt\+solver\.

Section[2](https://arxiv.org/html/2607.13344#S2)of this paper provides a review of key concepts in constraint answer set programming\. Section[3](https://arxiv.org/html/2607.13344#S3)starts by detailing the CASP dialects supported byezsmtv3by utilizing a formalization of a variant of the Traveling Salesman problem as our running example\. It concludes with the presentation on the architecture of theezsmtv3system and the discussion of its implementation\. Given that optimization statements are new toezsmtv3in relation to its older “sibling”ezsmt\+, Section[4](https://arxiv.org/html/2607.13344#S4)introduces syntax and semantics of language constructs used to express optimization statements within programs supported by the system\. This section concludes with the details on the implementation\. In Section[5](https://arxiv.org/html/2607.13344#S5), we discuss results on benchmarking the performance ofezsmtv3against its closest CASP relatives such asclingcon,clingo\[LP\]andclingo\[DL\]\. We note that the capabilities ofezsmtv3extends beyond any of these peers as, for example, the system is capable to support reasoning with constraint atoms that contain both integer and real variables\. At last we remark on future work\.

## 2Background

### 2\.1Logic Programs and Input Answer Sets

Many definitions presented in this section follow the lines by[Lierler](https://arxiv.org/html/2607.13344#bib.bib142)\[[2023a](https://arxiv.org/html/2607.13344#bib.bib142), Sections 3 and 4\]\.

##### Logic programs

Avocabularyis a set of propositional symbols, also called atoms\. Aliteralis an atomaaor its negation¬a\\neg a\. A*\(propositional\) logic program*over vocabularyσ\\sigmais a set of*rules*of the form

a←b1,…,bℓ,n​o​t​bℓ\+1,…,n​o​t​bm,n​o​tn​o​t​bm\+1,…,n​o​tn​o​t​bn\.\\begin\{array\}\[\]\{l\}a\\leftarrow b\_\{1\},\\ldots,b\_\{\\ell\},\\ not\\ b\_\{\\ell\+1\},\\ldots,\\ not\\ b\_\{m\},\\ \\ not\\ \\ not\\ b\_\{m\+1\},\\ldots,\\ not\\ \\ not\\ b\_\{n\}\.\\end\{array\}\(1\)whereaais an atom inσ\\sigmaor⊥\\bot, and eachbib\_\{i\}, where1≤i≤n1\\leq i\\leq n, is an atom inσ\\sigma\. We will use the abbreviated form of a rule \([1](https://arxiv.org/html/2607.13344#S2.E1)\), i\.e\.,

whereBBstands for the right hand side of the arrow in \([1](https://arxiv.org/html/2607.13344#S2.E1)\), and is also called abody\. ByB\+B^\{\+\}we denote thepositivepart of bodyBB, i\.e\.,b1,…,bℓb\_\{1\},\\ldots,b\_\{\\ell\}\. We sometimes identify bodyBBwith the propositional formula

b1∧…∧bℓ∧¬bℓ\+1∧…∧¬bm∧¬¬bm\+1∧…∧¬¬bn\.b\_\{1\}\\wedge\\ldots\\wedge b\_\{\\ell\}\\wedge\\neg b\_\{\\ell\+1\}\\wedge\\ldots\\wedge\\neg b\_\{m\}\\wedge\\neg\\neg b\_\{m\+1\}\\wedge\\ldots\\wedge\\neg\\neg b\_\{n\}\.\(3\)and rule \([1](https://arxiv.org/html/2607.13344#S2.E1)\) with the propositional formula \(implication\)B→aB\\rightarrow a\. The expressionaais the*head*of the rule\. A rule whose head is the symbol⊥\\botis called adenial\. A rule \([2](https://arxiv.org/html/2607.13344#S2.E2)\) whose body is empty, i\.e\.,n=0n=0is called afact; in this case it is frequently written asa\.a\.\(whileBBis identified with⊤\\topand⊤→a\\top\\rightarrow ais identified withaa\)\. For a logic programΠ\\Pi\(a propositional formulaFF\), by𝐴𝑡​\(Π\)\\mathit\{At\}\(\\Pi\)\(by𝐴𝑡​\(F\)\\mathit\{At\}\(F\)\) we denote the set of atoms occurring inΠ\\Pi\(inFF\)\.

It is customary for a given vocabularyσ\\sigma, to identify a setXXof atoms overσ\\sigmawith \(i\) a complete and consistent set of literals overσ\\sigmaconstructed asX∪\{¬a∣a∈σ∖X\}X\\cup\\\{\\neg a\\mid a\\in\\sigma\\setminus X\\\}, and respectively with \(ii\) an assignment function or interpretation that assigns truth value𝑡𝑟𝑢𝑒\\mathit\{true\}to every atom inXXand𝑓𝑎𝑙𝑠𝑒\\mathit\{false\}to every atom inσ∖X\\sigma\\setminus X\. Within the scope of this paper, we are interested in sets of atoms in relation to respective programs, so that the signature of that program will be considered for reference\. We say a setXXof atomssatisfiesrule \([2](https://arxiv.org/html/2607.13344#S2.E2)\), ifXX\(understood as an assignment function\) satisfies the propositional formulaB→aB\\rightarrow a\. Naturally, we can speak about setXXsatisfying the body or the negative part of the body of the rule as we identify these with respective propositional formulas\. We sayXXsatisfies a programΠ\\Pi, ifXXsatisfies every rule inΠ\\Pi\. In this case, we also say thatXXis a model ofΠ\\Pi\. We may abbreviate the satisfaction relation with symbol⊧\\models\(to denote that a set of atoms satisfies a rule, a body, a program, or a formula\)\.

ThereductΠX\\Pi^\{X\}of a programΠ\\Pirelative to a setXXof atoms is obtained by first removing all rules \([1](https://arxiv.org/html/2607.13344#S2.E1)\) such thatXXdoes not satisfy the negative part of the body

¬bℓ\+1∧…∧¬bm∧¬¬bm\+1∧…∧¬¬bn,\\neg b\_\{\\ell\+1\}\\wedge\\ldots\\wedge\\neg b\_\{m\}\\wedge\\neg\\neg b\_\{m\+1\}\\wedge\\ldots\\wedge\\neg\\neg b\_\{n\},and replacing all remaining rules witha←b1,…,bℓa\\leftarrow b\_\{1\},\\ldots,b\_\{\\ell\}\.

###### Definition 1\(Answer set\)

A setXXof atoms is an answer set, if it is the minimal set that satisfies all rules ofΠX\\Pi^\{X\}\[Lifschitzet al\.,[1999](https://arxiv.org/html/2607.13344#bib.bib72)\]\.

###### Example 1

Consider a program

b←a\.c←n​o​t​a\.\\begin\{array\}\[\]\{l\}b\\leftarrow a\.\\\\ c\\leftarrow not\\ a\.\\\\ \\end\{array\}\(4\)This program has a single answer set, namely,\{c\}\\\{c\\\}\. Let us construct a new program from program \([4](https://arxiv.org/html/2607.13344#S2.E4)\) by appending a single fact to it\.

a\.b←a\.c←n​o​t​a\.\\begin\{array\}\[\]\{l\}a\.\\\\ b\\leftarrow a\.\\\\ c\\leftarrow not\\ a\.\\\\ \\end\{array\}\(5\)This program has a single answer set, namely,\{a,b\}\\\{a,b\\\}\.

Consider now another program

a←n​o​t​n​o​t​a\.b←a\.c←n​o​t​a\.\\begin\{array\}\[\]\{l\}a\\leftarrow not\\ not\\ a\.\\\\ b\\leftarrow a\.\\\\ c\\leftarrow not\\ a\.\\\\ \\end\{array\}\(6\)The first rule of this program is typically written as

Rules of this form are calledchoice rules\. We can intuitively read the rule above as “atomaamay be the case”\. This program has two answer sets:

\{a,b\}\\\{a,b\\\}and\{c\}\\\{c\\\}\.\(7\)
We now state the definition of an input answer set, as it is instrumental in defining constraint answer set programs\.

###### Definition 2\(Input Answer Set\)

For a logic programΠ\\Piover vocabularyσ\\sigmaand vocabularyι⊆σ\\iota\\subseteq\\sigmasuch that none ofι\\iota’s elements occur in the heads of rules inΠ\\Pi, a setXXof atoms overσ\\sigmais an*input answer set*ofΠ\\Pirelative toι\\iota, whenXXis an answer set of the programΠ∪\(X∩ι\)\\Pi\\cup\(X\\cap\\iota\)\.

Recall program \([4](https://arxiv.org/html/2607.13344#S2.E4)\), which has two input answer sets relative to signature\{a\}\\\{a\\\}\. These answer sets are listed in \([7](https://arxiv.org/html/2607.13344#S2.E7)\)\.

The reader may obtain new insights about the definition of an input answer set in light of the following formal result\.

###### Proposition 1

For a logic programΠ\\Piover vocabularyσ\\sigmaand vocabularyι⊆σ\\iota\\subseteq\\sigmasuch that none ofι\\iota’s elements occur in the heads of rules inΠ\\Pi, the answer sets of a program

Π∪\{\{a\}\.∣a∈ι\}\\Pi\\cup\\\{~\\\{a\\\}\.~\\mid a\\in\\iota\\\}coincide with the input answer sets of programΠ\\Pirelative toι\\iota\.

Thus it is not by chance that answer sets of program \([6](https://arxiv.org/html/2607.13344#S2.E6)\) and input answer sets of program \([4](https://arxiv.org/html/2607.13344#S2.E4)\) relative to signature\{a\}\\\{a\\\}coincide\.

Thedependency graphofΠ\\Piis the directed graphGGsuch that

- •the vertices ofGGare the atoms occurring inΠ\\Pi, and
- •for every rule \([1](https://arxiv.org/html/2607.13344#S2.E1)\) inΠ\\Piwhose head is not⊥\\bot,GGhas an edge from atomaato each atom in positive partb1,…,bℓb\_\{1\},\\dots,b\_\{\\ell\}of its body\.

A program is calledtightif its dependency graph is acyclic\. It is easy to see that any sample program discussed so far is tight\. The simplest nontight program is as followsa←a\.a\\leftarrow a\.

### 2\.2Constraints, CSP, SMT

Lierler and Susman\[[2017](https://arxiv.org/html/2607.13344#bib.bib108)\]illustrated that the notion of a constraint syntactically coincides with ground literals of satisfiability modulo theories \(SMT\)\. Furthermore, a constraint satisfaction problem \(CSP\) — posed as a set of constraints — can be identified with a conjunction of ground literals, which is evaluated by means of first\-order logic interpretations/structures representative of a particular “uniform” SMT\-logic\[Lierler and Susman,[2017](https://arxiv.org/html/2607.13344#bib.bib108)\]\. Thus, in a way we can understand satisfiability modulo theories via the lens of satisfiability modulo constraints\.

Intuitively, uniform SMT\-logics are defined via interpretations/structures whose domain, interpretation of “theory/constraint/interpreted” predicate symbols, and “interpreted” function symbols are fixed\. In practice, special forms of constraints are commonly used\.Integer linear constraintsare examples of these special cases\. Let us recall their syntactic shape and provide some intuitions for their interpretations prior to diving into formal settings\. An\(integer\) linear expressionhas the form

a1​x1\+⋯\+an​xn,a\_\{1\}x\_\{1\}\+\\cdots\+a\_\{n\}x\_\{n\},\(8\)wherea1,…,ana\_\{1\},\\dots,a\_\{n\}are \(integer\) numbers andx1,…,xnx\_\{1\},\\dots,x\_\{n\}are \(constraint\) variables whose domain ranges over \(integer\) numbers\. Note how this definition encapsulates both integer linear expressions and linear expressions over real numbers\. For the latter, we drop the word integer as a requirement on coefficients and variables\. It is customary to omit coefficients when their value is11and also replace\+\+by−\-when the coefficient is a negative number, while that negative number is replaced by its absolute value\. The SMT technology utilizes the standard SMT\-LIB language\[Barrettet al\.,[2010](https://arxiv.org/html/2607.13344#bib.bib150)\]\. In that language prefix notation is used so that expression \([8](https://arxiv.org/html/2607.13344#S2.E8)\) is written as

\+\(×\(a1,x1\),\+\(×\(a2,x2\),⋯\+\(×\(an−1,xn−1\),×\(an,xn\)\)…\)\.\+\(\\times\(a\_\{1\},x\_\{1\}\),\+\(\\times\(a\_\{2\},x\_\{2\}\),\\dots\+\(\\times\(a\_\{n\-1\},x\_\{n\-1\}\),\\times\(a\_\{n\},x\_\{n\}\)\)\\dots\)\.We call a constraint\(integer\) linearwhen it has the form

whereeeis \(an integer\) linear expression,kkis \(an integer\) number, and⋈\\bowtiebelongs to

\{<,\>,≤,≥,=,≠\}\.\\\{<,\>,\\leq,\\geq,=,\\neq\\\}\.\(10\)We can write \([9](https://arxiv.org/html/2607.13344#S2.E9)\) as an expression⋈\(e,k\)\\bowtie\(e,k\)in prefix notation\. Wheneeis also written in prefix notation, it is easy to see how this constraint takes the shape of a ground atom\. Let us agree to call these kinds of atomsconstraint \(ground\) atoms\. In the sequel, we use the termsconstraintandconstraint atominterchangeably\.

For instance, consider an integer linear constraint

When written in prefix notation it takes the shape of constraint ground atom

\>\(\+\(×\(2,x\),×\(3,y\)\),0\),\>\(\+\(\\times\(2,x\),\\times\(3,y\)\),0\),where

- •\>\>is a binary “interpreted” predicate symbol;
- •\+\+and×\\timesare binary “interpreted” function symbols;
- •0,22, and33are 0\-arity “interpreted” function symbols; and
- •xxandyyare 0\-arity “un\-interpreted” function symbols\.

In the logic literature, 0\-arity un\-interpreted function symbols are frequently referred to as object constants, whereas in the constraint processing literature they are referred to as \(constraint\) variables\. Here, we use the termconstraint variables\. Prior to some formal definitions, let us talk about this constraint atom as a formula within satisfiability modulo Linear Integer Arithmetic Logic, intuitively\. This logic is defined by interpretations, such that

- •\>\>is interpreted as an arithmetic greater than relation;
- •\+\+and×\\timesare interpreted as usual in arithmetic;
- •0,22, and33are mapped into respective integer domain elements identified with the same symbol, thus we may also refer to these function symbols as integers; and
- •xxandyyare mapped into integers; in general, the domain for 0\-arity function symbols occurring in constraint atoms is the set of integers\.

In naming the constraints, we use conventions adopted by SMT\-LIB222[https://smt\-lib\.org/logics\.shtml](https://smt-lib.org/logics.shtml)so that

- •IA stands for the theory Ints \(Integer Arithmetic\);
- •RA stands for the theory Reals \(Real Arithmetic\);
- •IRA stands for the theory Reals and Ints \(mixed Integer Real Arithmetic\);
- •IDL stands for Integer Difference Logic;
- •L before IA, RA, or IRA stands for the linear fragment of those arithmetics\.

Let us call

- •integer linear constraints —LIA constraint atoms \(LIA constraints\);
- •linear constraints —LRA constraint atoms \(LRA constraints\);
- •constraints that syntactically have the form of expression \([9](https://arxiv.org/html/2607.13344#S2.E9)\), while the coefficients and constraint variables of this expression can be both integer and real numbers —mixed integer real constraint atoms \(LIRA constraints\);
- •constraints that have the form x−y⋈c​or​x⋈y,x\-y\\bowtie c\\hbox\{~~~~~~ or~~~~~~ \}x\\bowtie y,\(12\)where⋈\\bowtieis one of the arithmetic relations in \([10](https://arxiv.org/html/2607.13344#S2.E10)\),xxandyyare constraint variables over integers, andccis an integer —IDL constraint atoms \(IDL constraints\)\.

We are now ready to provide formal definitions for four logics within SMT framework utilized in this work\.

###### Definition 3\(Satisfiability Modulo Theories Formula or SMT Formula\)

Formula in satisfiability modulo Linear Integer Arithmetic Logic or SMT\(LIA\) Formula — is a variable\-free first order logic formula that consists of propositional or LIA constraint atoms\. Its interpretations can be captured by valuations – functions – that map all propositional atoms to truth values and constraint variables to integers; while arithmetic predicate and function symbols are interpreted as customary in arithmetic\.

SMT\(LRA\) formulas or SMT formulas in LRA Logic, SMT\(LIRA\) formulas or SMT formulas in LIRA Logic, SMT\(IDL\) formulas or SMT formulas in IDL Logic are defined similarly considering LRA, LIRA, and IDL constraint atoms, respectively, in place of LIA constraint atoms\. Interpretations for these formulas are captured by valuations that respect domains of the constraint atoms according to their types\.

Models of SMT formulas are interpretations that satisfy SMT formulas, where the satisfaction relation is understood classically as in first order logic\.

###### Example 2

For instance, the SMT\(LIA\) formula

p→\(\(x≥1∧x≤3\)∨x=5\)\.p\\rightarrow\\big\(\(x\\geq 1\\wedge x\\leq 3\)\\vee x=5\\big\)\.\(13\)consists of propositional atomppand LIA constraint atoms

x≥1x≤3x=5\.\\begin\{array\}\[\]\{lll\}x\\geq 1&x\\leq 3&x=5\.\\end\{array\}This formula has four models whenppis interpreted as𝑡𝑟𝑢𝑒\\mathit\{true\}captured by the following valuations

x↦1p↦𝑡𝑟𝑢𝑒x↦2p↦𝑡𝑟𝑢𝑒x↦3p↦𝑡𝑟𝑢𝑒x↦5p↦𝑡𝑟𝑢𝑒\\begin\{array\}\[\]\{ll\}x\\mapsto 1&p\\mapsto\\mathit\{true\}\\\\ x\\mapsto 2&p\\mapsto\\mathit\{true\}\\\\ x\\mapsto 3&p\\mapsto\\mathit\{true\}\\\\ x\\mapsto 5&p\\mapsto\\mathit\{true\}\\\\ \\end\{array\}There are an infinite number of models for this formula whenppis interpreted as𝑓𝑎𝑙𝑠𝑒\\mathit\{false\}including, for example, one captured by the valuation

x↦4p↦𝑓𝑎𝑙𝑠𝑒\.\\begin\{array\}\[\]\{ll\}x\\mapsto 4&p\\mapsto\\mathit\{false\}\.\\end\{array\}

We are now ready to state definitions for constraint satisfaction problems\.

###### Definition 4\(Constraint satisfaction problem or CSP\)

We call a finite set of constraints a constraint satisfaction problem \(CSP\)\. Within this work we will consider CSPs of particular kind\. Namely,

- •Linear Integer Arithmetic CSP \(LIA CSP\) formed as a set of LIA constraints;
- •Linear Real Arithmetic CSP \(LRA CSP\) formed as a set of LRA constraints;
- •LIRA CSP formed as a set of LIRA constraints;
- •Integer Difference Logic CSP \(IDL CSP\) formed as a finite set of IDL constraints\.

As we identify constraints with ground atoms, we also identify a CSP with a conjunction of constraints/ground atoms occurring in its set\. Thus, any LIA CSP, LRA CSP, LIRA CSP, and IDL CSP can be viewed as a special form of SMT\(LIA\), SMT\(LRA\), SMT\(LIRA\), SMT\(IDL\) formula, respectively\. We call models of these formulas solutions of respective CSPs\.

###### Example 3

One of the solutions to the LIA CSP composed of a single constraint \([11](https://arxiv.org/html/2607.13344#S2.E11)\) is a valuation that mapsxxto0andyyto11\. If we are to form another LIA CSP – a set composed of constraint \([11](https://arxiv.org/html/2607.13344#S2.E11)\) and constrainty≠1y\\neq 1, then the valuation that mapsxxto0andyyto11is not a solution, while, for instance, a valuation that mapsxxto0andyyto22is\.

Both LRA and IDL CSPs are interesting from the perspective that there are tractable algorithms to decide whether these problems have solutions\. This is not the case for LIA and LIRA CSPs\.

### 2\.3Constraint answer set programs and their relation to SMT

Letσr\\sigma\_\{r\}andσi\\sigma\_\{i\}be two disjoint vocabularies\. We refer to their elements as*regular*and*irregular*333In the literature on constraint answer set programming, atoms of this kind are frequently calledconstraintatoms\. In the literature on satisfiability modulo theories, atoms with similar role are calledtheoryatoms\.atoms, respectively\.

###### Definition 5\(Constraint Answer Set Program or CAS Program\)

Letσ=σr∪σi\\sigma=\\sigma\_\{r\}\\cup\\sigma\_\{i\}be a vocabulary so thatσr\\sigma\_\{r\}andσi\\sigma\_\{i\}are disjoint;ℬ\\mathcal\{B\}be a set of constraints;γ\\gammabe an injective function from the set of irregular literals overσi\\sigma\_\{i\}toℬ\\mathcal\{B\}\.

We call a tripleP=⟨Π,ℬ,γ⟩P=\\langle\\Pi,\\mathcal\{B\},\\gamma\\ranglea CAS program over vocabularyσr∪σi\\sigma\_\{r\}\\cup\\sigma\_\{i\}, whenΠ\\Piis a logic program overσr∪σi\\sigma\_\{r\}\\cup\\sigma\_\{i\}such that any rule that contains atoms inσi\\sigma\_\{i\}is a rule with symbol⊥\\botin its head\.

A setX⊆𝐴𝑡​\(Π\)X\\subseteq\\mathit\{At\}\(\\Pi\)of atoms is an*answer set*ofPPif

1. \(a\)XXis an input answer set ofΠ\\Pirelative toσi\\sigma\_\{i\}, and
2. \(b\)the following CSP has a solution:\{γ​\(a\)∣a∈X∩σi\}∪\{γ​\(¬a\)∣a∈σi∖X\}\.\\\{\\gamma\(a\)\\mid a\\in X\\cap\\sigma\_\{i\}\\\}\\cup\\\{\\gamma\(\\neg a\)\\mid a\\in\\sigma\_\{i\}\\setminus X\\\}\.

A pair⟨X,ν⟩\\langle X,\\nu\\rangleis an*extended answer set*ofPPifXXis an*answer set*ofPPand valuationν\\nuis a solution to the CSP constructed in \(b\)\.

Within this work we consider CAS programs⟨Π,ℬ,γ⟩\\langle\\Pi,\\mathcal\{B\},\\gamma\\rangleof a particular kind\. Namely,

- •CAS\(LIA\) programs whose setℬ\\mathcal\{B\}of constraints is formed by LIA constraints;
- •CAS\(LRA\) programs whose setℬ\\mathcal\{B\}of constraints is formed by LRA constraints;
- •CAS\(LIRA\) programs whose setℬ\\mathcal\{B\}of constraints is formed by LIRA constraints;
- •CAS\(IDL\) programs whose setℬ\\mathcal\{B\}of constraints is formed by IDL constraints\.

It is due to note that when CAS programs are written in practice, the CASP systems permit a user listing an irregular atom in the head of the rule\. Yet, that should be considered as “syntactic sugar” so that a rule of the form \([2](https://arxiv.org/html/2607.13344#S2.E2)\), whereaais an irregular atom is seen as an abbreviation for the rule

←B,n​o​t​a\.\\leftarrow B,\\ not\\ a\.In the presentation, we utilize vertical bars to mark the irregular atoms which will have intuitive mappings into their respective constraints\. For instance, irregular atom\|x≥12\|\|x\\geq 12\|naturally maps into constraintx≥12x\\geq 12\.

###### Example 4

We now exemplify the definition of a CAS program\. LetΠ1\\Pi\_\{1\}be logic program \([6](https://arxiv.org/html/2607.13344#S2.E6)\) extended with a denial

←a,\|x≥12\|,\\leftarrow a,\\ \|x\\geq 12\|,where\|x≥12\|\|x\\geq 12\|denotes an irregular atoms with constraint variablexx\. Letℬ1\\mathcal\{B\}\_\{1\}be a set of integer linear constraints\{x≥12,x<12\}\\\{x\\geq 12,x<12\\\};γ1\\gamma\_\{1\}be an injective function from irregular literals in the signature ofΠ1\\Pi\_\{1\}to constraints

\|x≥12\|→x≥12,¬\|x≥12\|→x<12\.\|x\\geq 12\|\\rightarrow x\\geq 12,\\ \\ \\ \\ \\neg\|x\\geq 12\|\\rightarrow x<12\.CAS program⟨Π1,ℬ1,γ1⟩\\langle\\Pi\_\{1\},\\mathcal\{B\}\_\{1\},\\gamma\_\{1\}\\ranglehas three answer sets, namely,

\{a,b\}\{c\}\{c,\|x≥12\|\}\\begin\{array\}\[\]\{l\}\\\{a,b\\\}\\\\ \\\{c\\\}\\\\ \\\{c,\|x\\geq 12\|\\\}\\\\ \\end\{array\}and infinitely many extended answer sets:

\{a,b,x↦11\}\{a,b,x↦10\}\{a,b,x↦9\}​…\{c,x↦11\}\{c,x↦10\}\{c,x↦9\}​…\{c,\|x≥12\|,x↦12\}\{c,\|x≥12\|,x↦13\}\{c,\|x≥12\|,x↦14\}…\\begin\{array\}\[\]\{lll\}\\\{a,b,x\\mapsto 11\\\}&\\\{a,b,x\\mapsto 10\\\}&\\\{a,b,x\\mapsto 9\\\}\\dots\\\\ \\\{c,x\\mapsto 11\\\}&\\\{c,x\\mapsto 10\\\}&\\\{c,x\\mapsto 9\\\}\\dots\\\\ \\\{c,\|x\\geq 12\|,x\\mapsto 12\\\}&\\\{c,\|x\\geq 12\|,x\\mapsto 13\\\}&\\\{c,\|x\\geq 12\|,x\\mapsto 14\\\}\\dots\\\\ \\end\{array\}

We refer to CAS programP=⟨Π,ℬ,γ⟩P=\\langle\\Pi,\\mathcal\{B\},\\gamma\\rangleastightwhen its first memberΠ\\Pihas this property\.

[Lierler and Susman](https://arxiv.org/html/2607.13344#bib.bib108)\[[2017](https://arxiv.org/html/2607.13344#bib.bib108)\]illustrated that for CAS programs of the four kinds considered here, one can construct an SMT formula \(of the four kinds considered here\) so that its models coincide with the extended answer sets of the given program\. They generalized the concepts of completion and level ranking – originally introduced bycla78andNiemelä \[[2008](https://arxiv.org/html/2607.13344#bib.bib944)\], respectively – which are essential in the construction of such an SMT formula\. Intuitively, completion is a process that turns a CAS program into an SMT formula\. This formula comes with a special guarantee that every extended answer set of the given program is a model of its completion\. For the class of tight programs the reverse direction is also the case\. As a result, the extended answer sets of a CAS program coincide with the models of its completion\. In case of a program being nontight, so called level ranking constraints added to a completion will ensure that computed models \(modulo newly introduced integer variables within level ranking constraints\) are exactly the answer sets\. We now provide details of that translation relevant to understanding the workings of theezsmtv3system\.

Within the translation, irregular atoms are introduced that encode level ranking constraints required to weed out models of the completion that are not answer sets\. For instance, an irregular atom\|lra−lrb≥1\|\|lr\_\{a\}\-lr\_\{b\}\\geq 1\|encodes an IDL \(or LIA or LIRA\) constraintl​ra−l​rb≥1lr\_\{a\}\-lr\_\{b\}\\geq 1, wherel​ralr\_\{a\}andl​rblr\_\{b\}are integer constraint variables\. LetP=⟨Π,ℬ,γ⟩P=\\langle\\Pi,\\mathcal\{B\},\\gamma\\ranglebe a CAS program overσr∪σi\\sigma\_\{r\}\\cup\\sigma\_\{i\}\. If a program is not tight, for every atoma∈σra\\in\\sigma\_\{r\}that occurs inΠ\\Pi, we introduce an integer variablel​ralr\_\{a\}\. The SMT formulaℱP\\mathcal\{F\}^\{P\}is constructed as a conjunction of the following

1. 1\.implications corresponding to rules \([1](https://arxiv.org/html/2607.13344#S2.E1)\) inΠ\\Pi;
2. 2\.for each regular atomaaoccurring within the given CAS program, the implication - •a→⋁a←B∈ΠBa\\rightarrow\\displaystyle\\bigvee\_\{a\\leftarrow B\\in\\Pi\}B, when the program is tight - •a→⋁a←B∈Π\(B∧⋀b∈B\+∖σi\|l​ra−l​rb\|≥1\)a\\rightarrow\\displaystyle\\bigvee\_\{a\\leftarrow B\\in\\Pi\}\\big\(B\\wedge\\bigwedge\_\{b\\in B^\{\+\}\\setminus\\sigma\_\{i\}\}\|lr\_\{a\}\-lr\_\{b\}\|\\geq 1\\big\), otherwise;
3. 3\.for each irregular atom\|c\|∈σi\|c\|\\in\\sigma\_\{i\}occurring within the given CAS program \(whereccis a constraint; recall that irregular atoms are assumed to have a natural mapping into respective constraints\), the equivalence\|c\|⟷c\|c\|\\ \\longleftrightarrow\\ c;
4. 4\.in case the considered program is not tight, for each irregular atom of the form\|lra−lrb≥1\|\|lr\_\{a\}\-lr\_\{b\}\\geq 1\|introduced within the translation, the equivalence \|lra−lrb≥1\|⟷lra−lrb≥1\.\|lr\_\{a\}\-lr\_\{b\}\\geq 1\|\\ \\longleftrightarrow\\ lr\_\{a\}\-lr\_\{b\}\\geq 1\.

In case of a tight CAS programPP, formulaℱP\\mathcal\{F\}^\{P\}captures the completion ofPP\.

###### Example 5

Recall CAS program⟨Π1,ℬ1,γ1⟩\\langle\\Pi\_\{1\},\\mathcal\{B\}\_\{1\},\\gamma\_\{1\}\\ranglefrom Example[4](https://arxiv.org/html/2607.13344#Thmexample4)\. Let us call itP1P\_\{1\}\.ℱP1\\mathcal\{F\}^\{P\_\{1\}\}is as follows

¬¬a→aa→b¬a→ca∧\|x≥12\|→⊥a→¬¬ab→ac→¬a\|x≥12\|⟷x≥12\\begin\{array\}\[\]\{llll\}\\neg\\neg a\\rightarrow a&a\\rightarrow b&\\neg a\\rightarrow c&a\\wedge\\ \|x\\geq 12\|\\rightarrow\\bot\\\\ a\\rightarrow\\neg\\neg a&b\\rightarrow a&c\\rightarrow\\neg a&\\\\ \|x\\geq 12\|\\longleftrightarrow x\\geq 12&&&\\\\ \\end\{array\}The models of this formula coincide with the answer sets of⟨Π1,ℬ1,γ1⟩\\langle\\Pi\_\{1\},\\mathcal\{B\}\_\{1\},\\gamma\_\{1\}\\rangle\.

Figure 1:Mapping of CAS programs to respective SMT formulas\.Figure[1](https://arxiv.org/html/2607.13344#F1)summarizes the details on which kind of SMT formula systemezsmtv3obtains during the application of the described translation process depending on the properties of the given CAS program\. For instance, row 2 in the table of this figure states that given a CAS\(LRA\) program which is

- •tight, the translation results in SMT\(LRA\) formula;
- •non\-tight, the translation results in SMT\(LIRA\) formula\.

## 3ezsmtVersion 3 Language\(s\), Use Case, and Architecture

This section is devoted at large to the description of the language and architecture of theezsmtVersion 3 system, abbreviated asezsmtv3\. Prior to providing the details on the system’s components, we articulate a bird’s\-eye view on the system by pointing at its major design choices\. We also provide a sample use case of the system utilizing the Traveling Salesman problem\. The presentation of this use case is intermixed with the details on the syntactic constructs supported by theezsmtv3together with their mappings into respective CAS fragments\.

In a way,ezsmtv3can be seen as a system that puts together the ideas and practices behind two CASP solvers, namely,clingconversion 3 \(and above\)\[Banbaraet al\.,[2017](https://arxiv.org/html/2607.13344#bib.bib128)\]andezsmt\+\[Shen and Lierler,[2018b](https://arxiv.org/html/2607.13344#bib.bib137)\]\. In particular, fromclingconit borrows an idea to utilize capabilities unique to the groundergringoversion 5\[Gebseret al\.,[2016](https://arxiv.org/html/2607.13344#bib.bib130)\]\. This grounder provides a possibility

- •to specify the grammar of the language of constraints of interest and
- •to use that newly defined language in writing programs that are subsequently grounded bygringo\.

Fromezsmt\+,ezsmtv3borrows an idea to utilize an SMT solver, such asz3orcvc5, as its search engine back\-end after computing completion and level rankings of a given CAS program\. The combination of thegringoversion 5 front\-end and an SMT solver as a back\-end uniquely positions systemezsmtv3not only as a CASP solver but also as an easily extensible framework for creating new kinds of CASP solvers\. Indeed, SMT solvers support a multitude of distinct logics – languages for specifications of constraint atoms – whilegringoversion 5 allows us to specify a language of such constraint atoms and quickly incorporate these within the grounding stage of processing\. The major routines of building completion and then translating that internal representation into the standard language supported by SMT solvers, namely, SMT\-LIB is something thatezsmtv3inherits fromezsmt\+and provides as part of the framework for extensions to new logics\. In the sequel, we omit the reference to version ofgringoassuming version 5 as default\.

### 3\.1ezsmtv3Language\(s\) and Its Use Case

We start this section by uncovering the details of theezsmtv3language used for formulating programs in CAS\(LIA\)\. We then present the CAS\(LIA\) formalization of a variant of the Traveling Salesman \(TS\) Problem \([Lawleret al\.](https://arxiv.org/html/2607.13344#bib.bib140),[1985](https://arxiv.org/html/2607.13344#bib.bib140);[Gutin and Punnen](https://arxiv.org/html/2607.13344#bib.bib141),[2007](https://arxiv.org/html/2607.13344#bib.bib141)\)\. The presented CAS\(LIA\) program is written in the language supported by systemsezsmtv3\(andclingcon\)\. The similar formalization of the TS problem was presented byLierler \[[2023a](https://arxiv.org/html/2607.13344#bib.bib142)\]in the language supported by the CASP solversezcsp\[Balduccini and Lierler,[2017](https://arxiv.org/html/2607.13344#bib.bib27)\]\(andezsmt\+\)\. At last, we discuss the details ofezsmtv3language used for formulating programs in CAS\(LRA\), CAS\(LIRA\), and CAS\(IDL\)\.

#### 3\.1\.1ezsmtv3CAS\(LIA\) Language

As mentioned earlier, systemgringois used withinezsmtv3as a front\-end to ground a considered CAS program\. Section[3\.1\.2](https://arxiv.org/html/2607.13344#S3.SS1.SSS2)demystifies the process of grounding\. It presents the Traveling Salesman problem encoding that is formalized using CAS\(LIA\) “schemata” rules — rules that contain “ASP” variables and hence can be seen as abbreviations for groups of corresponding ground/propositional CAS\(LIA\) rules such as presented in preliminaries\. Within this section, we consider ground/propositional programs for simplicity\.

Listing 1:Encoding of LIA Logic ingringoversion 5\.1\#theorylia\{

linear\_term\{

3\-:2,unary;

\*:1,binary,left;

5\+:0,binary,left;

\-:0,binary,left

7\};

9dom\_term\{

\-:3,unary;

11\+:3,unary;

\*:2,binary,left;

13\+:1,binary,left;

\-:1,binary,left;

15\.\.:0,binary,left

\};

17

&dom/0:dom\_term,\{=\},linear\_term,head;

19&sum/0:linear\_term,\{<=,\>=,\>,<,=,\!=\},linear\_term,any;

&logic/1:linear\_term,head

21\}\.

Consider Listing[1](https://arxiv.org/html/2607.13344#LST1)\. It introduces the reader to the LIA language specification for groundergringoused withinezsmtv3, which echoes the one utilized withinclingconversion 5 \(clingconv5\)444The theory specification used withinclingconv5is located at[https://github\.com/potassco/clingcon/blob/master/libclingcon/clingcon/parsing\.hh](https://github.com/potassco/clingcon/blob/master/libclingcon/clingcon/parsing.hh)\.– the latest version of systemclingconrooted in the ideas byBanbaraet al\.\[[2017](https://arxiv.org/html/2607.13344#bib.bib128)\]\. Thus, any CAS\(LIA\) program forezsmtv3can be seen as a program written forclingconv5so that it can be solved by that system also\. \(It is due to remark thatclingconv5’s specification has additions that for instance specify such a directive as the&showstatement\. Yet,ezsmtv3does not support statements of the kind\.\) We can see the specification in Listing[1](https://arxiv.org/html/2607.13344#LST1)as a collection of requirements on the kinds of statements that we expectgringoto process\. We refer the reader to the paper byGebseret al\.\[[2016](https://arxiv.org/html/2607.13344#bib.bib130)\]for more details and intuitions behind the presented theory specification\. Here, we utilize examples to illustrate its purpose\. In addition to syntactic restrictions on the kinds of statements supported by specifications of Listing[1](https://arxiv.org/html/2607.13344#LST1), we pose additional requirements on these expressions, which have to be verified at the level whengringooutput is being processed\. Withinezsmtv3, we adopt the requirements closely related to those described by[Banbaraet al\.](https://arxiv.org/html/2607.13344#bib.bib128)\([2017](https://arxiv.org/html/2607.13344#bib.bib128), Pages 12 and 13\) for the constraints expressed using key words&domand&sum\. We now summarize the requirements and also discuss the nature of these constraints and how they are captured byezsmtv3\.

Domain Constraintshave the form

&d​o​m​\{d1;…;dm\}=t,\\texttt\{$\\&dom\\\{d\_\{1\};\\dots;d\_\{m\}\\\}=t$\},\(14\)where:

- •did\_\{i\}\(1≤i≤m1\\leq i\\leq m\) can beuuor a rangev\.\.wv\.\.w, withuu,vv,wwbeing of the form \([8](https://arxiv.org/html/2607.13344#S2.E8)\) so that - –aia\_\{i\}andxix\_\{i\}\(1≤i≤n1\\leq i\\leq n\) are integers \(with typical conventions such as, for instance, if one of the coefficients is in the multiplications of this expression is11it can be omitted\) and thus,uu,vv, andwwcan be evaluated to integers\); and - –v≤wv\\leq w\.
- •ttis a constraint variable\.

If expression \([14](https://arxiv.org/html/2607.13344#S3.E14)\) is such that everydid\_\{i\}\(1≤i≤m1\\leq i\\leq m\) is eitheruuor a rangev\.\.wv\.\.w, withuu,vv,wwbeingintegerswe call this statementnormal\. This expression is intuitively understood as imposing the following requirement on values that constraint variablettcan be mapped to\. Namely, any value in the following set⋃i=1n\[di\]\\bigcup\_\{i=1\}^\{n\}\[d\_\{i\}\], where

\[d\]=\{\{u\}ifdisu\{v,\.\.,w\}ifdisv\.\.w, wherev≤w\.\[d\]=\\begin\{cases\*\}$\\\{u\\\}$&if $d$ is $u$\\\\ $\\\{v,\.\.,w\\\}$&if $d$ is $v\.\.w$, where $v\\leq w$\.\\end\{cases\*\}
Internally,ezsmtv3simplifies&d​o​m\\&domstatements by evaluating possibly complex linear expressions occurring in these statements into corresponding integers resulting in the normal&d​o​m\\&domstatement\. For instance, consider the following lines to occur in someezsmtv3program

```
&dom{1..3; 5+3*4} = x:- a, not b.
&dom{1+2..4*4} = x.
```

Internally, they will be simplified by the system into

&d​o​m​\{1\.\.3;17\}=x←a,n​o​t​b\.&d​o​m​\{3\.\.16\}=x\.\\begin\{array\}\[\]\{l\}\\&dom\\\{1\.\.3;17\\\}=x\\leftarrow a,\\ not\\ b\.\\\\ \\&dom\\\{3\.\.16\\\}=x\.\\end\{array\}\(15\)
Syntactically, a \(ground\)ezsmtv3rule containing normal&d​o​m\\&domconstraint has the form

whereDDis expression \([14](https://arxiv.org/html/2607.13344#S3.E14)\) andBBis the body of this rule understood as in \([2](https://arxiv.org/html/2607.13344#S2.E2)\)\. Given the fact that withinezsmtv3we utilize SMT\(LIA\) formulas behind the stage to reason over a CAS\(LIA\) program, we present the semantics of statement \([16](https://arxiv.org/html/2607.13344#S3.E16)\) by means of translating it into an SMT\(LIA\) formula that has to be satisfied whenever statement \([16](https://arxiv.org/html/2607.13344#S3.E16)\) appears in the considered program\. We view \([16](https://arxiv.org/html/2607.13344#S3.E16)\) as an abbreviation for the following SMT\(LIA\) implication

B→\(\[\[d1\]\]∨⋯∨\[\[dn\]\]\),B\\rightarrow\\big\(\[\[d\_\{1\}\]\]\\vee\\cdots\\vee\[\[d\_\{n\}\]\]\\big\),where

\[\[d\]\]=\{t=uifdisu\(t≥v∧t≤w\)ifdisv\.\.w\.\[\[d\]\]=\\begin\{cases\*\}\\hbox\{$t=u$\}&if $d$ is $u$\\\\ \\hbox\{$\\big\(t\\geq v\\wedge t\\leq w\\big\)$\}&if $d$ is $v\.\.w$\.\\end\{cases\*\}Recall that we identify bodyBBwith the respective conjunction\. WhenBBis empty \(as, for instance, in the second line of \([15](https://arxiv.org/html/2607.13344#S3.E15)\)\), we can simplify the implication above and identify it with an expression

\[\[d1\]\]∨⋯∨\[\[dn\]\]\.\[\[d\_\{1\}\]\]\\vee\\cdots\\vee\[\[d\_\{n\}\]\]\.
For instance, the groundezsmtv3rules listed in \([15](https://arxiv.org/html/2607.13344#S3.E15)\) are understood as the conjunction of the following SMT\(LIA\) formulas:

\(a∧¬b\)→\(\(x≥1∧x≤3\)∨x=17\),\(x≥3∧x≤16\)\.\\begin\{array\}\[\]\{l\}\(a\\wedge\\neg b\)\\rightarrow\\big\(\(x\\geq 1\\wedge x\\leq 3\)\\vee x=17\\big\),\\\\ \(x\\geq 3\\wedge x\\leq 16\)\.\\end\{array\}
Here, it is due to note thatclingconis based on finite domain constraint solving so that in its implementation constraint variables over integers are considered within a default domain−230​\.\. 230\-2^\{30\}\\ \.\.\\ 2^\{30\}unless a&d​o​m\\&domexpression is provided for this variable that restricts its range; in case ofezsmtv3no restrictions on the range of integers are considered by default\.

Linear Constraintshave the form

&s​u​m​\{t1;…;tn\}⋈tn\+1,\\&sum\\\{t\_\{1\};\\dots;t\_\{n\}\\\}\\bowtie t\_\{n\+1\},\(17\)where:

- •eachtit\_\{i\}\(1≤i≤n\)\(1\\leq i\\leq n\)is an integer linear expression555Within the implementation, integer linear expressions are understood more liberally than defined here so that, for example2×22\\times 2or\(5\+2\)×z\(5\+2\)\\times zare considered within the realm of allowed syntax\.;
- •⋈\\bowtiebelongs to \([10](https://arxiv.org/html/2607.13344#S2.E10)\)\.

This syntax captures expressions of the formt1\+t2\+⋯\+tm⋈tm\+1t\_\{1\}\+t\_\{2\}\+\\dots\+t\_\{m\}\\bowtie t\_\{m\+1\}\. In turn, using standard algebraic operations this expression can be transformed into an integer linear constraint\. We view \([17](https://arxiv.org/html/2607.13344#S3.E17)\) as an irregular atom corresponding to an underlying integer linear constraint \(note that there may be multiple equivalent representations of such a constraint and any of these suffice for our purposes; indeedx<1x<1can be seen as an equivalent representation tox−1≤0x\-1\\leq 0\)\.

For instance, the expression of the form

```
&sum{2*2;3+x+(5+2)*z}=y
```

occurring within a groundezsmtv3program is identified with an irregular atom

\|x−y\+7×z=−7\|\|x\-y\+7\\times z=\-7\|which has a natural mapping into respective LIA constraint \(recall our convention to use vertical bars to denote irregular atoms\)\.

Syntactically, a \(ground\)ezsmtv3rule may contain expressions of the form \([17](https://arxiv.org/html/2607.13344#S3.E17)\) both in the head and the body of the rule, whileezsmtv3identifies them with respective irregular atoms\. For instance, the rule of the form

&sum\{2\*2;3\+x\+\(5\+2\)\*z\}=y:\- a, not b\.\(18\)is understood as a denial

←¬\|x−y\+7z=−7\|,a,notb\.\\leftarrow\\neg\|x\-y\+7z=\-7\|,\\ a,\\ not\\ b\.\(19\)
###### Example 6

Recall a program from Example[4](https://arxiv.org/html/2607.13344#Thmexample4)\. Using the describedezsmtv3CAS\(LIA\) language this program has the following form

```
{a}.
  b:-a.
  c:-not a.
  :-a, &sum{x}>=12.
```

#### 3\.1\.2Traveling Salesman Problem as CAS\(LIA\) Program

Let us state avariantof theTraveling Salesman Problem:

> We are given a graph with nodes as cities and edges as roads\. Each road directly connects a pair of cities, and costs a salesman some time to go through \(time is expressed as a positive integer value in this variant of the problem\)\. The salesman is supposed to pass each city exactly once\. Find: a route traversing all the cities, yet only once visiting each one of them, under certain maximum cost of total time\.

In the classical formulation of the TS problem, a route with the minimum cost is of interest\. Here, we state a decision problem in place of a related optimization problem\. Also, in the classical formulation there is no restriction on weights over routes being integers\.

Figure[2](https://arxiv.org/html/2607.13344#F2)shows an instance of the TS problem \(a weighted graph\)\. Listing[2](https://arxiv.org/html/2607.13344#LST2)encodes this representation as a set of facts\. On the right hand side of Figure[2](https://arxiv.org/html/2607.13344#F2), we find two solutions to this problem\.

Figure 2:Sample TS Instance and SolutionsListing 2:Encoding of the TS Instance\.city\(a\)\.city\(b\)\.city\(c\)\.city\(d\)\.

initial\(a\)\.

road\(a,b\)\.road\(b,c\)\.road\(c,d\)\.

cost\(a,b,1\)\.cost\(b,c,1\)\.cost\(c,d,1\)\.

road\(d,a\)\.road\(a,c\)\.road\(b,d\)\.

cost\(d,a,1\)\.cost\(a,c,2\)\.cost\(b,d,2\)\.

maxCost\(4\)\.

Listing[3](https://arxiv.org/html/2607.13344#LST3)presents the CASP encoding for the TS problem, whose instances are provided in the style of the instance presented in Listing[2](https://arxiv.org/html/2607.13344#LST2)\. This CASP encoding respects the LIA logic and supports the syntax specified by the theory specification in Listing[1](https://arxiv.org/html/2607.13344#LST1)\. Let us start by stating intuitions behind this encoding\. The first line specifies that theroadrelation is symmetric\. The second line suggests that thecostof the road taken in either directions is the same\. Line 4 specifies that for each city in the problem exactly one road that leads away from the city has to be part of the solution encoded by binary relationroute\. Line 5 specifies that for each city exactly one road that leads into this city has to be part of the solution\. Lines 7 and 8 encode a notion of a reached city from an initial city\. Line 10 requires that each city in the problem is identified as reached from the initial city\. Lines 12 through 15 utilize constructs, whose syntax is defined within the theory specification in Listing[1](https://arxiv.org/html/2607.13344#LST1)\. In other words, in the absence of the code within Listing[1](https://arxiv.org/html/2607.13344#LST1),gringowould identify these lines as outside of the scope of its applicability\. Line 12

- •introduces irregular atoms into discourse – atoms that refer to constraint variables and
- •specifies possible values for these constraint variables\.

Lines 13 through 15 state requirements/constraints on these variables\. In particular, Line 12 specifies a domain of possible values for the instances of constraint variables of the formc\(X,Y\)\. Namely, their domains are restricted by two values: one being0and another being the costs associated with the roads fromXXtoYY\. Lines 13 and 14 state the conditions on when instances of constraint variablesc\(X,Y\)are assigned0or the associated cost\. Line 15 specifies an integer linear constraint that states that the sum of all possible instances of constraint variablesc\(X,Y\)should not exceed the maximum cost specified\.

Listing 3:Encoding of the TS Problem\.1road\(Y,X\):\-road\(X,Y\)\.

cost\(Y,X,C\):\-cost\(X,Y,C\)\.

3

1\{route\(X,Y\):road\(X,Y\)\}1:\-city\(X\)\.

51\{route\(X,Y\):road\(X,Y\)\}1:\-city\(Y\)\.

7reached\(X\):\-initial\(X\)\.

reached\(Y\):\-reached\(X\),route\(X,Y\)\.

9

:\-city\(X\),notreached\(X\)\.

11

&dom\{0;C\}=c\(X,Y\):\-cost\(X,Y,C\)\.

13&sum\{c\(X,Y\)\}=0:\-cost\(X,Y,C\),notroute\(X,Y\)\.

&sum\{c\(X,Y\)\}=C:\-cost\(X,Y,C\),route\(X,Y\)\.

15:\-&sum\{c\(X,Y\):cost\(X,Y,C\)\}\>W,maxCost\(W\)\.

It is easy to see that the considered encoding of the TS problem contains kinds of rules that are outside of the syntax of logic programs presented in the Background section\. In particular, this program uses

- •ASP variables — namely,XX,YY,CC, andWW\(identifiers starting with the capital letters\) — so that program’s atoms are not propositional;
- •aggregate expressions within Lines 4 and 5\. In fact, each of these rules is an abbreviation for two rules, where one rule contains a choice expression in the head and another rule is a constraint containing count\-aggregate expression in the body\.

Aggregate expressions are the common constructs within the practice of answer set programming\. We refer an interested reader to the work byCalimeriet al\.\[[2020b](https://arxiv.org/html/2607.13344#bib.bib998)\], for instance, for more formal details on aggregates\. Here, we informally discuss their roles using Line 4 within Listing[3](https://arxiv.org/html/2607.13344#LST3)as an example\. The expression presented on the line is an abbreviation for two rules:

```
{route(X,Y)}:- road(X,Y), city(X).
:- not #count{X,Y:route(X,Y),road(X,Y)}=1, city(X).
```

The first line can be intuitively read asany road leading from some city may form a part of the route\. The wordmaypoints at thechoice\. The second rule contains acount\-aggregate expression and states thatfor a city exactly one tuple corresponding to a road should be considered to be part of the route\.

This is a good place to demystify the effects of the grounding process and the role of ASP variables\. The process ofgroundingis defined through ensuring that ASP variables are instantiated with all possible permutations of the object constants, so that a rule with ASP variables can be seen as an abbreviation for the group of propositional rules instantiated with the object constants occurring in the program\. Groundergringoperforms a process denoted asintelligent groundingthat is similar to a procedure well described byFaberet al\.\[[2012](https://arxiv.org/html/2607.13344#bib.bib15)\]\. While performing intelligent grounding a system attempts not only to instantiate given logic rules with all possible object constants of the considered program, but also to perform some simplifications and reductions that still guarantee that the produced propositional program has the same answer sets as the one that would be produced by the straight\-forward instantiation of grounding\. The exact procedure behindgringois best documented byKaminski \[[2023](https://arxiv.org/html/2607.13344#bib.bib996)\]\. Lines in Listings[2](https://arxiv.org/html/2607.13344#LST2)and[4](https://arxiv.org/html/2607.13344#LST4)form the output ofgringo, when it is invoked with the flag\-ton the code obtained by concatenating the lines within Listings[1](https://arxiv.org/html/2607.13344#LST1),[2](https://arxiv.org/html/2607.13344#LST2)and[3](https://arxiv.org/html/2607.13344#LST3)\. Flag\-tinstructsgringoto print output in human readable form\. Let us now discuss intuitions on which snippets of code within Listings[2](https://arxiv.org/html/2607.13344#LST2)and[3](https://arxiv.org/html/2607.13344#LST3)are relevant in producing propositional rules in Listing[4](https://arxiv.org/html/2607.13344#LST4):

- •Lines 1 through 4 are produced bygringoby relying on the facts in Listing[2](https://arxiv.org/html/2607.13344#LST2)and Lines 1 and 2 in Listing[3](https://arxiv.org/html/2607.13344#LST3)\.
- •Lines 5\-20 are produced bygringoby relying on the facts in Listing[2](https://arxiv.org/html/2607.13344#LST2); Lines 1 and 3 in Listing[4](https://arxiv.org/html/2607.13344#LST4); and Lines 4 and 5 in Listing[3](https://arxiv.org/html/2607.13344#LST3)\.
- •Lines 21\-28 are produced bygringoby relying on the fact in Line 2 in Listing[2](https://arxiv.org/html/2607.13344#LST2); Lines 5\-20 in Listing[4](https://arxiv.org/html/2607.13344#LST4)suggesting which tuples may appear inrouterelation; and Lines 7 and 8 in Listing[3](https://arxiv.org/html/2607.13344#LST3)\.
- •Lines 30\-35 are due to Line 12 in Listing[3](https://arxiv.org/html/2607.13344#LST3)and thecostrelations established in Listing[2](https://arxiv.org/html/2607.13344#LST2)and Lines 2 and 4 in Listing[4](https://arxiv.org/html/2607.13344#LST4)\.
- •Lines 30\-35 are due to Line 12 in Listing[3](https://arxiv.org/html/2607.13344#LST3)and thecostrelations established in Listing[2](https://arxiv.org/html/2607.13344#LST2)and Lines 2 and 4 in Listing[4](https://arxiv.org/html/2607.13344#LST4)\.
- •Lines 36\-53 are due to Lines 13 and 14 in Listing[3](https://arxiv.org/html/2607.13344#LST3); thecostrelations established in Listing[2](https://arxiv.org/html/2607.13344#LST2)and Lines 2 and 4 in Listing[4](https://arxiv.org/html/2607.13344#LST4); and Lines 5\-20 in Listing[4](https://arxiv.org/html/2607.13344#LST4)\.
- •Line 54 is due to Line 15 in Listing[3](https://arxiv.org/html/2607.13344#LST3); themaxCostgiven in Listing[2](https://arxiv.org/html/2607.13344#LST2); thecostrelations established in Listing[2](https://arxiv.org/html/2607.13344#LST2)and Lines 2, 4 in Listing[4](https://arxiv.org/html/2607.13344#LST4)\.

Listing 4:Part of the Grounded TS Problem with respect to TS Instance in Listing[2](https://arxiv.org/html/2607.13344#LST2)1road\(d,b\)\.road\(c,a\)\.road\(a,d\)\.

cost\(d,b,2\)\.cost\(c,a,2\)\.cost\(a,d,1\)\.

3road\(d,c\)\.road\(c,b\)\.road\(b,a\)\.

cost\(d,c,1\)\.cost\(c,b,1\)\.cost\(b,a,1\)\.

51<=\#count\{0,route\(a,b\):route\(a,b\);0,route\(a,c\):route\(a,c\);

0,route\(a,d\):route\(a,d\)\}<=1\.

71<=\#count\{0,route\(b,c\):route\(b,c\);0,route\(b,d\):route\(b,d\);

0,route\(b,a\):route\(b,a\)\}<=1\.

91<=\#count\{0,route\(c,d\):route\(c,d\);0,route\(c,a\):route\(c,a\);

0,route\(c,b\):route\(c,b\)\}<=1\.

111<=\#count\{0,route\(d,a\):route\(d,a\);0,route\(d,b\):route\(d,b\);

0,route\(d,c\):route\(d,c\)\}<=1\.

131<=\#count\{0,route\(d,a\):route\(d,a\);0,route\(c,a\):route\(c,a\);

0,route\(b,a\):route\(b,a\)\}<=1\.

151<=\#count\{0,route\(a,b\):route\(a,b\);0,route\(d,b\):route\(d,b\);

0,route\(c,b\):route\(c,b\)\}<=1\.

171<=\#count\{0,route\(b,c\):route\(b,c\);0,route\(a,c\):route\(a,c\);

0,route\(d,c\):route\(d,c\)\}<=1\.

191<=\#count\{0,route\(c,d\):route\(c,d\);0,route\(b,d\):route\(b,d\);

0,route\(a,d\):route\(a,d\)\}<=1\.

21reached\(a\)\.reached\(b\):\-route\(a,b\)\.

reached\(c\):\-route\(a,c\)\.reached\(d\):\-route\(a,d\)\.

23reached\(b\):\-route\(d,b\),reached\(d\)\.

reached\(c\):\-route\(d,c\),reached\(d\)\.

25reached\(d\):\-route\(c,d\),reached\(c\)\.

reached\(b\):\-route\(c,b\),reached\(c\)\.

27reached\(c\):\-route\(b,c\),reached\(b\)\.

reached\(d\):\-route\(b,d\),reached\(b\)\.

29:\-notreached\(b\)\.:\-notreached\(c\)\.:\-notreached\(d\)\.

&dom\{\(0;1\)\}=\(c\(a,b\)\)\.&dom\{\(0;1\)\}=\(c\(b,c\)\)\.

31&dom\{\(0;1\)\}=\(c\(c,d\)\)\.&dom\{\(0;1\)\}=\(c\(d,a\)\)\.

&dom\{\(0;2\)\}=\(c\(a,c\)\)\.&dom\{\(0;2\)\}=\(c\(b,d\)\)\.

33&dom\{\(0;2\)\}=\(c\(d,b\)\)\.&dom\{\(0;2\)\}=\(c\(c,a\)\)\.

&dom\{\(0;1\)\}=\(c\(a,d\)\)\.&dom\{\(0;1\)\}=\(c\(d,c\)\)\.

35&dom\{\(0;1\)\}=\(c\(c,b\)\)\.&dom\{\(0;1\)\}=\(c\(b,a\)\)\.

&sum\{c\(a,b\)\}=\(0\):\-notroute\(a,b\)\.

37&sum\{c\(b,c\)\}=\(0\):\-notroute\(b,c\)\.

&sum\{c\(c,d\)\}=\(0\):\-notroute\(c,d\)\.

39&sum\{c\(d,a\)\}=\(0\):\-notroute\(d,a\)\.

&sum\{c\(a,c\)\}=\(0\):\-notroute\(a,c\)\.

41&sum\{c\(b,d\)\}=\(0\):\-notroute\(b,d\)\.

&sum\{c\(d,b\)\}=\(0\):\-notroute\(d,b\)\.

43&sum\{c\(c,a\)\}=\(0\):\-notroute\(c,a\)\.

&sum\{c\(a,d\)\}=\(0\):\-notroute\(a,d\)\.

45&sum\{c\(d,c\)\}=\(0\):\-notroute\(d,c\)\.

&sum\{c\(c,b\)\}=\(0\):\-notroute\(c,b\)\.

47&sum\{c\(b,a\)\}=\(0\):\-notroute\(b,a\)\.

&sum\{c\(a,b\)\}=\(1\):\-route\(a,b\)\.&sum\{c\(b,c\)\}=\(1\):\-route\(b,c\)\.

49&sum\{c\(c,d\)\}=\(1\):\-route\(c,d\)\.&sum\{c\(d,a\)\}=\(1\):\-route\(d,a\)\.

&sum\{c\(a,c\)\}=\(2\):\-route\(a,c\)\.&sum\{c\(b,d\)\}=\(2\):\-route\(b,d\)\.

51&sum\{c\(d,b\)\}=\(2\):\-route\(d,b\)\.&sum\{c\(c,a\)\}=\(2\):\-route\(c,a\)\.

&sum\{c\(a,d\)\}=\(1\):\-route\(a,d\)\.&sum\{c\(d,c\)\}=\(1\):\-route\(d,c\)\.

53&sum\{c\(c,b\)\}=\(1\):\-route\(c,b\)\.&sum\{c\(b,a\)\}=\(1\):\-route\(b,a\)\.

:\-&sum\{c\(a,b\);c\(b,c\);c\(c,d\);c\(d,a\);c\(a,c\);c\(b,d\);

55c\(d,b\);c\(c,a\);c\(a,d\);c\(d,c\);c\(c,b\);c\(b,a\)\}\>\(4\)\.

##### How rules with&sumand ASP variables connect to CAS\(LIA\) rules

Listing[4](https://arxiv.org/html/2607.13344#LST4)provides us with the propositional rendering of CAS program encoding of our running example of the TS problem\. Let us use it to connect to the formal notions introduced in Section[2](https://arxiv.org/html/2607.13344#S2)\. Consider rules in Lines 36 and 54\-55 in Listing[4](https://arxiv.org/html/2607.13344#LST4)\. We can view these as corresponding to the following two rules written in the syntax discussed in Section[2](https://arxiv.org/html/2607.13344#S2)

∣c\(a,b\)=0∣←notroute\(a,b\)\.←∣c\(a,b\)\+c\(b,c\)\+c\(c,d\)\+c\(d,a\)\+c\(a,c\)\+c\(b,d\)\+c\(d,b\)\+c\(c,a\)\+c\(a,d\)\+c\(d,c\)\+c\(c,b\)\+c\(b,a\)\>4∣\.\\begin\{array\}\[\]\{rl\}&\\mid c\(a,b\)=0\\mid\\leftarrow not\\ route\(a,b\)\.\\\\ &\\leftarrow\\mid c\(a,b\)\+c\(b,c\)\+c\(c,d\)\+c\(d,a\)\+c\(a,c\)\+c\(b,d\)\+\\\\ &~~~~~c\(d,b\)\+c\(c,a\)\+c\(a,d\)\+c\(d,c\)\+c\(c,b\)\+c\(b,a\)\>4\\mid\.\\end\{array\}In these rules, two irregular atoms appear marked by vertical bars\. They naturally translate into LIA constraints with twelve integer constraint variables includingc​\(a,b\)c\(a,b\)andc​\(b,c\)c\(b,c\), for example\.

##### Invokingezsmtv3

A unique capability ofezsmtv3lies in the fact that it provides a frontend to distinct SMT solvers, namely,cvc4,cvc5,yices, andz3\. One may specify an SMT solver of interest at the command line\. In addition, one may specify whether single or multiple answer sets \(or extended answer sets\) are of interest\.

Let us assume the presence of the files

1. 1\.tsp\.inst– whose content is present in Listing[2](https://arxiv.org/html/2607.13344#LST2);
2. 2\.tsp\.enc– whose content is present in Listing[3](https://arxiv.org/html/2607.13344#LST3)together with an additional directive of the form\#show route/2\.This directive instructs the system to only display atoms formed with this predicate symbol in the output\.

Then, the command line

ezsmt tsp\.inst tsp\.enc \-s z3 \-e 0 \-E

produces the output given in Listing[5](https://arxiv.org/html/2607.13344#LST5)\. This output matches the solutions listed in Figure[2](https://arxiv.org/html/2607.13344#F2): Answer 1 and 2 encode Solutions 1 and 2, respectively\. Within this command line in addition to specifying files containing the program to process, we state

- •a backend SMT solver that should be used – here,z3– with\-s z3,
- •a number of answer sets that should be enumerated – here,all– with\-e 0,
- •a request to consider extended answer sets within the enumeration process\-E\.

Listing 5:ezsmtv3output for the TS sample problem\.Answer1:route\(a,d\)route\(d,c\)route\(c,b\)route\(b,a\)

c\(a,b\)=0c\(b,c\)=0c\(c,d\)=0c\(d,a\)=0c\(a,c\)=0c\(b,d\)=0

c\(d,b\)=0c\(c,a\)=0c\(a,d\)=1c\(d,c\)=1c\(c,b\)=1c\(b,a\)=1

Finishedround1in118ms

0msSMTCheckSatisfiability

16msSMTGetValues

Answer2:route\(a,b\)route\(b,c\)route\(c,d\)route\(d,a\)

c\(a,b\)=1c\(b,c\)=1c\(c,d\)=1c\(d,a\)=1c\(a,c\)=0c\(b,d\)=0

c\(d,b\)=0c\(c,a\)=0c\(a,d\)=0c\(d,c\)=0c\(c,b\)=0c\(b,a\)=0

Finishedround2in67ms

0msSMTCheckSatisfiability

35msSMTGetValues

It is due to remark that within the code base ofezsmtv3, the specifications presented in Listing[1](https://arxiv.org/html/2607.13344#LST1)are used to instructgringo\(invoked within\) on what expressions it should find syntactically valid \(Section[3\.2](https://arxiv.org/html/2607.13344#S3.SS2)narrates the details on the architecture ofezsmtv3\)\.

Let us now speak about the distinction between\-e 0and\-e 0 \-Esettings\. The former is concerned with enumerating distinct answer sets disregarding the specific values that constraint variables obtain\. The later will instructezsmtv3to enumerate distinct extended answer sets\. Let us consider a simple program presented in Listing[6](https://arxiv.org/html/2607.13344#LST6)\. Theezsmtv3system invoked with\-e 0on this sample program produces two solutions total that correspond to distinct answer sets, whileezsmtv3invoked with\-e 0 \-Eproduces three extended answer sets\.

Listing 6:Sample CAS\(LIA\)ezsmtv3program with multiple \(extended\) answer sets&dom\{1\.\.3\}=x\.

\{a\}\.

&sum\{x\}=1:\-a\.

&sum\{x\}<3:\-nota\.

#### 3\.1\.3ezsmtv3CAS\(LRA\), CAS\(LIRA\), and CAS\(IDL\) Languages

We now present the details on the encodings of the constraints supported by theezsmtv3system when it assumes the roles of CAS\(LRA\), CAS\(LIRA\), and CAS\(IDL\) solvers, respectively\.

##### The CAS\(LRA\) Language

Section[3\.1\.1](https://arxiv.org/html/2607.13344#S3.SS1.SSS1)described the CAS\(LIA\) language supported byezsmtv3\. The same section can be seen as the one describing the details of the CAS\(LRA\) language supported by the system modulo the condition that non\-integer real numbers are listed using quotation marks\. For instance, the expression of the form

&sum\{"2\.4"\*2;3\+x\+\(5\+2\)\*z\}=y\(20\)occurring within a ground CAS\(LRA\)ezsmtv3program is identified with an irregular atom

\|x−y\+7×z=−7\.8\|\|x\-y\+7\\times z=\-7\.8\|\(21\)which has a natural mapping into a respective LRA constraint with three constraint variables over reals, namely,xx,yy, andzz\. Just as we attempted to make the fragment of the CAS\(LIA\) language supported byezsmtv3compatible with theclingconlanguage, we also attempted to make the fragment of the CAS\(LRA\) language supported byezsmtv3compatible with theclingo\[LP\]Janhunenet al\.\[[2017](https://arxiv.org/html/2607.13344#bib.bib7)\]language so that a CAS\(LRA\) program written forezsmtv3can be processed byclingo\[LP\]system \(modulo omitting the directive&l​o​g​i​c​\(l​r​a\)\.\\&logic\(lra\)\.described below\)\. It is due to note that

- •clingo\[LP\]supports an additional optimization statement that is outside of the scope ofezsmtv3and
- •clingo\[LP\]is less permissive in the form of the&s​u​m\\&sumstatements it allows\. For example, the expression of the form \([20](https://arxiv.org/html/2607.13344#S3.E20)\) is considered syntactically invalid byclingo\[LP\]\. Yet, recall how this expression corresponds to irregular atom \([21](https://arxiv.org/html/2607.13344#S3.E21)\), which we could encode in the syntax understood byclingo\[LP\]as follows &sum\{x;\(\-1\)\* y;7\* z\}="\-7\.8"\.

In addition, anezsmtv3CAS\(LRA\) program may contain the following declaration

```
&logic(lra).
```

This declaration instructsezsmtv3that the program it is dealing with is CAS\(LRA\) program\. Alternatively, a flag\-l 1within the command line can be used to invokeezsmtv3instructing it to process a CAS\(LRA\) program\.

The theory specification for CAS\(LRA\) is identical to the specification in Listing[1](https://arxiv.org/html/2607.13344#LST1)modulo an additional line inserted after line 18 of that listing:

&logic/1 : var\_term, head;\(22\)This additional line allowsezsmtv3to introduce the directive&logic\(lra\)\.

##### The CAS\(LIRA\) Language

The theory specification for CAS\(LIRA\) programs required bygringois identical to the specification listed in Listing[1](https://arxiv.org/html/2607.13344#LST1)modulo two additional lines inserted after line 18 of that listing\. The first line is presented in \([22](https://arxiv.org/html/2607.13344#S3.E22)\) and the second line follows:

These two additional lines allowezsmtv3to process the directives of the following kind

&logic\(lira\)\.&type\{x; y\}=int\.\\begin\{array\}\[\]\{l\}\\hbox\{\{\\&logic\(lira\)\.\}\}\\\\ \\hbox\{\{\\&type\\\{x; y\\\}=int\.\}\}\\\\ \\end\{array\}\(23\)In this snippet of sample code, the first line declares toezsmtv3that the program it currently considers is within the CAS\(LIRA\) language; alternatively, a user may use flag\-l 2within the command line to invokeezsmtv3in such a mode\. Before we discuss the role of the second line, let us introduce a termfunctional nameof a constraint variable\. Within the programs thatezsmtv3supports a constraint variable may take one of two forms

vv​\(t1,…,tn\)\.\\begin\{array\}\[\]\{l\}v\\\\ v\(t\_\{1\},\\dots,t\_\{n\}\)\.\\end\{array\}In these expressions, we callvvafunctional nameof a constraint variable\. The sample code&type\{x; y\}=int\.states a condition that any constraint variable with functional namexxoryyoccurring in a given program is considered to be integer\. Any constraint variable occurring within a program whose functional name is missing from a declaration of this kind is considered to be a constraint variable over reals\.

For the remainder, Section[3\.1\.1](https://arxiv.org/html/2607.13344#S3.SS1.SSS1)can be seen as a section describing the details of the CAS\(LIRA\) language supported byezsmtv3modulo the condition that real numbers that are not integers are listed using quotation marks\. For instance, expression \([20](https://arxiv.org/html/2607.13344#S3.E20)\) occurring within a ground CAS\(LIRA\)ezsmtv3program that contains lines in \([23](https://arxiv.org/html/2607.13344#S3.E23)\) and no other type\-declarations is identified with an irregular atom of the form \([21](https://arxiv.org/html/2607.13344#S3.E21)\), which has a natural mapping into the respective LIRA constraint with integer constraint variablesxxandyy, and real constraint variablezz\.

##### The CAS\(IDL\) Language

The theory specification for CAS\(IDL\) programs is in Listing[7](https://arxiv.org/html/2607.13344#LST7)\. This specification allowsezsmtv3to provide support for

- •difference logic constraints of the form \([12](https://arxiv.org/html/2607.13344#S2.E12)\); and
- •the declaration This directive instructsezsmtv3that it is dealing with CAS\(IDL\) program; alternatively, a user may use flag\-l 3for the same instruction\.

Listing 7:Encoding of IDL Logic ingringoversion 5\.\#theoryidl\{

linear\_term\{

\-:2,unary;

\*:1,binary,left;

\+:0,binary,left;

\-:0,binary,left

\};

dom\_term\{

\-:3,unary;

\+:3,unary;

\*:2,binary,left;

\+:1,binary,left;

\-:1,binary,left;

\.\.:0,binary,left

\};

&dom/0:dom\_term,\{=\},linear\_term,head;

&diff/0:linear\_term,\{<=,\>=,<,\>,=,\!=\},linear\_term,any;

&logic/1:linear\_term,head

\}\.

For instance, expressions of the form

and

occurring within a ground CAS\(LRA\)ezsmtv3program are identified with irregular atoms

and

respectively\. Both of these irregular atoms have a natural mapping into respective IDL constraints\.

It is due to note that the CAS\(IDL\)ezsmtv3program is often suitable for processing with solverclingo\[DL\]\[Janhunenet al\.,[2017](https://arxiv.org/html/2607.13344#bib.bib7)\]\. Yet, the dialect of CAS\(IDL\)ezsmtv3programs permits the following expressions that are outside the language fragment ofclingo\[DL\]:

- •the&l​o​g​i​c\\&logicdirective, which specifies the IDL logic to be used within the encoding\. This directive can be eliminated from programs when proper flag is used to invokeezsmtv3\.
- •the&d​o​m\\&domspecifications for variables\. These expressions are treated in the same way as described for the case of CAS\(LIA\) fragment, and it is easy to see that the resulting SMT formulas are within the SMT\(IDL\) fragment\.clingo\[DL\]bypasses the support for this language feature\.

### 3\.2ezsmtv3Architecture

Figure[3](https://arxiv.org/html/2607.13344#F3)presents the architecture of theezsmtv3system\. This system is able to process CAS\(LIA\), CAS\(LRA\), CAS\(LIRA\), and CAS\(IDL\) utilizing the language constructs as specified in Section[3\.1](https://arxiv.org/html/2607.13344#S3.SS1)\. We start by briefly describing the system’s workings\. Then we provide details for its more complex elements\.

At first, theezsmtv3system determines which kind of program it is given – CAS\(LIA\), CAS\(LRA\), CAS\(LIRA\), or CAS\(IDL\)\. After that, it utilizes groundergringo\([Gebseret al\.](https://arxiv.org/html/2607.13344#bib.bib130),[2016](https://arxiv.org/html/2607.13344#bib.bib130);[Kaminskiet al\.](https://arxiv.org/html/2607.13344#bib.bib136),[2023](https://arxiv.org/html/2607.13344#bib.bib136)\) to eliminate ASP variables\. Systemgringoproduces a ground/propositional program in the format called Answer Set Programming Intermediate Format \(ASPIF\) \([Gebseret al\.](https://arxiv.org/html/2607.13344#bib.bib130),[2016](https://arxiv.org/html/2607.13344#bib.bib130);[Kaminskiet al\.](https://arxiv.org/html/2607.13344#bib.bib136),[2023](https://arxiv.org/html/2607.13344#bib.bib136)\)\. The grounded program written in ASPIF is then read by the Reader component of the system, which stores the rules, regular and irregular atoms from the program accordingly\. The logic interface is then set and the corresponding constraint variables are declared with specified types\. Routines of systemcmodels\(diff\)\[Shen and Lierler,[2018a](https://arxiv.org/html/2607.13344#bib.bib124)\]are used to compute completion and level rankings of the program\. Then, theezsmtv3system translates the completion augmented with level rankings into SMT formulas in the syntax of the standard SMT\-LIB language\[Barrettet al\.,[2010](https://arxiv.org/html/2607.13344#bib.bib150)\]\. These formulas are then fed into an SMT solver, which finds a model of the formulas\. Each found model corresponds to an extended answer set of the given program\. We now provide more essential details behind each sub\-component of theezsmtv3system depicted in Figure[3](https://arxiv.org/html/2607.13344#F3)\.

![Refer to caption](https://arxiv.org/html/2607.13344v1/ezsmtv3-architecture.png)Figure 3:ezsmtv3Architecture##### Thegringo5 block

Section[3\.1\.2](https://arxiv.org/html/2607.13344#S3.SS1.SSS2)used an instance of a Traveling Salesman problem formalized as CAS\(LIA\) program to illustrate the process of grounding\. Within theezsmtv3groundergringoversion 5 is utilized\. It is a sub\-component of already mentioned systemclingo 5\. Sections[3\.1\.1](https://arxiv.org/html/2607.13344#S3.SS1.SSS1)and[3\.1\.3](https://arxiv.org/html/2607.13344#S3.SS1.SSS3)highlighted the presence and importance of theory specifications – recall, Listings[1](https://arxiv.org/html/2607.13344#LST1)and[7](https://arxiv.org/html/2607.13344#LST7)– that enable us to define the syntactic constructs of various CAS languages thatgringois then able to process\. For example, the theory specification in Listing[7](https://arxiv.org/html/2607.13344#LST7)instructsgringothat atoms of the form \([24](https://arxiv.org/html/2607.13344#S3.E24)\) and/or \([25](https://arxiv.org/html/2607.13344#S3.E25)\) are valid constructs syntactically\. Given such a theory specification,gringois able to ground the respective programs and encode these using the ASPIF format \([Gebseret al\.](https://arxiv.org/html/2607.13344#bib.bib130),[2016](https://arxiv.org/html/2607.13344#bib.bib130);[Kaminskiet al\.](https://arxiv.org/html/2607.13344#bib.bib136),[2023](https://arxiv.org/html/2607.13344#bib.bib136)\)\. This format is best documented in the appendix of the extended version of the paper byGebseret al\.\[[2016](https://arxiv.org/html/2607.13344#bib.bib130)\]available at[https://www\.cs\.uni\-potsdam\.de/wv/publications/DBLP\_conf/iclp/GebserKKOSW16x\.pdf](https://www.cs.uni-potsdam.de/wv/publications/DBLP_conf/iclp/GebserKKOSW16x.pdf)\. The grounded logic program in ASPIF can be seen as a list of statements in normal form that utilize numerical values to represent program’s atoms and its internal structure\.

##### The Reader block

The ASPIF statements generated by groundergringoare interpreted by the Reader block\. The Reader block parses ASPIF statements provided bygringoand stores the information about rules, regular, irregular atoms, constraint variables into the internal data structures ofezsmtv3\.

It is due to note thatgringomay recognize some expressions that are outside of the considered syntax as valid\. For instance, in the realm of theory specification for IDL constraints presented in Listings[7](https://arxiv.org/html/2607.13344#LST7),gringowill recognize the following expression as a valid irregular atom

if it occurs within head or body of some of its rules\. Intuitively this expression maps into

that is outside the syntax of IDL constraints\. For this reason the Reader block also implements additional checks to warn the user about mistakes in the considered encodings\.

##### The Logics block

Within the Logics block ofezsmtv3, we first determine whether a given program is of kind CAS\(LIA\), CAS\(LRA\), CAS\(LIRA\), or CAS\(IDL\)\. For that purpose&l​o​g​i​c\\&logicand/or command line−l\-ldirectives are used as specified in Section[3\.1](https://arxiv.org/html/2607.13344#S3.SS1)\. In case of conflicting information between directives expressed by&l​o​g​i​c\\&logicstatement within the considered program and command line, the&l​o​g​i​c\\&logicstatement has higher precedence\. By default, in the absence of any&l​o​g​i​c\\&logicstatement or flag−l\-lin the command line the program is considered to be within the CAS\(IDL\) fragment\. Using the information about a kind of a given program,ezsmtv3is able to assign each constraint variable occurring within irregular atoms a proper domain\.

##### Thecmodels\(diff\)block

Theezsmtv3system incorporates a number of routines stemming from the answer set solver calledcmodels\(diff\)\[Shen and Lierler,[2018a](https://arxiv.org/html/2607.13344#bib.bib124)\]\. In particular, it borrows thecmodels\(diff\)code that determines whether a given program is tight, performs so called completion on a given program, computes level ranking formulas in case a formula is not tight, and clausifies the resulting formulas\. These routines are key to implementing the translation provided in the concluding part of Section[2\.3](https://arxiv.org/html/2607.13344#S2.SS3)\. Indeed, bullets 1 and 2 of that translation are captured by the process of completion and construction of level ranking formulas\. Just as in the case ofcmodels\(diff\), we can instructezsmtv3to construct different kinds of level ranking formulas using flags\-levelRanking,\-levelRankingStrong,\-SCClevelRanking, and\-SCClevelRankingStrong\. We refer the reader to the work byShen and Lierler \[[2018a](https://arxiv.org/html/2607.13344#bib.bib124)\]for more details on the different kinds of level ranking formulas supported bycmodels\(diff\)andezsmtv3\. The default behavior of systemezsmtv3is captured by\-SCClevelRanking\.

By default, we set the upper bound for a level ranking variable corresponding to an atom as the number of atoms inside the strongly connected component of the program’s dependency graph containing the corresponding atom\. A larger upper bound can also be selected using the flag\-\-all\-atoms\-upper\-boundwhich sets the upper bound as the total number of atoms inside the program\. Finally, the resulting formulas are stored in semi\-Dimacs format documented bySusman and Lierler \[[2016b](https://arxiv.org/html/2607.13344#bib.bib131)\]\.

##### The Solver Interface block

The Solver Interface block is responsible for two tasks, namely, translation and solving\. In the translation phase, the formulas in semi\-Dimacs form obtained from a previous block are transformed into the syntax of the Standard language for SMT solvers called SMT\-LIB\[Barrettet al\.,[2010](https://arxiv.org/html/2607.13344#bib.bib150)\]\. The translation procedure is in the style of the one described bySusman and Lierler \[[2016b](https://arxiv.org/html/2607.13344#bib.bib131)\]\. During this transformation, in addition to encoding the SMT formula corresponding to a given program and computed in thecmodels\(diff\)block, the declarations for the used SMT logic, propositional atoms, and constraint variables are included\.

Let us consider a simple example to illustrate transformations occurring withinezsmtv3\. Assume some CAS\(LIA\) program that contains rule \([18](https://arxiv.org/html/2607.13344#S3.E18)\), which we understand as a denial \([19](https://arxiv.org/html/2607.13344#S3.E19)\)\. Thecmodels\(diff\)block will turn this denial into a group of SMT\(LIA\) formulas, namely,

\|x−y\+7z=−7\|∨¬a∨b,\|x−y\+7z=−7\|↔x−y\+7z=−7\.\\begin\{array\}\[\]\{l\}\|x\-y\+7z=\-7\|\\vee\\neg a\\vee b,\\\\ \|x\-y\+7z=\-7\|\\leftrightarrow x\-y\+7z=\-7\.\\end\{array\}Within an SMT\-LIB code for the considered program we will find the following lines that we annotate with the comments for readability \(comments start with semicolon\):

```
; Quantifier free Linear Arithmetic: SMT(LIA) language
(set-logic QF_LIA)

; Declaration of boolean and integer variables used
(declare-fun a () Bool)
(declare-fun b () Bool)
(declare-fun x () Int)
(declare-fun y () Int)
(declare-fun z () Int)

; |EZSMT_THEORY(4)| is the name given within Ezsmtv3
; to irregular atom |x-y+7z=-7|
(declare-fun |EZSMT_THEORY(4)| () Bool)

; SMT(LIA) formulas stated above encoded in SMT-LIB
(assert (or |EZSMT_THEORY(4)| (not a) b))
(assert (= |EZSMT_THEORY(4)| (= (+ x (* (- 1) y) (* 7 z)) (- 7))))
```

Figure[1](https://arxiv.org/html/2607.13344#F1)summarized what kind of CAS programs are mapped into what kind of SMT formulas\. The table below details a logic declaration statement in SMT\-LIB format appropriate to invoke a correct solving routine for the respective SMT formula:

SMT\(LIA\)\(set\-logic QF\_LIA\)SMT\(LRA\)\(set\-logic QF\_LRA\)SMT\(IDL\)\(set\-logic QF\_IDL\)SMT\(LIRA\)\(set\-logic AUFLIRA\)
In the solving phase, an SMT solver is given an obtained SMT\-LIB theory\. The back\-and\-forth communication between the Solver Interface block and the SMT solver of choice makes it possible for the system to output multiple \(extended\) answer sets\. The command line directives can be used to provideezsmtv3with a specific number of solutions to be computed\.

All SMT solvers currently supported by theezsmtv3system, namelycvc4,cvc5,yices, andz3implement so called incremental solving\. Within incremental solving settings one may invoke an SMT solver on a theory and instruct it to compute a model; once that model is computed the SMT solver puts its computation on hold and waits for further instructions\. At that point it is possible to add more assertions to the theory already populated within the SMT solver’s data structures and ask it to look for yet another model of an updated theory\. This process can be repeated\.ezsmtv3utilizes incremental solving for computing multiple answer sets \(or extended answer sets\) by iteratively adding an assertion that is false when previously computed \(extended\) answer set holds\. Given an answer setAAof CAS programPPthe negation of the following formula

⋀a​t​o​m​a∈Aa∧⋀a​o​c​c​u​r​s​i​n​P​a​n​d​a∉A¬a\\bigwedge\_\{atom~a\\in A\}a~\\wedge~\\bigwedge\_\{a~occurs~in~P~and~a\\not\\in A\}\\neg a\(26\)forms such an assertion\. Given an extended answer set⟨A,ν⟩\\langle A,\\nu\\rangleof CAS programPP, the negation of the formula formed by the conjunction of formulas \([26](https://arxiv.org/html/2607.13344#S3.E26)\) and

⋀c​o​n​s​t​r​a​i​n​t​v​a​r​i​a​b​l​e​x​o​c​c​u​r​s​i​n​Px=ν​\(x\)\\bigwedge\_\{constraint~variable~x~occurs~in~P\}x=\\nu\(x\)forms such an assertion\.

This way of implementing enumeration of multiple \(extended\) answer sets is inspired by the enumeration done by answer set solvercmodels\(diff\)\[Shen and Lierler,[2018a](https://arxiv.org/html/2607.13344#bib.bib124), Section 5\]\. Yet, utilization of incremental mode of SMT solving is unique toezsmtv3\. Theezsmt\+system invoked SMT solvers from scratch each iteration\.

##### The SMT Solvers block

In our work, we implemented support withinezsmtv3for four SMT solvers, namely,cvc4\[Barrettet al\.,[2011](https://arxiv.org/html/2607.13344#bib.bib132)\],cvc5\[Barrettet al\.,[2021](https://arxiv.org/html/2607.13344#bib.bib133)\],yices\[Dutertre and De Moura,[2006](https://arxiv.org/html/2607.13344#bib.bib135)\], andz3\[De Moura and Bjørner,[2008](https://arxiv.org/html/2607.13344#bib.bib134)\]\. Yet, given that we use SMT\-LIB to interface these solvers it requires limited effort to implement support for any other solver supporting SMT\-LIB format\. This implementation effort mainly has to be directed towards processing output of the solvers as their output formats are not identical\.

## 4Optimizations

We now turn our attention to weak constraints/optimizations supported byezsmtv3\. It is due to note that such language constructs were out of scope for the system’s predecessorezsmt\+\. Theezsmtv3system supports the syntax of weak constraints as they are described byCalimeriet al\.\[[2020a](https://arxiv.org/html/2607.13344#bib.bib581)\]as part of the ASP\-Core2 standard language of logic programs\. Here we provide the natural extension of the semantics of these statements to the CAS programs\.

Calimeriet al\.\[[2020a](https://arxiv.org/html/2607.13344#bib.bib581)\]present the syntax of weak constraints allowing ASP variables in the context; then, grounding is used to obtain propositional program with weak constraints and the notion of an optimal answer set is defined\. Here, we present all relevant definitions using the propositional case but note thatezsmtv3provides support for non\-grounded statements that are tackled by the means of groundergringo\.

Aweak constrainthas the form

:∼a1,…,aj,notaj\+1,…,notam\[w@ℓ,t1,…,tn\],:\\sim a\_\{1\},\\dotsc,a\_\{j\},\\ not\\ a\_\{j\+1\},\\dotsc,\\ not\\ a\_\{m\}\[w@\\ell,t\_\{1\},\\dots,t\_\{n\}\],\(27\)wherem\>0m\>0anda1,…,ama\_\{1\},\\ldots,a\_\{m\}are atoms,ww\(weight\) is an integer,ℓ\\ell\(level\) is a positive integer,tit\_\{i\}\(n≥0n\\geq 0\) are symbols\. In the sequel, we abbreviate expression

:∼a1,…,aj,notaj\+1,…,notam:\\sim a\_\{1\},\\dotsc,a\_\{j\},\\ not\\ a\_\{j\+1\},\\dotsc,\\ not\\ a\_\{m\}\(28\)occurring in \([27](https://arxiv.org/html/2607.13344#S4.E27)\) asDDand identify it with the propositional formula

a1∧…∧aj∧¬aj\+1∧…∧¬am\.a\_\{1\}\\wedge\\dotsc\\wedge a\_\{j\}\\wedge\\ \\neg a\_\{j\+1\}\\wedge\\dotsc\\wedge\\ \\neg a\_\{m\}\.\(29\)We may refer to this formula as thebodyof a weak constraint\.

###### Definition 6\(Optimization program or o\-program\)

An optimization program \(or o\-program\) over vocabularyσ\\sigmais a pair\(P,W\)\(P,W\), wherePPis a CAS program overσ\\sigmaandWWis a finite set of weak constraints overσ\\sigma\. Let𝒫=\(P,W\)\\mathcal\{P\}=\(P,W\)be an optimization program over vocabularyσ\\sigma\(intuitively,PPandWWforms hard and soft fragments, respectively\)\. SetXXof atoms overσ\\sigmais an answer set of𝒫\\mathcal\{P\}when it is an answer set ofPP\.

Byλ​\(𝒫\)\{\\lambda\(\{\\mathcal\{P\}\}\)\}we denote the set of all levels associated with optimization program𝒫\\mathcal\{P\}constructed as\{ℓ∣D​\[w​@​ℓ,t1,…,tn\]∈W\}\\\{\\ell\\mid\\,D\[w@\\ell,t\_\{1\},\\dots,t\_\{n\}\]\\in W\\\}\. Given an answer setXXof o\-program𝒫\\mathcal\{P\}, we mapXXandΠ\\Pito a set of tuples as follows:

weak​\(𝒫,X\)=\{\(w​@​ℓ,t1,…,tn\)∣D​\[w​@​ℓ,t1,…,tn\]∈W​and​X⊧D\};\\text\{weak\}\(\\mathcal\{P\},X\)=\\\{\(w@\\ell,t\_\{1\},\\dots,t\_\{n\}\)\\mid D\[w@\\ell,t\_\{1\},\\dots,t\_\{n\}\]\\in W\\hbox\{ and \}X\\models D\\\};We are now ready to define a number associated with o\-program, its answer set, and a levelℓ∈λ​\(𝒫\)\\ell\\in\{\\lambda\(\{\\mathcal\{P\}\}\)\}:

𝒫ℓX=∑D​\[w​@​ℓ,t1,…,tn\]∈weak​\(𝒫,X\)w\\mathcal\{P\}\_\{\\ell\}^\{X\}=\\sum\_\{D\[w@\\ell,t\_\{1\},\\dots,t\_\{n\}\]\\in\\text\{weak\}\(\\mathcal\{P\},X\)\}\{w\}
###### Definition 7\(Optimal answer sets\)

LetXXandX′X^\{\\prime\}be answer sets of𝒫\\mathcal\{P\}\. Answer setXXis dominated byX′X^\{\\prime\}if there is some integerℓ∈λ​\(𝒫\)\\ell\\in\{\\lambda\(\{\\mathcal\{P\}\}\)\}such that

𝒫ℓX′<𝒫ℓX\\mathcal\{P\}\_\{\\ell\}^\{X^\{\\prime\}\}<\\mathcal\{P\}\_\{\\ell\}^\{X\}\(30\)and

𝒫ℓ′X′=𝒫ℓ′X\\mathcal\{P\}\_\{\\ell^\{\\prime\}\}^\{X^\{\\prime\}\}=\\mathcal\{P\}\_\{\\ell^\{\\prime\}\}^\{X\}\(31\)for all integersℓ′\>ℓ\\ell^\{\\prime\}\>\\ell\.

An answer setX∗X^\{\*\}of𝒫\\mathcal\{P\}is optimal if there is no answer setX′X^\{\\prime\}of𝒫\\mathcal\{P\}such thatX∗X^\{\*\}is dominated byX′X^\{\\prime\}\.

###### Example 7

We now exemplify the definitions of an optimization program and an optimal answer set\. Recall the CAS program constructed in Example[4](https://arxiv.org/html/2607.13344#Thmexample4)\. Let us denote it as thatP1P\_\{1\}\. An optimal answer set of o\-program

\(P1,\{:∼a\.\[−1@1\]\}\)\(P\_\{1\},\\\{:\\sim a\.~\[\-1@1\]\\\}\)\(32\)is\{a​b\}\\\{a~b\\\}; whereas program

\(P1,\{:∼a\.\[1@1\]\}\)\(P\_\{1\},\\\{:\\sim a\.~\[1@1\]\\\}\)\(33\)has two optimal answer sets\{c\}\\\{c\\\}and\{c,\|x≥12\|\}\\\{c,\|x\\geq 12\|\\\}\. An optimal answer set of another o\-program

\(P1,\{:∼a\.\[−1@1\]:∼\|x=12\|\.\[−2@1\]\}\)\\begin\{array\}\[\]\{cl\}\(P\_\{1\},&\\\{~:\\sim a\.~\[\-1@1\]\\\\ &~~~:\\sim\|x=12\|\.~\[\-2@1\]\\\}\)\\end\{array\}is\{c,\|x=12\|\}\\\{c,~~\|x=12\|\\\}\.

Let us now consider slightly more complex o\-programs\. LetW1W\_\{1\}denote the set consisting of the following weak constraints:

:∼a\.\[−1​@​1\]:∼b\.\[−1​@​1\]:∼a,b\.\[−1​@​1\]:∼c\.\[−2​@​1\]\\begin\{array\}\[\]\{ll\}:\\sim a\.&\[\-1@1\]\\\\ :\\sim b\.&\[\-1@1\]\\\\ :\\sim a,b\.&\[\-1@1\]\\\\ :\\sim c\.&\[\-2@1\]\\end\{array\}O\-program\(P1,W1\)\(P\_\{1\},W\_\{1\}\)has two optimal answer sets, namely,

\{c\}and\{c,\|x≥12\|\}\.\\\{c\\\}\\hbox\{ and \}\\\{c,\|x\\geq 12\|\\\}\.\(34\)LetW2W\_\{2\}denote the set consisting of the following weak constraints:

:∼a\.\[−1​@​1,l\]:∼b\.\[−1​@​1,m\]:∼a,b\.\[−1​@​1,n\]:∼c\.\[−2​@​1,o\]\\begin\{array\}\[\]\{ll\}:\\sim a\.&\[\-1@1,l\]\\\\ :\\sim b\.&\[\-1@1,m\]\\\\ :\\sim a,b\.&\[\-1@1,n\]\\\\ :\\sim c\.&\[\-2@1,o\]\\end\{array\}O\-program\(P1,W2\)\(P\_\{1\},W\_\{2\}\)has a unique optimal answer set

It is worth noting that an alternative syntax is frequently used by answer set programming practitioners when they expresses optimization criteria:

\#​m​i​n​i​m​i​z​e​\{w1​@​ℓ1,t11,…,t1​k1:l​i​t​s1;…;wn​@​ℓn,tn​1,…,tn​kn:l​i​t​sn\},\\\#minimize\\\{w\_\{1\}@\\ell\_\{1\},t\_\{11\},\\dots,t\_\{1\{k\_\{1\}\}\}:lits\_\{1\};~~\\dots;~~w\_\{n\}@\\ell\_\{n\},t\_\{n1\},\\dots,t\_\{n\{k\_\{n\}\}\}:lits\_\{n\}\\\},\(36\)wherek1,…,kn≥0k\_\{1\},\\dots,k\_\{n\}\\geq 0andl​i​t​silits\_\{i\}is of the forma1,…,aj,n​o​t​aj\+1,…,n​o​t​ama\_\{1\},\\dotsc,a\_\{j\},\\ not\\ a\_\{j\+1\},\\dotsc,\\ not\\ a\_\{m\}so thatm\>0m\>0anda1,…,ama\_\{1\},\\dots,a\_\{m\}are atoms\. This statement stands fornnweak constraints

:∼lits1\[w1@ℓ1t11,…,t1​k1\]…:∼litsn\[wn@ℓn,tn​1,…,tn​kn\]\.\\begin\{array\}\[\]\{l\}:\\sim lits\_\{1\}\[w\_\{1\}@\\ell\_\{1\}t\_\{11\},\\dots,t\_\{1\{k\_\{1\}\}\}\]\\\\ ~~\\dots\\\\ :\\sim lits\_\{n\}\[w\_\{n\}@\\ell\_\{n\},t\_\{n1\},\\dots,t\_\{n\{k\_\{n\}\}\}\]\.\\end\{array\}Similarly, statement

\#​m​a​x​i​m​i​z​e​\{w1​@​ℓ1,t11,…,t1​k1:l​i​t​s1;…;wn​@​ℓn,tn​1,…,tn​kn:l​i​t​sn\}\\\#maximize\\\{w\_\{1\}@\\ell\_\{1\},t\_\{11\},\\dots,t\_\{1\{k\_\{1\}\}\}:lits\_\{1\};~~\\dots;~~w\_\{n\}@\\ell\_\{n\},t\_\{n1\},\\dots,t\_\{n\{k\_\{n\}\}\}:lits\_\{n\}\\\}\(37\)stands fornnweak constraints

:∼lits1\[−w1@ℓ1t11,…,t1​k1\]…:∼litsn\[−wn@ℓn,tn​1,…,tn​kn\]\.\\begin\{array\}\[\]\{l\}:\\sim lits\_\{1\}\[\-w\_\{1\}@\\ell\_\{1\}t\_\{11\},\\dots,t\_\{1\{k\_\{1\}\}\}\]\\\\ ~~\\dots\\\\ :\\sim lits\_\{n\}\[\-w\_\{n\}@\\ell\_\{n\},t\_\{n1\},\\dots,t\_\{n\{k\_\{n\}\}\}\]\.\\end\{array\}
###### Example 8

Consider o\-program \([32](https://arxiv.org/html/2607.13344#S4.E32)\)\. The optimization requirement

:∼a\.\[−1@1\]:\\sim a\.~\[\-1@1\]of that program can be stated either as

\#​m​i​n​i​m​i​z​e​\{−1​@​1:a\}\\\#minimize\\\{\-1@1:a\\\}or as

\#​m​a​x​i​m​i​z​e​\{1​@​1:a\}\\\#maximize\\\{1@1:a\\\}SetW2W\_\{2\}of weak constraints from Example[7](https://arxiv.org/html/2607.13344#Thmexample7)can be represented as

\#​m​i​n​i​m​i​z​e​\{−1​@​1,l:a;−1​@​1,m:b;−1​@​1,n:a,b;−2​@​1,o:c\}\.\\\#minimize\\\{\-1@1,l:a;\-1@1,m:b;\-1@1,n:a,b;\-2@1,o:c\\\}\.

### 4\.1ezsmt3 implementation details

We now turn our attention to the question of how the support for optimization statements is implemented withinezsmtv3\.

We used propositional programs with weak constraints to introduce their semantics\. Yet,ezsmtv3supports weak constraints with ASP variables\. As for any other language constructs,ezsmtv3starts its processing by invoking groundergringoto produce a propositional program\. It is due to note thatgringomakes additional transformations to weak constraints so that the resulting set of weak constraints has a simpler form than discussed in the earlier section\. During this transformation auxiliary atoms are introduced into the program\. When answer sets are computed for this new program the auxiliary atoms can be safely dropped to obtain the answer sets of the original program\. The weak constraints that systemezsmtv3is exposed to beyond the point of grounding has one of the following forms

:∼a\.\[w@ℓ,t1,…,tn\]\\displaystyle:\\sim\\ a\.~\[w@\\ell,t\_\{1\},\\dots,t\_\{n\}\]\(38\):∼nota\.\[w@ℓ,t1,…,tn\]\\displaystyle:\\sim\\ not\\ a\.~\[w@\\ell,t\_\{1\},\\dots,t\_\{n\}\]\(39\)whereaais an atom\. In addition, any weak constraint that appears within a ground program produced bygringois such that the expressionw​@​ℓ,t1,…,tnw@\\ell,t\_\{1\},\\dots,t\_\{n\}appearing in that weak constraint is unique \(for example, it could be used as an identifier for this constraint in the program\)\. Let us call a program satisfying stated conditions –gringo o\-program\.

Here we avoid describing formally the procedure implemented withingringofor “normalizing” optimization statements\. Yet, we use our sample setsW1W\_\{1\}andW2W\_\{2\}of weak constrains from Example[7](https://arxiv.org/html/2607.13344#Thmexample7)to hint at its details\. SetW1W\_\{1\}will be rewritten bygringoin the following style

a​u​x1←a\.a​u​x1←b\.a​u​x1←a,b\.:∼aux1\.\[−1​@​1\]:∼c\.\[−2​@​1\]\\begin\{array\}\[\]\{ll\}aux\_\{1\}\\leftarrow a\.&\\\\ aux\_\{1\}\\leftarrow b\.&\\\\ aux\_\{1\}\\leftarrow a,b\.&\\\\ :\\sim aux\_\{1\}\.&\[\-1@1\]\\\\ :\\sim c\.&\[\-2@1\]\\end\{array\}whereas setW2W\_\{2\}will be rewritten bygringoas

a​u​x2←a,b\.:∼a\.\[−1​@​1,l\]:∼b\.\[−1​@​1,m\]:∼aux2\.\[−1​@​1,n\]:∼c\.\[−2​@​1,o\]\\begin\{array\}\[\]\{ll\}aux\_\{2\}\\leftarrow a,b\.&\\\\ :\\sim a\.&\[\-1@1,l\]\\\\ :\\sim b\.&\[\-1@1,m\]\\\\ :\\sim aux\_\{2\}\.&\[\-1@1,n\]\\\\ :\\sim c\.&\[\-2@1,o\]\\end\{array\}so thata​u​x1aux\_\{1\}anda​u​x2aux\_\{2\}are some fresh auxiliary atoms\.

In order to process o\-programs with weak constraints of the form \([38](https://arxiv.org/html/2607.13344#S4.E38)\) and \([39](https://arxiv.org/html/2607.13344#S4.E39)\),ezsmtv3relies on the transformations proposed byLierler\[[2023b](https://arxiv.org/html/2607.13344#bib.bib4),[2024](https://arxiv.org/html/2607.13344#bib.bib5)\]in the scope of so called w\-systems\. W\-systems are meant as an abstraction to encapsulate various logic\-based formalisms extended with optimization expressions\. It is due to note that the semantic characterization of optimization statements utilized byLierler\[[2023b](https://arxiv.org/html/2607.13344#bib.bib4),[2024](https://arxiv.org/html/2607.13344#bib.bib5)\]is in the tradition stemming from partial weighted MaxSat\[Fu and Malik,[2006](https://arxiv.org/html/2607.13344#bib.bib931)\]\. We restate their semantics for the case of optimization programs studied here and point at the differences\. Yet, for the case of gringo o\-programs the semantics as stated here and the one studied byLierler\[[2023b](https://arxiv.org/html/2607.13344#bib.bib4),[2024](https://arxiv.org/html/2607.13344#bib.bib5)\]coincide\. Thus, the transformations that we mentioned in the beginning of the paragraph can be safely applied\.

Let us define another number associated with o\-program𝒫\\mathcal\{P\}, its answer setXX, and a levelℓ∈λ​\(𝒫\)\\ell\\in\{\\lambda\(\{\\mathcal\{P\}\}\)\}:

𝒫X\#ℓ=∑D​\[w​@​ℓ,t1,…,tn\]∈W​and​X⊧Dw\\mathcal\{P\}\{\{\}^\{\\\#\}\}\_\{\\ell\}^\{X\}=\\sum\_\{D\[w@\\ell,t\_\{1\},\\dots,t\_\{n\}\]\\in W\\hbox\{ and \}X\\models D\}\{w\}We define a concept of pw\-dominance and pw\-optimal answer sets as in Definition[7](https://arxiv.org/html/2607.13344#Thmdefinition7)by replacing𝒫\\mathcal\{P\}with𝒫\#\\mathcal\{P\}^\{\\\#\}in equations \([30](https://arxiv.org/html/2607.13344#S4.E30)\) and \([31](https://arxiv.org/html/2607.13344#S4.E31)\)\.

###### Example 9

Let us now illustrate the difference between optimal and pw\-optimal answer sets\. Consider the CAS program denoted as\(P1,W1\)\(P\_\{1\},W\_\{1\}\)in Example[7](https://arxiv.org/html/2607.13344#Thmexample7)\. Its two optimal answer sets are listed in \([34](https://arxiv.org/html/2607.13344#S4.E34)\)\. Its unique pw\-optimal answer set is presented in \([35](https://arxiv.org/html/2607.13344#S4.E35)\)\. On the other hand, recall that \([35](https://arxiv.org/html/2607.13344#S4.E35)\) is the unique optimal answer set of o\-program\(P1,W2\)\(P\_\{1\},W\_\{2\}\)\. The same set forms the unique pw\-optimal answer sets of\(P1,W2\)\(P\_\{1\},W\_\{2\}\)\.

In the last example, when we consider o\-program\(P1,W2\)\(P\_\{1\},W\_\{2\}\), it is not by chance that its optimal and pw\-optimal answer sets coincide\. This is a consequence of a general fact captured by the following proposition\.

###### Proposition 2

For o\-program\(P,W\)\(P,W\), if the cardinality of a set

\{\(w​@​ℓ,t1,…,tn\)∣D​\[w​@​ℓ,t1,…,tn\]∈W\}\\\{\(w@\\ell,t\_\{1\},\\dots,t\_\{n\}\)\\mid D\[w@\\ell,t\_\{1\},\\dots,t\_\{n\}\]\\in W\\\}\(40\)is equal to the cardinality ofWW, then the optimal and pw\-optimal answer sets of\(P,W\)\(P,W\)coincide\.

Note how given setsW1W\_\{1\}andW2W\_\{2\}from Example[9](https://arxiv.org/html/2607.13344#Thmexample9), the sets corresponding to \([40](https://arxiv.org/html/2607.13344#S4.E40)\) follow, respectively:

\{1@1,−2@1\}\{1@1,l−1​@​1,m−1​@​1,n−2@1,0\}\\begin\{array\}\[\]\{llll\}\\\{\\\-1@1,&\-2@1\\\}&&\\\\ \\\{\\\-1@1,l&\-1@1,m&\-1@1,n&\-2@1,0\\\}\\\\ \\end\{array\}It is easy to see that any gringo o\-program satisfies the if\-condition of Proposition[2](https://arxiv.org/html/2607.13344#Thmproposition2)\.

Now that we established that transformations studied byLierler\[[2024](https://arxiv.org/html/2607.13344#bib.bib5)\]are safe for gringo o\-programs we present some details on these transformations\. First, the weak constraints are normalized so that they only contain positive weights\. Second, the weights of the weak constraints are rescaled based on the factor computed for each level while taking into account the weights of smaller levels\. As a result, newly composed weak constraints can be considered of the same level\. The first rewriting is simple\. It starts by dropping all weak constraints with0weight\. Then, any weak constraint of the form \([38](https://arxiv.org/html/2607.13344#S4.E38)\) that has a negative weightw<0w<0is replaced by the following weak constraint:

:∼nota\.\[−w@ℓ,t1,…,tn\]:\\sim\\ not\\ a\.~\[\-w@\\ell,t\_\{1\},\\dots,t\_\{n\}\]and any weak constraint of the form \([39](https://arxiv.org/html/2607.13344#S4.E39)\) that has a negative weightwwis replaced by:

:∼a\.\[−w@ℓ,t1,…,tn\]\.:\\sim\\ a\.~\[\-w@\\ell,t\_\{1\},\\dots,t\_\{n\}\]\.Note how−1​w\-1wresults in a positive integer\. The second rewriting that eliminates all the distinct levels in favor of single level11is more involved and we refer the reader to Section 5\.2 byLierler\[[2024](https://arxiv.org/html/2607.13344#bib.bib5)\]for the details on the procedure\.Lierler\[[2023b](https://arxiv.org/html/2607.13344#bib.bib4),[2024](https://arxiv.org/html/2607.13344#bib.bib5)\]illustrate that the described rewritings preserve the pw\-optimal models of the program\. Systemezsmtv3implements these rewritings\.

Upon the completion of the rewriting process, theezsmtv3deals with the collection of weight constraints of the following form

:∼a1\.\[w1@1,t11,…,t1​n1\]…:∼ak\.\[wk@1,tk​1,…,tk​nk\]:∼notak\+1\.\[wk\+1@1,tk\+11,…,tk\+1​nk\+1\]…:∼notak\+m\.\[wk\+m@1,tk\+m​1,…,tk\+m​nk\+m\]\\begin\{array\}\[\]\{l\}:\\sim\\ a\_\{1\}\.~\[w\_\{1\}@1,t\_\{11\},\\dots,t\_\{1n\_\{1\}\}\]\\\\ \\dots\\\\ :\\sim\\ a\_\{k\}\.~\[w\_\{k\}@1,t\_\{k1\},\\dots,t\_\{k\{n\_\{k\}\}\}\]\\\\ :\\sim\\ not\\ a\_\{k\+1\}\.~\[w\_\{k\+1\}@1,t\_\{\{k\+1\}1\},\\dots,t\_\{\{k\+1\}n\_\{k\+1\}\}\]\\\\ \\dots\\\\ :\\sim\\ not\\ a\_\{k\+m\}\.~\[w\_\{k\+m\}@1,t\_\{\{k\+m\}1\},\\dots,t\_\{\{k\+m\}\{n\_\{k\+m\}\}\}\]\\\\ \\end\{array\}so that all weak constraints are of the same level11and all weightsw1,…,wk,wk\+1,…,wk\+mw\_\{1\},\\dots,w\_\{k\},w\_\{k\+1\},\\dots,w\_\{k\+m\}are positive numbers\. Given the above collection of the weak constraints,ezsmtv3composes the following expression in the language of the SMT\-LIB:

\(assert\(=val\(\+\(i​t​e​a1​w1​0\)…\(i​t​e​ak​wk​0\)\(i​t​e​\(n​o​t​ak\+1\)​wk\+1​0\)…\(i​t​e​\(n​o​t​ak\+m\)​wk\+m​0\)\)\)\)\\begin\{array\}\[\]\{ll\}\(assert\\ \(=\\ val\\ \(\+&\(ite\\ a\_\{1\}\\ w\_\{1\}\\ 0\)\\\\ &\\dots\\\\ &\(ite\\ a\_\{k\}\\ w\_\{k\}\\ 0\)\\\\ &\(ite\\ \(not\\ a\_\{k\+1\}\)\\ w\_\{k\+1\}\\ 0\)\\\\ &\\dots\\\\ &\(ite\\ \(not\\ a\_\{k\+m\}\)\\ w\_\{k\+m\}\\ 0\)\\\\ &\)\)\)\\end\{array\}where variablev​a​lvalis declared as an integer and expressioniteis intuitively evaluated as an if\-then\-else statement\. Note how the introduction of integer variablev​a​lvaltranslates into the use of SMT\(LIA\) or SMT\(LIRA\) logics when the SMT solver is invoked as depicted in Figure[4](https://arxiv.org/html/2607.13344#F4)\.

It is now due to describe the iterative procedure utilized to compute optimal answer sets\. When the first answer set of a given program with weak constraints is computed, the answer is inspected to collect the valuevvof variablev​a​lval\. Then the new SMT\-LIB statement is composed

\(a​s​s​e​r​t\(<v​a​l​v\)\)\(assert\\ \(<\\ val\\ v\)\)\(41\)and the SMT solver of choice is instructed to continue its search with this new statement\. The process of inspecting for the value of variablev​a​lvaland appending the statement of the form \([41](https://arxiv.org/html/2607.13344#S4.E41)\) is repeated till we establish that the problem becomes unsatisfiable\. Systemezsmtv3implements an anytime approach for computing optimal answer sets\. In other words, it displays each found answer set to a user with the guarantee that each following answer set dominates the one presented earlier\.

Figure 4:Mapping of logics from CAS programs with weak constraints to respective SMT formulas\.

## 5Experimental Analysis

In this section, we present the results on comparing the performance of systemezsmtv3with the state\-of\-the\-art solvers such asclingcon\[Banbaraet al\.,[2017](https://arxiv.org/html/2607.13344#bib.bib128)\],clingo\[DL\]\[Janhunenet al\.,[2017](https://arxiv.org/html/2607.13344#bib.bib7)\], andclingo\[LP\]\[Janhunenet al\.,[2017](https://arxiv.org/html/2607.13344#bib.bib7)\]\. The unique part of this comparison is that all encodings used were identical for all systems involved\. This also explains the choice of systems to benchmark against\. Cited papers above present experimental comparison of stated systems with other related technologies\.

Three benchmarks, namely, Reverse Folding \(RF\), Incremental Scheduling \(IS\), and Weighted Sequence \(WS\), come from the Third Answer Set Programming Competition\[Calimeriet al\.,[2011](https://arxiv.org/html/2607.13344#bib.bib9)\]\. We obtain theclingconencoding of IS from work byBanbaraet al\.\[[2017](https://arxiv.org/html/2607.13344#bib.bib128)\]\. We include a benchmark problem called Blending \(BL\) from work byBiavaschi\[[2017](https://arxiv.org/html/2607.13344#bib.bib122)\]\. We also add a modification of this benchmark called Mixed\-BL, which contains variables over both integers and reals\. Three more benchmarks, namely, RoutingMin \(RMin\), RoutingMax \(RMax\), and Traveling Salesman \(TS\) are obtained from work byLiuet al\.\[[2012](https://arxiv.org/html/2607.13344#bib.bib103)\]\. The original TS benchmark is an optimization problem, and we turn it into a decision problem\. The original RoutingMax and RoutingMin problems are stated as CAS\(LIA\) programs\. It was possible to find a formulation of these problems using the CAS\(IDL\) language\.666Such a reformulation was suggested by Max Ostrowski\.In addition, we created another variant of the RoutingMax problem encoding by re\-formulating one of its integer linear constraints in the original encoding as an aggregate \(\#​s​u​m\\\#sum\) expression\. The Labyrinth \(LB\) benchmark is extended from the domain presented in the Fifth Answer Set Programming Competition\[Calimeriet al\.,[2016](https://arxiv.org/html/2607.13344#bib.bib10)\]\. This extension allows us to add integer linear constraints into the problem encoding\. Also, we present results on two benchmarks from work byBalducciniet al\.\[[2017](https://arxiv.org/html/2607.13344#bib.bib125)\], namely, Car and Generator \(GN\)\. It is due to remark that all encodings from the literature were inspected and when possible augmented with additional domain restrictions for their constraint variables\. This change was due to an observation that systems such asclingcontypically benefit from prespecified tighter domain on constraint variables\.

All benchmarks are run on an Ubuntu 20\.04\.6 LTS \(64\-bit\) system with an Intel® Core™ i7\-7700 CPU @ 3\.60GHz with 31\.2 GiB RAM\. The resource allocated for each benchmark instance is limited to one CPU core and 4 GiB of RAM\. We set a timeout of 1800 seconds for each instance\. Systems that we use to compare the performance of variants ofezsmtv3\(invoking SMT solvercvc4v\. 1\.8;cvc5v\. 1\.0\.8;yicesv\. 2\.6\.4;z3v\. 4\.8\.7 \) areclingconv\. 5\.2\.1,clingo\[LP\]v\. 0\.2\.0 andclingo\[DL\]v\. 1\.5\.0\. Thegringosystem v\. 5\.4\.0 is used as a grounder forezsmtv3\.

Within all presented figures, all of the steps involved, including grounding and translation, are reported as part of the total solving time\. Letterℰ\\mathcal\{E\}stands forezsmtv3;c\-constand forclingcon; andc\[DL\]stands forclingo\[DL\]\. The number in parenthesis after the name of the benchmark specifies how many instances were used in experiments\. The time reported is the cumulative time of all the instances of the particular benchmark\. The number of unsolved instances due to timeout or insufficient memory is put inside parentheses\. The cumulative time mentioned in bold font is the least time taken for that particular benchmark problem using the corresponding solvers\. The “\-” symbol is used to show that the considered solver does not support this particular encoding\. The benchmarks are divided into categories\. The acronyms T and NT in the category names indicate that the programs are tight and non\-tight, respectively\. The second part of the category name indicates the logic used to formulate the CAS encoding of the considered problems\. For non\-tight \(NT\) programs, more solving options are possible, such as the use of different level ranking formulas using flags\.Shen and Lierler\[[2018b](https://arxiv.org/html/2607.13344#bib.bib137)\]highlights the impact of the level ranking flags on the performance ofezsmt\+\. Similar impact is expected onezsmtv3\.

Before presenting individual results let us mention thatezsmtv3can be seen as a more versatile system than its mentioned peersclingcon,clingo\[DL\], andclingo\[LP\]\. Indeed,ezsmtv3supports programs of four kinds, namely, CAS\(LIA\), CAS\(IDL\), CAS\(LRA\), and CAS\(LIRA\)\. Systemsclingcon,clingo\[DL\], andclingo\[LP\]support CAS\(LIA\), CAS\(IDL\), CAS\(LRA\) programs,respectively\. This fact explains why figures that follow contain benchmark data for different subsets of systems\.

We start the discussion of the experimental analysis with the presentation of Figure[5](https://arxiv.org/html/2607.13344#F5)\. This figure is meant to illustrate the uniqueness of theezsmtv3system\. Unlike its other peer systems geared to support a specific logic,ezsmtv3implements various logics including LIRA\. Thus,ezsmtv3is capable of solving new kinds of domains\. In the future, we envision extensions of the system to more logics provided by the SMT\-solving portfolio\. Another special feature ofezsmtv3is that it can be seen as a multitude of systems\. Indeed, each SMT solver invoked by the system provides us with different computational capabilities\. Figure[5](https://arxiv.org/html/2607.13344#F5)illustrates that SMT solverscvc4andcvc5are superior toz3for the case of the considered benchmark\. The same figure does not present timings forezsmtv3invokingyices\. This is due to the fact that SMT solveryicesprovides no support for LIRA logic\.

Figure 5:Summary of Experimental Data on CAS\(LIRA\) EncodingsFigure[6](https://arxiv.org/html/2607.13344#F6)presents the comparison betweenclingo\[LP\]andezsmtv3on CAS\(LRA\) encodings available\. Figure[7](https://arxiv.org/html/2607.13344#F7)presents the comparison betweenclingconandezsmtv3on CAS\(LIA\) encodings\. It is due to note that systemclingconis a mature tool that has been under development for close to a decade, whereasclingo\[LP\]has been developed to illustrate the versatility ofclingoseries 5 that provides capabilities to bootstrap nontrivial extensions\. These figures seem to indicate that relying on SMT solvers as a backend is a viable approach\. We see howezsmtv3variants are competitive or superior with respect toclingo\[LP\]\. At the same time it is obvious that when a technology is specifically geared towards solving CAS\(LIA\) programs such asclingcon, then the efforts are paid off\. On several of the benchmarks,ezsmtv3is comparable in its performance withclingcon, but often enoughclingconexhibits superior performance\. This consistent difference may also be due to the fact that solving technology of SMT solvers works under no assumption of finite domains such as imposed by the technology behindclingcon\. Yet, when it is important to lift finite domain restrictionsezsmtv3is now an option\. Worth noting,ezsmtv3seems to weather a competition better in a realm of tight programs versus nontight\.

Figure 6:Summary of Experimental Data on CAS\(LRA\) EncodingsFigure 7:Summary of Experimental Data on CAS\(LIA\) EncodingsLast but not least we present Figure[8](https://arxiv.org/html/2607.13344#F8)that summarizes the results for CAS\(IDL\) encodings\. In the same table, we add lines from the earlier figure that showcase the results for the same problems encoded as CAS\(LIA\) programs and solved by different technologies\. This table points at the possibility to improveezsmtv3by exploring other translations of aggregate expressions \(\#​s​u​m\\\#sum, in this case\) than these currently implemented withinezsmtv3\(these routines the system inherits from answer set solvercmodels\[Giunchigliaet al\.,[2006](https://arxiv.org/html/2607.13344#bib.bib65)\]\)\. The experimental data points at the superiority of specialized propagators for processing aggregate expressions\.

CategoryBenchmarkc\-conc\[DL\]ℰ\\mathcal\{E\}\(z3\)ℰ\\mathcal\{E\}\(yices\)ℰ\\mathcal\{E\}\(cvc4\)ℰ\\mathcal\{E\}\(cvc5\)\(100\)NT\-LIARMax\(\#sum\)20\.34\-35166\.7910802\.8616754\.0010707\.14RMax\(&sum\)10\.62\-2087\.30592\.44\(100\)1743\.65NT\-IDLRMax DL\-4\.3822682\.929687\.7810620\.8516277\.06NT\-LIARMin1\.17\-95\.8191\.88110\.67107\.61NT\-IDLRMin DL\-1\.24110\.75100\.94122\.15115\.02

Figure 8:Summary of Experimental Data on Variants of Routing Problems: CAS\(IDL\) and CAS\(LIA\) encodings combined
## 6Conclusions

This paper gives a detailed account of theezsmtv3system\. A central focus of our work was the development of a robust and extensible CASP software framework which may significantly advance declarative programming and knowledge representation by offering both enhanced modeling expressiveness and access to cutting\-edge solver performance\. We aimed to emulate and expand upon the success of extensible platforms such as theclingo 5series\[Gebseret al\.,[2019](https://arxiv.org/html/2607.13344#bib.bib6)\]and the influential SAT solverminisat\[Eén and Sörensson,[2003](https://arxiv.org/html/2607.13344#bib.bib1274)\], both of which served as blueprints for designing modular, API\-driven solvers\. Also, the extensibility ofminisatled to more than a decade of impactful developments in SAT and related technologies, including its use in solvers likecmodels\[Giunchigliaet al\.,[2006](https://arxiv.org/html/2607.13344#bib.bib65)\]andminisat\(ID\)\[de Catet al\.,[2014](https://arxiv.org/html/2607.13344#bib.bib41)\]\. Similarly, the flexibility ofclingo 5enabled the rapid prototyping of new CASP solvers such asclingo\[LP\]andclingo\[DL\]\[Janhunenet al\.,[2017](https://arxiv.org/html/2607.13344#bib.bib7)\]\.

To validate our claim that theezsmtv3system is capable to support the rapid development of new CASP technologies we bootstrap four distinct CASP solvers, one that support linear integer constraints, another one that supports constraints over reals, then one that supports mixed real integer constraints and difference logic constraints\. All of these were implemented using the same streamlined methodology that we carefully document here\. One of the intentions of this description is to attract broader community involvement with theezsmtv3framework with the potential of seeing new solvers that support other logics widely used within SMT\. We focused on developing a clear and accessible interface for expressing and reasoning with different kinds of constraints\. This required the introduction of new language features, and streamlined integration with SMT solver technology via an incremental solving interface\. The experiment section articulates the validity of the approach and properly places the system among its peers\.

One more observation is due\. Theezsmtv3system can be seen as an alternative to SMT\-LIB front\-end to SMT solvers\. As such, it provides a declarative programming language based on logic programming conventions to this automated reasoning technology\. A similar idea was explored by theezscpsystem\[Balduccini and Lierler,[2017](https://arxiv.org/html/2607.13344#bib.bib27)\]in the scope of constraint satisfaction processing\. That system utilized CSP solvers to process CAS programs\. An alternative view to that work was simplifying utilization of CSP solvers by providing them with the convenient interface through declarative programming languages based on logic programming\.

As a direction for future work it is important to explore the possibility of incorporating various features supported by distinguished CASP systems\. For example, systemsclingo\[LP\]andclingo\[DL\]allow a programmer to use irregular atoms in heads of the rules\. Systemclingconsupports additional constraint types, such asall\-different, and permits stating optimization conditions over linear sums of values of constraint variables\. This direction requires deeper theoretical and practical investigation on how to incorporate such features and capabilities intoezsmtv3\.

##### Acknowledgments

We are grateful to Nicholas Wilson for his contributions to the original prototype ofezsmtv3as part of his Master Project \(thesis equivalent\) at the University of Nebraska Omaha\. We are thankful to Zachary Hansen for his assistance to build a sand\-basket forezsmtv3available on the University of Nebraska Omaha server and providing his valuable remarks on the complete draft of the paper\. Last but not least we are grateful to anonymous reviewers for taking their time to provide detailed comments on the paper\.

##### Competing interests

The author\(s\) declare none\.

## References

- M\. Balduccini and Y\. Lierler \(2017\)Constraint answer set solver ezcsp and why integration schemas matter\.Theory and Practice of Logic Programming17\(4\),pp\. 462–515\.External Links:[Document](https://dx.doi.org/10.1017/S1471068417000102)Cited by:[§1](https://arxiv.org/html/2607.13344#S1.p1.1),[§1](https://arxiv.org/html/2607.13344#S1.p2.1),[§3\.1](https://arxiv.org/html/2607.13344#S3.SS1.p1.1),[§6](https://arxiv.org/html/2607.13344#S6.p3.1)\.
- M\. Balduccini, D\. Magazzeni, M\. Maratea, and E\. C\. Leblanc \(2017\)CASP solutions for planning in hybrid domains\.Theory and Practice of Logic Programming17\(4\),pp\. 591–633\.External Links:[Document](https://dx.doi.org/10.1017/S1471068417000187)Cited by:[§5](https://arxiv.org/html/2607.13344#S5.p2.1)\.
- M\. Banbara, B\. Kaufmann, M\. Ostrowski, and T\. Schaub \(2017\)Clingcon: the next generation\.Theory and Practice of Logic Programming \(TPLP\)17\(4\),pp\. 408–461\.Cited by:[§3\.1\.1](https://arxiv.org/html/2607.13344#S3.SS1.SSS1.p2.1),[§3](https://arxiv.org/html/2607.13344#S3.p2.1),[§5](https://arxiv.org/html/2607.13344#S5.p1.1),[§5](https://arxiv.org/html/2607.13344#S5.p2.1)\.
- C\. Barrett, R\. Sebastiani, S\.A\. Seshia, and C\. Tinelli \(2008\)Satisfiability modulo theories\.InHandbook of Satisfiability,A\. Biere, M\. Heule, H\. van Maaren, and T\. Walsch \(Eds\.\),pp\. 737–797\.Cited by:[§1](https://arxiv.org/html/2607.13344#S1.p1.1)\.
- C\. Barrett, H\. Barbosa, M\. Brain, G\. Kremer, M\. Mann, A\. Mohamed, M\. Mohamed, A\. Niemetz, A\. Nötzli, A\. Ozdemir,et al\.\(2021\)CVC5 at the smt competition 2021\.Note:SMT\-COMP 2021 system descriptionExternal Links:[Link](https://smt-comp.github.io/2021/system-descriptions/cvc5.pdf)Cited by:[§1](https://arxiv.org/html/2607.13344#S1.p3.1),[§3\.2](https://arxiv.org/html/2607.13344#S3.SS2.SSS0.Px6.p1.1)\.
- C\. Barrett, C\. L\. Conway, M\. Deters, L\. Hadarean, D\. Jovanović, T\. King, A\. Reynolds, and C\. Tinelli \(2011\)Cvc4\.InComputer Aided Verification: 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14\-20, 2011\. Proceedings 23,pp\. 171–177\.Cited by:[§1](https://arxiv.org/html/2607.13344#S1.p3.1),[§3\.2](https://arxiv.org/html/2607.13344#S3.SS2.SSS0.Px6.p1.1)\.
- C\. Barrett, A\. Stump, and C\. Tinelli \(2010\)The Satisfiability Modulo Theories Library \(SMT\-LIB\)\.Note:www\.SMT\-LIB\.orgCited by:[§2\.2](https://arxiv.org/html/2607.13344#S2.SS2.p2.5),[§3\.2](https://arxiv.org/html/2607.13344#S3.SS2.SSS0.Px5.p1.1),[§3\.2](https://arxiv.org/html/2607.13344#S3.SS2.p2.1)\.
- C\. Barrett and C\. Tinelli \(2014\)Satisfiability modulo theories\.InHandbook of Model Checking,E\. Clarke, T\. Henzinger, and H\. Veith \(Eds\.\),Cited by:[§1](https://arxiv.org/html/2607.13344#S1.p1.1)\.
- M\. Bartholomew and J\. Lee \(2014\)Logics in artificial intelligence: 14th european conference, jelia 2014, funchal, madeira, portugal, september 24\-26, 2014\. proceedings\.E\. Fermé and J\. Leite \(Eds\.\),pp\. 529–542\.External Links:ISBN 978\-3\-319\-11558\-0,[Document](https://dx.doi.org/10.1007/978-3-319-11558-0%5F37),[Link](http://dx.doi.org/10.1007/978-3-319-11558-0_37)Cited by:[§1](https://arxiv.org/html/2607.13344#S1.p1.1)\.
- S\. Biavaschi \(2017\)Automated reasoning methods in hybrid systems\.Note:Annual Report of “Scuola Superiore dell’Università di Udine”Cited by:[§5](https://arxiv.org/html/2607.13344#S5.p2.1)\.
- G\. Brewka, T\. Eiter, and M\. Truszczyński \(2011\)Answer set programming at a glance\.Communications of the ACM54\(12\),pp\. 92–103\.Cited by:[§1](https://arxiv.org/html/2607.13344#S1.p1.1)\.
- F\. Calimeri, W\. Faber, M\. Gebser, G\. Ianni, R\. Kaminski, T\. Krennwallner, N\. Leone, M\. Maratea, F\. Ricca, and T\. Schaub \(2020a\)ASP\-Core\-2 input language format\.Theory And Practice Of Logic Programming20\(2\),pp\. 294–309\.External Links:[Document](https://dx.doi.org/10.1017/s1471068419000450)Cited by:[§4](https://arxiv.org/html/2607.13344#S4.p1.1),[§4](https://arxiv.org/html/2607.13344#S4.p2.1)\.
- F\. Calimeri, W\. Faber, M\. Gebser, G\. Ianni, R\. Kaminski, T\. Krennwallner, N\. Leone, M\. Maratea, F\. Ricca, and T\. Schaub \(2020b\)ASP\-Core\-2 input language format\.Theory and Practice of Logic Programming20\(2\),pp\. 294–309\.External Links:[Document](https://dx.doi.org/10.1017/S1471068419000450)Cited by:[§3\.1\.2](https://arxiv.org/html/2607.13344#S3.SS1.SSS2.p5.1)\.
- F\. Calimeri, M\. Gebser, M\. Maratea, and F\. Ricca \(2016\)Design and results of the fifth answer set programming competition\.Artif\. Intell\.231\(C\),pp\. 151–181\.Cited by:[§5](https://arxiv.org/html/2607.13344#S5.p2.1)\.
- F\. Calimeri, G\. Ianni, F\. Ricca, and et al\. \(2011\)The third answer set programming competition: preliminary report of the system competition track\.InProceedings of the International Conference on Logic Programming and Nonmonotonic Reasoning \(LPNMR\),Berlin, Heidelberg,pp\. 388–403\.Cited by:[§5](https://arxiv.org/html/2607.13344#S5.p2.1)\.
- B\. de Cat, B\. Bogaerts, M\. Bruynooghe, and M\. Denecker \(2014\)Predicate logic as a modelling language: the IDP system\.CoRRabs/1401\.6312\.External Links:[Link](http://arxiv.org/abs/1401.6312)Cited by:[§6](https://arxiv.org/html/2607.13344#S6.p1.1)\.
- L\. De Moura and N\. Bjørner \(2008\)Z3: an efficient smt solver\.InInternational conference on Tools and Algorithms for the Construction and Analysis of Systems,pp\. 337–340\.Cited by:[§1](https://arxiv.org/html/2607.13344#S1.p3.1),[§3\.2](https://arxiv.org/html/2607.13344#S3.SS2.SSS0.Px6.p1.1)\.
- B\. Demoen and V\. Lifschitz \(Eds\.\) \(2004\)Logic programming, 20th international conference, iclp 2004, saint\-malo, france, september 6\-10, 2004, proceedings\.Lecture Notes in Computer Science, Vol\.3132,Springer\-Verlag\.External Links:ISBN 3\-540\-22671\-0Cited by:[I\. Elkabani, E\. Pontelli, and T\. C\. Son \(2004\)](https://arxiv.org/html/2607.13344#bib.bib480)\.
- C\. Drescher and T\. Walsh \(2010\)A translational approach to constraint answer set solving\.Theory and Practice of Logic programming \(TPLP\)10\(4\-6\),pp\. 465–480\.Cited by:[§1](https://arxiv.org/html/2607.13344#S1.p1.1)\.
- B\. Dutertre and L\. De Moura \(2006\)The yices smt solver\.Tool paper at http://yices\. csl\. sri\. com/tool\-paper\. pdf2\(2\),pp\. 1–2\.Cited by:[§1](https://arxiv.org/html/2607.13344#S1.p3.1),[§3\.2](https://arxiv.org/html/2607.13344#S3.SS2.SSS0.Px6.p1.1)\.
- N\. Eén and N\. Sörensson \(2003\)An extensible SAT solver\.InProceedings of SAT\-2003,pp\. 502–518\.Cited by:[§6](https://arxiv.org/html/2607.13344#S6.p1.1)\.
- I\. Elkabani, E\. Pontelli, and T\. C\. Son \(2004\)Smodels with clp and its applications: a simple and effective approach to aggregates in ASP\.See[Logic programming, 20th international conference, iclp 2004, saint\-malo, france, september 6\-10, 2004, proceedings, Demoen and Lifschitz](https://arxiv.org/html/2607.13344#bib.bib481),pp\. 73–89\.Cited by:[§1](https://arxiv.org/html/2607.13344#S1.p1.1)\.
- E\. Erdem, F\. Lin, and T\. Schaub \(Eds\.\) \(2009\)Proceedings of the tenth international conference on logic programming and nonmonotonic reasoning \(lpnmr’09\)\.Lecture Notes in Artificial Intelligence, Vol\.5753,Springer\-Verlag\.Cited by:[M\. Gebser, R\. Kaminski, M\. Ostrowski, T\. Schaub, and S\. Thiele \(2009a\)](https://arxiv.org/html/2607.13344#bib.bib1288)\.
- W\. Faber, N\. Leone, and S\. Perri \(2012\)InCorrect Reasoning: Essays on Logic\-Based AI in Honor of Vladimir Lifschitz,E\. Erdem, J\. Lee, Y\. Lierler, and D\. Pearce \(Eds\.\),pp\. 247–264\.Cited by:[§3\.1\.2](https://arxiv.org/html/2607.13344#S3.SS1.SSS2.p6.1)\.
- Z\. Fu and S\. Malik \(2006\)On solving the partial max\-sat problem\.InTheory and Applications of Satisfiability Testing \- SAT 2006,A\. Biere and C\. P\. Gomes \(Eds\.\),Berlin, Heidelberg,pp\. 252–265\.External Links:ISBN 978\-3\-540\-37207\-3Cited by:[§4\.1](https://arxiv.org/html/2607.13344#S4.SS1.p4.1)\.
- M\. Gebser, R\. Kaminski, B\. Kaufmann, M\. Ostrowski, T\. Schaub, and P\. Wanko \(2016\)Theory solving made easy with clingo 5\.InTechnical Communications of the 32nd International Conference on Logic Programming \(ICLP 2016\),Cited by:[§3\.1\.1](https://arxiv.org/html/2607.13344#S3.SS1.SSS1.p2.1),[§3\.2](https://arxiv.org/html/2607.13344#S3.SS2.SSS0.Px1.p1.1),[§3\.2](https://arxiv.org/html/2607.13344#S3.SS2.p2.1),[§3](https://arxiv.org/html/2607.13344#S3.p2.1)\.
- M\. Gebser, R\. Kaminski, B\. Kaufmann, and T\. Schaub \(2019\)Multi\-shot asp solving with clingo\.Theory and Practice of Logic Programming19\(1\),pp\. 27–82\.External Links:[Document](https://dx.doi.org/10.1017/S1471068418000054)Cited by:[§1](https://arxiv.org/html/2607.13344#S1.p3.1),[§6](https://arxiv.org/html/2607.13344#S6.p1.1)\.
- M\. Gebser, R\. Kaminski, M\. Ostrowski, T\. Schaub, and S\. Thiele \(2009a\)On the input language of ASP grounderGringo\.See[Proceedings of the tenth international conference on logic programming and nonmonotonic reasoning \(lpnmr’09\), Erdemet al\.](https://arxiv.org/html/2607.13344#bib.bib1289),pp\. 502–508\.Cited by:[§1](https://arxiv.org/html/2607.13344#S1.p3.1)\.
- M\. Gebser, M\. Ostrowski, and T\. Schaub \(2009b\)Constraint answer set solving\.See[51](https://arxiv.org/html/2607.13344#bib.bib75),pp\. 235–249\.Cited by:[§1](https://arxiv.org/html/2607.13344#S1.p1.1)\.
- Gebser,Martin, R\. Kaminski, B\. Kaufmann, J\. Romero, and T\. Schaub \(2015\)Progress inclaspseries 3\.InProceedings of the Thirteenth International Conference on Logic Programming and Nonmonotonic Reasoning \(LPNMR’15\),Cited by:[§1](https://arxiv.org/html/2607.13344#S1.p3.1)\.
- E\. Giunchiglia, Y\. Lierler, and M\. Maratea \(2006\)Answer set programming based on propositional satisfiability\.Journal of Automated Reasoning36,pp\. 345–377\.Cited by:[§5](https://arxiv.org/html/2607.13344#S5.p9.1),[§6](https://arxiv.org/html/2607.13344#S6.p1.1)\.
- G\. Gutin and A\.P\. Punnen \(Eds\.\) \(2007\)The traveling salesman problem and its variations\.Springer\-Verlag\.Cited by:[§3\.1](https://arxiv.org/html/2607.13344#S3.SS1.p1.1)\.
- J\. Jaffar and M\.J\. Maher \(1994\)Constraint logic programming: a survey\.Journal of Logic Programming19\(20\),pp\. 503–581\.Cited by:[§1](https://arxiv.org/html/2607.13344#S1.p1.1)\.
- T\. Janhunen, R\. Kaminski, M\. Ostrowski, T\. Schaub, S\. Schellhorn, and P\. Wanko \(2017\)Clingo goes linear constraints over reals and integers\.CoRRabs/1707\.04053\.Cited by:[§1](https://arxiv.org/html/2607.13344#S1.p1.1),[§3\.1\.3](https://arxiv.org/html/2607.13344#S3.SS1.SSS3.Px1.p1.4),[§3\.1\.3](https://arxiv.org/html/2607.13344#S3.SS1.SSS3.Px3.p3.1),[§5](https://arxiv.org/html/2607.13344#S5.p1.1),[§6](https://arxiv.org/html/2607.13344#S6.p1.1)\.
- T\. Janhunen, G\. Liu, and I\. Niemela \(2011\)Tight integration of non\-ground answer set programming and satisfiability modulo theories\.InProceedings of the 1st Workshop on Grounding and Transformations for Theories with Variables,Cited by:[§1](https://arxiv.org/html/2607.13344#S1.p1.1)\.
- R\. Kaminski, J\. Romero, T\. Schaub, and P\. Wanko \(2023\)How to build your own asp\-based system?\!\.Theory and Practice of Logic Programming23\(1\),pp\. 299–361\.Cited by:[§1](https://arxiv.org/html/2607.13344#S1.p3.1),[§3\.2](https://arxiv.org/html/2607.13344#S3.SS2.SSS0.Px1.p1.1),[§3\.2](https://arxiv.org/html/2607.13344#S3.SS2.p2.1)\.
- R\. Kaminski \(2023\)Complex reasoning with answer set programming\.doctoralthesis,University of Potsdam\.Cited by:[§1](https://arxiv.org/html/2607.13344#S1.p3.1),[§3\.1\.2](https://arxiv.org/html/2607.13344#S3.SS1.SSS2.p6.1)\.
- E\. L\. Lawler, J\. K\. Lenstra, A\. H\. G\. R\. Kan, and D\. B\. Shmoys \(Eds\.\) \(1985\)The traveling salesman problem: a guided tour of combinatorial optimization\.Wiley\.Cited by:[§3\.1](https://arxiv.org/html/2607.13344#S3.SS1.p1.1)\.
- Y\. Lierler and B\. Susman \(2017\)On relation between constraint answer set programming and satisfiability modulo theories\.Theory and Practice of Logic Programming17\(4\),pp\. 559–590\.Cited by:[§2\.2](https://arxiv.org/html/2607.13344#S2.SS2.p1.1),[§2\.3](https://arxiv.org/html/2607.13344#S2.SS3.p4.1)\.
- Y\. Lierler \(2014\)Relating constraint answer set programming languages and algorithms\.Artificial Intelligence207C,pp\. 1–22\.Cited by:[§1](https://arxiv.org/html/2607.13344#S1.p1.1)\.
- Y\. Lierler \(2023a\)Constraint answer set programming: integrational and translational \(or smt\-based\) approaches\.Theory and Practice of Logic Programming23\(1\),pp\. 195–225\.External Links:[Document](https://dx.doi.org/10.1017/S1471068421000478)Cited by:[§2\.1](https://arxiv.org/html/2607.13344#S2.SS1.p1.1),[§3\.1](https://arxiv.org/html/2607.13344#S3.SS1.p1.1)\.
- Y\. Lierler \(2023b\)Unifying framework for optimizations in non\-boolean formalisms\.Theory Pract\. Log\. Program\.23\(6\),pp\. 1248–1280\.External Links:[Link](https://doi.org/10.1017/s1471068422000400),[Document](https://dx.doi.org/10.1017/S1471068422000400)Cited by:[§4\.1](https://arxiv.org/html/2607.13344#S4.SS1.p4.1),[§4\.1](https://arxiv.org/html/2607.13344#S4.SS1.p8.5)\.
- Y\. Lierler \(2024\)An abstract view on optimizations in propositional frameworks\.Ann\. Math\. Artif\. Intell\.92\(2\),pp\. 355–391\.External Links:[Link](https://doi.org/10.1007/s10472-023-09914-6),[Document](https://dx.doi.org/10.1007/S10472-023-09914-6)Cited by:[§4\.1](https://arxiv.org/html/2607.13344#S4.SS1.p4.1),[§4\.1](https://arxiv.org/html/2607.13344#S4.SS1.p8.2),[§4\.1](https://arxiv.org/html/2607.13344#S4.SS1.p8.5)\.
- V\. Lifschitz, L\. R\. Tang, and H\. Turner \(1999\)Nested expressions in logic programs\.Annals of Mathematics and Artificial Intelligence25,pp\. 369–389\.Cited by:[Definition 1](https://arxiv.org/html/2607.13344#Thmdefinition1.p1.2.2)\.
- G\. Liu, T\. Janhunen, and I\. Niemela \(2012\)Answer set programming via mixed integer programming\.InKnowledge Representation and Reasoning Conference,External Links:[Link](https://www.aaai.org/ocs/index.php/KR/KR12/paper/view/4516)Cited by:[§1](https://arxiv.org/html/2607.13344#S1.p1.1),[§5](https://arxiv.org/html/2607.13344#S5.p2.1)\.
- V\. Marek and M\. Truszczyński \(1999\)Stable models and an alternative logic programming paradigm\.InThe Logic Programming Paradigm: a 25\-Year Perspective,pp\. 375–398\.Cited by:[§1](https://arxiv.org/html/2607.13344#S1.p1.1)\.
- V\. S\. Mellarkod, M\. Gelfond, and Y\. Zhang \(2008\)Integrating answer set programming and constraint logic programming\.Annals of Mathematics and Artificial Intelligence53\(1\-4\),pp\. 251–287\.Cited by:[§1](https://arxiv.org/html/2607.13344#S1.p1.1)\.
- I\. Niemelä \(1999\)Logic programs with stable model semantics as a constraint programming paradigm\.Annals of Mathematics and Artificial Intelligence25,pp\. 241–273\.Cited by:[§1](https://arxiv.org/html/2607.13344#S1.p1.1)\.
- I\. Niemelä \(2008\)Stable models and difference logic\.Annals of Mathematics and Artificial Intelligence53,pp\. 313–329\.Cited by:[§2\.3](https://arxiv.org/html/2607.13344#S2.SS3.p4.1)\.
- R\. Nieuwenhuis, A\. Oliveras, and C\. Tinelli \(2006\)Solving SAT and SAT modulo theories: from an abstract Davis\-Putnam\-Logemann\-Loveland procedure to DPLL\(T\)\.Journal of the ACM53\(6\),pp\. 937–977\.Cited by:[§1](https://arxiv.org/html/2607.13344#S1.p1.1)\.
- \[51\]\(2009\)Proceedings of 25th International Conference on Logic Programming\.Springer\.Cited by:[M\. Gebser, M\. Ostrowski, and T\. Schaub \(2009b\)](https://arxiv.org/html/2607.13344#bib.bib74)\.
- F\. Rossi, P\. van Beek, and T\. Walsh \(2008\)Constraint programming\.InHandbook of Knowledge Representation,F\. van Harmelen, V\. Lifschitz, and B\. Porter \(Eds\.\),pp\. 181–212\.Cited by:[§1](https://arxiv.org/html/2607.13344#S1.p1.1)\.
- D\. Shen and Y\. Lierler \(2018a\)SMT\-based answer set solver cmodels\-diff \(system description\)\.InTechnical Communications of the 34th International Conference on Logic Programming \(ICLP 2018\),Cited by:[§3\.2](https://arxiv.org/html/2607.13344#S3.SS2.SSS0.Px4.p1.1),[§3\.2](https://arxiv.org/html/2607.13344#S3.SS2.SSS0.Px5.p6.1.1),[§3\.2](https://arxiv.org/html/2607.13344#S3.SS2.p2.1)\.
- D\. Shen and Y\. Lierler \(2018b\)SMT\-based constraint answer set solver ezsmt\+ for non\-tight programs\.InSixteenth International Conference on Principles of Knowledge Representation and Reasoning,Cited by:[§1](https://arxiv.org/html/2607.13344#S1.p1.1),[§1](https://arxiv.org/html/2607.13344#S1.p2.1),[§3](https://arxiv.org/html/2607.13344#S3.p2.1),[§5](https://arxiv.org/html/2607.13344#S5.p5.1)\.
- B\. Susman and Y\. Lierler \(2016a\)SMT\-Based Constraint Answer Set Solver EZSMT \(System Description\)\.InTechnical Communications of the 32nd International Conference on Logic Programming \(ICLP 2016\),Vol\.52,pp\. 1:1–1:15\.Cited by:[§1](https://arxiv.org/html/2607.13344#S1.p1.1),[§1](https://arxiv.org/html/2607.13344#S1.p2.1)\.
- B\. Susman and Y\. Lierler \(2016b\)SMT\-based constraint answer set solver ezsmt \(system description\)\.InTechnical Communications of the 32nd International Conference on Logic Programming \(ICLP 2016\),Cited by:[§3\.2](https://arxiv.org/html/2607.13344#S3.SS2.SSS0.Px4.p2.1),[§3\.2](https://arxiv.org/html/2607.13344#S3.SS2.SSS0.Px5.p1.1)\.
- J\. Wittocx, M\. Mariën, and M\. Denecker \(2008\)Theidpsystem: a model expansion system for an extension of classical logic\.InProceedings of Workshop on Logic and Search, Computation of Structures from Declarative Descriptions \(LaSh\),pp\. 153–165\.Note:available at[https://lirias\.kuleuven\.be/bitstream/123456789/229814/1/lash08\.pdf](https://lirias.kuleuven.be/bitstream/123456789/229814/1/lash08.pdf)Cited by:[§1](https://arxiv.org/html/2607.13344#S1.p1.1)\.