Constraint Answer Set Programming versus Satisfiability Modulo Theories

Introduction

Constraint answer set programming (CASP) [Mellarkod et al., 2008; Gebser et al., 2009; Balduccini, 2009; Lierler, 2014] is a promising research direction that integrates answer set programming (ASP), a powerful knowledge representation paradigm, with constraint processing. Typical answer set programing tools start their computation with grounding, a process that substitutes variables for passing constants in respective domains. Thus large domains often form an obstacle for classical ASP. CASP enables a mechanism to model constraints over large domains so that they are processed in a non-typical way for ASP tools by delegating their solving to constraint solver systems specifically designed to handle large and sometimes infinite-domains. CASP solvers including CLINGCON [Gebser et al., 2009] and EZCSP [Balduccini, 2009] already put CASP on the map of efficient automated reasoning tools.

Constraint answer set programming often cites itself as a related initiative to Satisfiability Modulo Theories (SMT) solving [Barrett and Tinelli, 2014]. Yet, the exact link is obscured as the terminology and concepts used in both fields differ. To add to the complexity of the picture several answer set programming modulo theories formalisms have been proposed. For instance, Liu et.al. [2012], Janhunen et.al [2011], and Lee and Meng [2013] introduced logic programs modulo linear constraints, logic programs modulo difference constraints, and ASPMT programs respectively.

In this work we attempt to unify the terminology used in CASP and SMT so that the differences and similarities of logic programs with constraints versus logic programs modulo theories become apparent. At the same time, we introduce the notion of constraint formulas, which are similar to that of logic programs with constraints. We identify a special class of SMT theories that we call "uniform". Commonly used theories in satisfiability modulo solving such as integer linear, difference logic, and linear arithmetics belong to uniform theories. This class of theories helps us to establish precise links (i) between constraint formulas and SMT formulas, and (ii) between CASP and SMT. We are able to then provide a formal description relating a family of distinct constraint answer set programming formalisms.

⇤We would like to thank Martin Brain for the discussions that lead us to undertake this research. We are also grateful to Vladimir Lifschitz, Cesare Tinelli, and Mirek Truszczynski for the conversations related to the topic of this paper.

We believe that this unified outlook allows us not only to better understand the landscape of CASP languages and systems, but also to foster new ideas for CASP solvers design as well as SMT solvers design. For example, theoretical results of this work establish the method for using SMT systems for computing answer sets of a broad class of "tight" constraint answer set programs. Similarly, CASP technology can be used to solve certain classes of SMT problems.

The outline of the paper is as follows. We start by reviewing concepts of logic programs, completion, and (input) answer sets. We then present (i) generalized constraint satisfaction problems, (ii) constraint answer set programs, and (iii) constraint formulas. Next we introduce satisfiability modulo theories and respective SMT formulas. We define a class of uniform theories and establish links between CASP and SMT. The paper concludes by relating a family of distinct constraint answer set programming formalisms.

Logic Programs, Completion, and Input Answer Sets

A vocabulary is a set of propositional symbols also called atoms. As customary, a literal is an atom a or its negation, denoted ≻a. A (propositional) logic program, denoted by ⇧, over vocabulary σ is a set of rules of the form

where a is an atom over σ or ?, and each bi, 1  i  m, is an atom in σ. We will sometime use the abbreviated form for a rule (1)

where B stands for b1↪ ▷ ▷ ▷ ↪ b`↪ not b`+1↪ ▷ ▷ ▷ ↪ not bm↪ and is also called a body. We sometimes identify B with the propositional formula b1^▷ ▷ ▷^b`^≻b`+1^▷ ▷ ▷^≻bm and note that the order of its terms is immaterial. The expression a is the head of the rule. When a is ?, we often omit it and say that the head is empty. We write hd(⇧) for the set of nonempty heads of rules in ⇧. We refer the reader to the paper by Gelfond and Lifschitz [1988] for details on the definition of an answer set.

We call a rule whose body is empty a fact. In such cases, we drop the arrow. We sometimes may identify a set X of atoms with a set of facts ¶a▷ ♣ a 2 X♦. Also, it is customary for a given vocabulary σ, to identify a set X of atoms over σ with (i) a complete and consistent set of literals over σ constructed as X[¶≻a ♣ a 2 σ∩X♦, and respectively with (ii) an assignment function or interpretation that assigns truth value true to every atom in X and false to every atom in σ ∩ X.

For a program ⇧ over vocabulary σ, the completion of ⇧ [Clark, 1978], denoted by Comp(⇧), is the set of classical formulas that consists of the implications B ! a for all rules (2) in ⇧ and the implications

for all atoms a in σ.

It is well known that for the large class of logic programs, referred to as "tight" programs, its answer sets coincide with models of its completion, as shown by Fages [1994]. Tightness is a syntactic condition on a program that can be verified by means of program's dependency graph. The dependency graph of ⇧ is the directed graph G such that (i) the vertices of G are the atoms occurring in ⇧, and (ii) for every rule (1) in ⇧ whose head is not ?, G has an edge from atom a to each atom b1↪ ▷ ▷ ▷ ↪ b`. A program is called tight if its dependency graph is acyclic.

We now introduce a generalization of a concept of an input answer set by Lierler and Truszczynski [2011]. In this work, we consider input answer sets relative to input vocabularies. We then extend the definition of completion so that we can state the result by Fages for the case of input answer sets. These concepts are essential for introducing constraint answer set programs and constraint formulas as they are defined over two disjoint vocabularies so that atoms stemming from those vocabularies "behave" differently. Input answer set semantics allows us to account for these differences.

Definition 1 For a logic program ⇧ over vocabulary σ, a set X of atoms over σ is an input answer set of ⇧ relative to vocabulary ◆ ✓ σ when X is an answer set of the program ⇧ [ ((X \ ◆) ∩ hd (⇧)).

Definition 2 For a program ⇧ over vocabulary σ, the inputcompletion of ⇧ relative to vocabulary ◆ ✓ σ, denoted by IComp(⇧↪ ◆), is defined as the set of propositional formulas (formulas in propositional logic) that consists of the implications B ! a for all rules (2) in ⇧ and the implications (3) for all atoms a occurring in (σ ∩ ◆) [ hd(⇧).

Theorem 1 For a tight program ⇧ over vocabulary σ and vocabulary ◆ ✓ σ, a set X of atoms from σ is an input answer set of ⇧ relative to ◆ if and only if X satisfies program's inputcompletion IComp(⇧↪ ◆).

Constraint Answer Set Programs

We start this section by presenting primitive constraints as defined by Marriott and Stuckey [1998, Section 1.1] using the notation convenient for our purposes. We refer to this concept as a constraint dropping the word "primitive". We use constraints to define a notion of a generalized constraint satisfaction problem that Marriott and Stuckey refer to as "constraint". We then review constraint satisfaction problems as commonly defined in artificial intelligence literature and illustrate that they are special case of generalized constraint satisfaction problems.

Constraints and Generalized Constraint Satisfaction Problem We adopt the following convention: for a function ⌫ and an element x, by x⌫ we denote the value that function ⌫ maps x to (in other words, x⌫ = ⌫(x)). A domain is a nonempty set of elements (values). A signature ⌃ is a set of variables, function symbols (or f-symbols), and predicate symbols. Function and predicate symbols are associated with a positive integer called arity. By ⌃♣v, ⌃♣r, and ⌃♣f we denote the subsets of ⌃ that contain all variables, all predicate symbols, and all f-symbols respectively.

For instance, we can define signature ⌃1 = ¶s↪ r↪ E↪ Q♦ by saying that s and r are variables, E is a predicate symbol of arity 1, and Q is a predicate symbol of arity 2. Then, ⌃1♣v = ¶s↪ r♦, ⌃1♣r = ¶E↪ Q♦, ⌃1♣f = ;.

Let D be a domain. For a set V of variables, we call a function ⌫ : V ! D a [V↪D] valuation. For a set F of fsymbols, we call a total function on F an [F↪ D] f-denotation, when it maps an n-ary f-symbol into a function Dn ! D. For a set R of predicate symbols, we call a total function on R an [R↪ D] r-denotation, when it maps an n-ary predicate symbol into an n-ary relation on D.

A table below presents definitions of sample domain D1, valuations ⌫1, ⌫2, and r-denotations ⇢1 and ⇢2.

A constraint vocabulary (c-vocabulary) is a pair [⌃↪D], where ⌃ is a signature and D is a domain. A term over a c-vocabulary [⌃↪D] is either a variable in ⌃♣v, a domain element in D, or an expression f(t1↪ ▷ ▷ ▷ ↪ tn), where f is an fsymbol of arity n in ⌃♣f and t1↪ ▷ ▷ ▷ ↪ tn are terms over [⌃↪D]

A constraint atom over a c-vocabulary [⌃↪ D] is an expression

where P is a predicate symbol from ⌃♣r of arity n and t1↪ ▷ ▷ ▷ ↪ tn are terms over [⌃↪D]. A constraint literal over a c-vocabulary [⌃↪D] is either a constraint atom (4) or an expression

where P(t1↪ ▷ ▷ ▷ ↪ tn) is a constraint atom over [⌃↪D]. For instance, expressions ≻E(s), ≻E(2), and Q(r↪ s) are constraint literals over [⌃1↪D1].

Let [⌃↪D] be a c-vocabulary, ⌫ be a [⌃♣v↪D] valuation, φ be a [⌃♣f ↪D] f-denotation, and ⇢ be a [⌃♣r↪D] r-denotation. First, we define recursively a value that valuation ⌫ assigns to a term ⌧ over [⌃↪ D] w.r.t. φ. We denote this value by ⌧ ⌫↪φ . For a term that is a variable x in ⌃♣v, x⌫↪φ = x⌫ . For a term that is a domain element d in D, d⌫↪φ is d itself. For a term ⌧ of the form f(t1↪ ▷ ▷ ▷ ↪ tn), ⌧ ⌫↪φ is defined recursively by the formula f(t1↪ ▷ ▷ ▷ ↪ tn)⌫↪φ = f φ (t⌫↪φ 1 ↪ ▷ ▷ ▷ ↪ t⌫↪φ n )▷ Second, we define what it means for valuation to be a solution of a constraint literal w.r.t. given f- and r-denotations. We say that ⌫ satisfies (is a solution to) constraint literal (4) over [⌃↪D] w.r.t. φ and ⇢ when ht⌫↪φ 1 ↪ ▷ ▷ ▷ ↪ t⌫↪φ n i 2 P ⇢ . Let R be an n-ary relation on D. By R we denote complement relation of R constructed as Dn ∩R. Valuation ⌫ satisfies (is a solution to) constraint literal of the form (5) w.r.t. φ and ⇢ when ht⌫↪φ 1 ↪ ▷ ▷ ▷ ↪ t⌫↪φ n i 2 P ⇢ ▷ For instance, valuation ⌫1 satisfies constraint literal Q(r↪ s) w.r.t. ⇢1, while valuation ⌫2 does not satisfy this constraint literal w.r.t. ⇢2 (when a signature contains no function symbols no reference to f-denotation is necessary in the definitions above).

We are now ready to define constraints, their syntax and semantics. To begin we introduce a lexicon, which is a tuple ([⌃↪D]↪ ⇢↪ φ), where [⌃↪D] is a c-vocabulary, ⇢ is [⌃♣r↪D] r-denotation, and φ is [⌃♣f ↪D] f-denotation. For a lexicon L = ([⌃↪ D]↪ ⇢↪ φ), we call any function that is [⌃♣v↪ D] valuation, a valuation over L. We will omit the last element of the tuple if the signature ⌃ of the lexicon contains no f-symbols. A constraint is defined over lexicon L = ([⌃↪ D]↪ ⇢↪ φ). Syntactically, it is a constraint literal over [⌃↪D] (lexicon L, respectively). Semantically, we say that valuation ⌫ over L satisfies (is a solution to) the constraint c when ⌫ satisfies c w.r.t. φ and ⇢. For instance, the table below presents definitions of sample lexicons L1, L2, and constraints c1, c2, c3, and c4.

a literal ≻E(2) over lexicon L2.

Valuation ⌫1 is a solution to c1, c2, c3, but not a solution to c4. Valuation ⌫2 is not a solution to c1, c2, c3, and c4. In fact, constraint c4 has no solutions. We sometimes omit the explicit mention of the lexicon when talking about constraints: we then may identify a constraint with its syntactic form of a constraint literal.

Definition 3 A generalized constraint satisfaction problem (GCSP) C is a finite set of constraints over a lexicon L = ([⌃↪D]↪ ⇢↪ φ). We say that a valuation ⌫ over L satisfies (is a solution to) GCSP C when ⌫ is a solution to every constraint in C.

For example, any subset of set ¶c2↪ c3↪ c4♦ of constraints forms a GCSP.

From GCSP to Constraint Satisfaction Problem We say that a lexicon is finite-domain if it is defined over a cvocabulary that refers to a domain whose set of elements is finite. Trivially, lexicons L1 and L2 are finite-domain. Consider a special case of a constraint of the form (4) over finitedomain lexicon L = ([⌃↪D]↪ ⇢) so that each ti is a variable. (For instance, constraints c1, c2, and c3 satisfy the stated requirements, while c4 does not.) In this case, we can syntactically identify (4) with the pair

A constraint satisfaction problem (CSP) is a set of pairs (6), where ⌃♣v and D of the finite-domain lexicon L are called variables and domain of CSP, respectively. Saying that valuation ⌫ over L satisfies (4) is the same as saying that ht⌫1 ↪ ▷ ▷ ▷ ↪ t⌫n i 2 P ⇢ ▷ The latter is the way in which a solution to expressions (6) in CSP is typically defined. As in the definition of semantics of GCSP, a valuation is a solution to a CSP problem C when it is a solution to every pair (6) in C. In conclusion, GCSP generalizes CSP by (i) elevating the restriction of finite-domain, and (ii) allowing us more elaborate syntactic expressions (e.g., recall f-symbols).

Constraint Answer Set Programs and Constraint Formulas Let σr and σi be two disjoint vocabularies. We refer to their elements as regular and irregular atoms respectively. For a program ⇧, by At (⇧) we denote the set of atoms occurring in it. Similarly, for a propositional formula F, by At(F) we denote the set of its atoms.

Definition 4 A constraint answer set program (CAS program) over the vocabulary σ = σr [ σi is a triple h⇧↪ B↪ γi, where ⇧ is a logic program over the vocabulary σ such that hd(⇧) \ σi = ;, B is a set of constraints over the same lexicon, and γ is an injective function from the set σi of irregular atoms to the set B of constraints.

• ÷ X ✓ At(⇧)

For a CAS program P = h⇧↪ B↪ γi over the vocabulary σ = σr [ σi so that L is the lexicon of the constraints in B, a set X ✓ σ is an answer set of P if

• ÷ X is an input answer set of ⇧ relative to σi, and

• ÷ the following GCSP over L has a solution

Note that ≻γ(a) may result in expression of the form ≻≻P(t1↪ ▷ ▷ ▷ ↪ tn) that we identify with P(t1↪ ▷ ▷ ▷ ↪ tn). (We use this convention across the paper.)

These definitions are generalizations of CAS programs introduced by Gebser et al. [2009] as they refer to the concept of GCSP in place of CSP in the original definition.

Just as we defined constraint answer set programs, we can define constraint formulas.

Definition 5 A constraint formula over the vocabulary σ = σr [ σi is a triple hF↪ B↪ γi, where F is a propositional formula over the vocabulary σ, B is a set of constraints over the same lexicon, and γ is an injective function from the set σi of irregular atoms to the set B of constraints.

For a constraint formula F = hF↪ B↪ γi over the vocabulary σ = σr [ σi so that L is the lexicon of the constraints in B, a set X ✓ σ is a model of F if

• ÷ X ✓ At(F)
• ÷ the following GCSP over L has a solution
• ÷ X is a model of F, and

Following theorem captures a relation between CAS programs and constraint formulas.

Theorem 2 For a CAS program P = h⇧↪ B↪ γi over the vocabulary σ = σr [ σi and a set X of atoms over σ, when ⇧ is tight, X is an answer set of P if and only if X is a model of constraint formula hIComp(⇧↪ σi)↪ B↪ γi over σ = σr [ σi.

Satisfiability Modulo Theories versus Constraint Formulas

First, in this section we introduce the notion of a "theory" in Satisfiability Modulo Theories (SMT) [Barrett and Tinelli, 2014]. Second, we present the definition of a "restriction formula" and state the conditions under which such formulas are satisfied by a given interpretation. These formulas are syntactically restricted classical ground predicate logic formulas. The presented notions of interpretation and satisfaction are usual, but are stated in terms convenient for our purposes. This facilitates uncovering the precise link between CASPlike formalisms and SMT-like formalisms. We note that in literature on SMT, the term "object constant" or "function symbol of arity 0" is commonly used to refer to elements in the signature that we call variables.

An interpretation I for a signature ⌃, or ⌃-interpretation, is a tuple (D↪ ⌫↪ ⇢↪ φ) where

• ÷ D is a domain,
• ÷ ⇢ is a [⌃♣r↪D] r-denotation, and
• ÷ ⌫ is a [⌃♣v↪D] valuation,
• ÷ φ is a [⌃♣f ↪D] f-denotation.

For signatures that contains no f-symbols, we omit the reference to the last element of the interpretation tuple.

For a signature ⌃, a ⌃-theory is a set of interpretations over ⌃. For instance, for signature ⌃1, by I1 and I2 we denote the following sample interpretations (D1↪ ⌫1↪ ⇢1) and (D1↪ ⌫2↪ ⇢1) respectively. Any subset of interpretations ¶I1↪ I2♦ exemplifies a unique ⌃1-theory.

A restriction formula over signature ⌃ is a finite set of constraint literals over c-vocabulary [⌃↪ ;]. Consider a ⌃- interpretation I = (D↪ ⌫↪ ⇢↪ φ). To each term ⌧ over a cvocabulary [⌃↪ ;], I assigns a value ⌧ ⌫↪φ that we denote by ⌧ I . We say that I satisfies restriction formula Φ over ⌃ when ⌫ satisfies every constraint literal in Φ w.r.t. φ and ⇢. For instance, a sample restriction formula over ⌃1 follows

Interpretation I2 satisfies this formula, while I1 does not.

We say that a restriction formula Φ over signature ⌃ is satisfiable in a ⌃-theory T, or is T-satisfiable, when there is an element of the set T that satisfies Φ. For example, restriction formula (7) is satisfiable in any ⌃1-theory that contains interpretation I2. On the other hand, restriction formula (7) is not satisfiable in ⌃1-theory ¶I1♦.

SMT and ASPT Programs We now introduce SMT formulas that merge the concepts of propositional formulas and ⌃-theories. Then, we present ASPT programs that merge the concepts of logic programs and ⌃-theories.

Definition 6 An SMT formula P over vocabulary σ = σr [ σi is a triple hF↪ T↪ θi, where F is a propositional formula over σ, T is a ⌃-theory, and θ is an injective function from irregular atoms σi to constraint literals over c-vocabulary [⌃↪ ;].

For an SMT formula hF↪ T↪ θi over σ, a set X ✓ σ is its model if

• ÷ X ✓ At(F),
• ÷ the following restriction formula
• ÷ X is a model of F, and

is satisfiable in ⌃-theory T .

In the literature on SMT, a more sophisticated syntax than SMT formulas provide is typically discussed. Yet, SMT solvers often rely on the so called propositional abstractions of predicate logic formulas [Barrett and Tinelli, 2014, Section 1.1], which, in their most commonly used case, coincide with SMT formulas discussed here.

Definition 7 A logic program modulo theories or ASPT program P over vocabulary σ = σr [ σi is a triple h⇧↪ T↪ θi, where ⇧ is a logic program over σ, T is a ⌃-theory. and θ is an injective function from irregular atoms σi to constraint literals over c-vocabulary [⌃↪ ;].

For an ASPT program h⇧↪ T↪ θi over σ, a set X ✓ σ is its model if

• ÷ X ✓ At(⇧),
• ÷ the following restriction formula
• ÷ X is an input answer set of ⇧ relative to σi, and

is satisfiable in ⌃-theory T .

Uniform Theories The presented definition of a ⌃-theory places no restrictions on the domains, r-denotations, or fdenotations being identical across the interpretations defining a theory. In practice, such restrictions are very common in SMT. We now define so called "uniform" theories that follow these typical restrictions. We will then show how restriction formulas interpreted over uniform theories can practically be seen as syntactic variants of GCSPs. This connection brings us to a straightforward relation between SMT formulas over uniform theories and constraint formulas as well as between CAS programs and ASPT programs. In the following section, we list several common SMT fragments such as satisfiability modulo difference logic and satisfiability modulo linear arithmetic whose theories are, in fact, uniform theories. We then use these findings to relate several ASP modulo theories approaches such as ASP(DL) introduced in [Liu et al., 2012] and ASP(LC) introduced in [Liu et al., 2012] to CASP approaches.

Definition 8 For a signature ⌃, we call a ⌃-theory T uniform over lexicon L = ([⌃↪ D]↪ ⇢↪ φ) when (i) all interpretations in T are of the form (D↪ ⌫↪ ⇢↪ φ) (note how valuation ⌫ is the only not fixed element in the interpretations), and (ii) for every possible [⌃♣v↪D] valuation ⌫, there is an interpretation (D↪ ⌫↪ ⇢↪ φ) in T .

To illustrate a concept of a uniform theory, a table below defines sample domain D2, valuations ⌫3 and ⌫4, and r-denotation ⇢3.

Valuations ⌫1 and ⌫2 can be seen not only as [⌃1♣v↪ D1] valuations but also as [⌃1♣v↪D2] valuations. The set

of ⌃1 interpretations is an example of a uniform theory over lexicon ([⌃1↪D2]↪ ⇢3). We denote this theory by T1. On the other hand, the set

of ⌃1 interpretations is an example of a non-uniform theory. Indeed, the condition (i) of Definition 8 does not hold for this theory: the last interpretation refers to a different domain than the others. Also, neither of ⌃1-theories ¶I1♦, ¶I1↪ I2♦ is uniform over lexicon ([⌃1↪D1]↪ ⇢1). In this case, the condition (ii) of Definition 8 does not hold.

It is easy to see that for uniform theories we can identify their interpretations of the form (D↪ ⌫↪ ⇢↪ φ) with their second element valuation ⌫. The other three elements are fixed by the lexicon over which the uniform theory is defined. In the following we will sometimes use this convention. For example, we may refer to interpretation (D2↪ ⌫1↪ ⇢3) of uniform theory T1 as ⌫1.

For uniform ⌃-theory T over lexicon ([⌃↪ D]↪ ⇢↪ φ) we can extend the syntax of restriction formulas by saying that a restriction formula is defined over c-vocabulary [⌃↪D] as a finite set of constraint literals over [⌃↪D] (earlier we considered constraint literals over [⌃↪ ;]). The earlier definition of semantics is still applicable. In the following for the uniform theories we assume such a more general syntax. Similarly, we can extend the definition of SMT formula given a constraint ⌃-theory T over lexicon ([⌃↪D]↪ ⇢↪ φ) as follows: an SMT formula P over vocabulary σ = σr [ σi is a triple hF↪ T↪ θi, where F is a propositional formula over σ, T is a ⌃-theory, and θ is an injective function from irregular atoms σi to constraint literals over c-vocabulary [⌃↪ D]. Note how θ-mapping refers do the domain of lexicon now in place of an empty set in the earlier definition. The definition of ASPT program can be extended in the same style. For the case of uniform theories we will assume the definition of SMT formulas as stated in this paragraph. The same applies to the case of ASPT programs modulo uniform theories.

We now present a theorem that makes the connection between GCSPs over some lexicon L and restriction formulas interpreted using the uniform theory T over the same lexicon L apparent: the question whether a given GCSP over L has a solution translates into the question whether the set of constraint literals of GCSP forming a restriction formula is T -satisfiable. Furthermore, any solution to such GCSP is also an interpretation in T that satisfies the respective restriction formula, and the other way around. We then relate SMT formulas "modulo uniform theories" and constraint formulas, as well as ASPT programs and CAS programs.

Theorem 3 For a lexicon L = ([⌃↪D]↪ ⇢↪ φ), a set Φ of constraint literals over c-vocabulary [⌃↪D], a uniform ⌃- theory T over lexicon L, the following holds

1. for any [⌃♣v↪D] valuation ⌫, there is an interpretation ⌫ in T ,
2. [⌃♣v↪D] valuation ⌫ is a solution to GCSP Φ over lexicon L if and only if interpretation ⌫ in T satisfies restriction formula Φ.
3. GCSP Φ over lexicon L has a solution if and only if restriction formula Φ is T -satisfiable.

Let L denote a lexicon ([⌃↪ D]↪ ⇢↪ φ). By BL we denote the set of all constraints over L. By TL we denote the uniform ⌃-theory over L.

Theorem 4 For a lexicon L = ([⌃↪D]↪ ⇢↪ φ), a vocabulary σ = σr [σi, and a set X of atoms over σ, set X is a model of SMT formula hF↪ TL↪ θi over σ if and only if X is a model of a constraint formula hF↪ BL↪ θi over σ (where θ is identified with the function from irregular atoms to constraints over L in a trivial way.)

This theorem illustrates that for uniform theories the language of SMT formulas and constraint formulas coincide. Or, that the language of constraint formulas is a special case of SMT formulas that are defined over uniform theories. We now show similar relation between CAS and ASPT programs.

Theorem 5 For a lexicon L = ([⌃↪D]↪ ⇢↪ φ), a vocabulary σ = σr [σi, and a set X of atoms over σ, set X is a model of ASPT program h⇧↪ TL↪ θi over σ if and only if X is a model of a CAS formula h⇧↪ BL↪ θi over σ.

SMT and CASP Connection

This section starts by introducing numeric signatures and lexicons, and particular uniform theories. These definitions allow us to precisely define the languages used by various constraint answer set solvers. We conclude with the discussion of the variety of solving techniques used in logic programming community.

Let Z and R denote the sets of integers and real numbers respectively. We say that a signature is numeric when it satisfies the following requirements (i) its only f-symbols are +, ⇥ of arity 2, and (ii) its only predicate symbols are <, >, , ≥, =, 6= of arity 2. We use the symbol A to denote a numeric signature. Let φZ and ⇢Z be [¶+↪⇥♦↪ Z] fdenotation and [¶<↪>↪↪≥↪=↪6=♦↪ Z] r-denotation respectively, where they map their function and predicate symbols into usual arithmetic operations and relations over integers. We call any lexicon of the form ([A↪ Z]↪ ⇢Z↪ φZ) integer. Similarly, φR and ⇢R denote [¶+↪ ⇥♦↪ R] f-denotation and

[¶<↪ >↪ ↪ ≥↪ =↪ 6=♦↪ R] r-denotation respectively, where they map their function and predicate symbols into usual arithmetic operations and relations over reals. We call any lexicon of the form ([A↪ R]↪ ⇢R↪ φR) numeric.

Such commonly used theories in SMT as linear real arithmetic, linear integer arithmetic, and integer difference logic are uniform. To be more precise, linear real arithmetic is an example of a uniform theory over a numeric lexicon. This arithmetic poses syntactic conditions on restriction formulas that it interprets. Namely, literals in these restriction formulas must correspond to linear constraints. Similarly, linear integer arithmetic and integer difference logic are examples of uniform theories over integer lexicons. Literals in restriction formulas in these arithmetics must correspond to integer linear constraints. Furthermore, the difference logic is a special case of integer linear arithmetic posing yet additional syntactic restrictions [Nieuwenhuis and Oliveras, 2005].

We call any ASPT program h⇧↪ T↪ θi over σr [ σi

• ÷ an ASPT(L) program if T is the uniform theory over a numeric lexicon and θ maps irregular atoms σi into linear constraints.
• ÷ an ASPT(IL) program if T is the uniform theory over an integer lexicon and θ maps irregular atoms σi into integer linear constraints.
• ÷ an ASPT(DL) program if T is the uniform theory over an integer lexicon and θ maps irregular atoms σi into difference logic constraints.

In the same style, we can define SMT(L), SMT(IL), and SMT(DL) formulas.

From Theorem 5, CAS programs of the form h⇧↪ B⇤L↪ γi, where L is a numeric lexicon and B⇤L is the set of all linear constraints over L, are essentially the same objects as ASPT(L) programs. Similarly, it follows that CAS programs of the form h⇧↪ B⇤L↪ γi, where L is an integer lexicon and B⇤L is the set of all integer linear constraints over L, are essentially the same objects as ASPT(IL) programs.

Obviously, Theorems 2 and 4 pave the way for using SMT systems that solve SMT(L) and SMT(IL) problems as is for solving tight ASPT(L) and ASPT(IL) programs respectively. It is sufficient to compute the input completion of the program relative to irregular atoms. This observation has been utilized in work by Lee and Meng [2013] and Janhunen et al. [2011]. Furthermore, Janhunen et al. propose a translation of ASPT(DL) programs into SMT(DL) formulas. System DINGO utilizes this translation by invoking SMT solver Z3 for finding models for ASPT(DL) programs. It is a direction of future work to generalize these results to arbitrary theories.

Outlook on Constraint Answer Set Solvers Table 1 presents the landscape of current constraint answer set solvers using the unified terminology of this section. The star ⇤ annotating language ASPT(IL) denotes that the solver supporting this language requires the specification of finite ranges for its variables (since finite-domain constraint solvers are used as underlying solving technology).

At a high-level abstraction, one may summarize the architectures of the CLINGCON and EZCSP solvers as ASPbased solvers plus theory solver. Given a CAS program h⇧↪ B↪ γi, both CLINGCON and EZCSP first use an answer set solver to compute an input answer set of ⇧. Second, they contact a theory solver to verify whether respective constraint satisfaction problem has a solution. In case of CLINGCON, finite domain constraint solver GECODE is used as a theory solver. System EZCSP uses constraint logic programming tools such as BPROLOG [Zhou, 2012], SICSTUS PROLOG [Carlsson and Fruehwirth, 2014], and SWI PROLOG [Wielemaker et al., 2012]. These tools provide EZCSP with the ability to work with three different kinds of constraints: finite-domain integer, integer-linear, and linear constraints. To process ASPT(L) programs, the solver MINGO translates these programs into mixed integer programming expressions and then uses the solver CPLEX [IBM, 2009] to solve these formulas. To process ASPT(DL) programs DINGO translates these programs into SMT(DL) formulas and applies the SMT solver Z3 [De Moura and Bjørner, 2008] to find their models.

The diversity of solving approaches used in CASP paradigms suggests that solutions of the kind are available for SMT technology. Typical SMT architecture is in a style of systems CLINGON and EZCSP. At a high-level abstraction, one may summarize common architectures of SMT solvers as satisfiability-based solvers augmented with theory solvers. Theory solvers are typically implemented within an SMT solver and are as such custom solutions. The fact that CLINGON and EZCSP use tools available from the constraint programming community suggests that these tools could be of use in SMT community also. The solution exhibited by system MINGO, where mixed integer programming is used for solving ASPT(L) programs, hints that a similar strategy can be implemented for solving SMT(L) formulas. These ideas have recently been explored in [King et al., 2014].

Conclusions

In this paper we unified the terminology stemming from the fields of CASP and SMT solving. This unification helped us identify the special class of so called uniform theories widely used in SMT practice. Given such theories, CASP and SMT solving share more in common than meets the eye. We expect this work to be a strong building block that will bolster the cross-fertilization between three different, even if related, automated reasoning communities: CASP, constraint (satisfaction processing) programming, and SMT. In the future, we would like to investigate a similar link to a related formalism of HEX-programs [Eiter et al., 2012].