On Relation between Constraint Answer Set Programming and Satisfiability Modulo Theories

TL;DR

This paper establishes a precise formal connection between constraint answer set programming and satisfiability modulo theories, enabling the use of SMT solvers for answer set computation.

Contribution

It provides a formal translation from constraint answer set programs with linear constraints to SMT, bridging the two fields and fostering cross-disciplinary advancements.

Findings

Formal relation between constraint answer set programming and SMT established

Translation enables use of SMT solvers for answer set computation

Facilitates cross-fertilization of theoretical and practical methods

Abstract

Constraint answer set programming is a promising research direction that integrates answer set programming with constraint processing. It is often informally related to the field of satisfiability modulo theories. Yet, the exact formal link is obscured as the terminology and concepts used in these two research areas differ. In this paper, we connect these two research areas by uncovering the precise formal relation between them. We believe that this work will booster the cross-fertilization of the theoretical foundations and the existing solving methods in both areas. As a step in this direction we provide a translation from constraint answer set programs with integer linear constraints to satisfiability modulo linear integer arithmetic that paves the way to utilizing modern satisfiability modulo theories solvers for computing answer sets of constraint answer set programs.

Tables

Table 1. Table 1: Example definitions for signature, valuation, and r-denotation

${\Sigma }_1$	$\{s,r,E,Q\}$
$D_1$	$\{1,2,3\}$
${\nu }_1$	$[\Sigma _1^{}{}_{|v}{}^{},D_1]$ valuation, where $s^{{\nu }_1}=1$ and $r^{{\nu }_1}=1$
${\nu }_2$	$[\Sigma _1^{}{}_{|v}{}^{},D_1]$ valuation, where $s^{{\nu }_2}=2$ and $r^{{\nu }_2}=1$
${\rho }_1$	$[\Sigma _1^{}{}_{|r}{}^{},D_1]$ r-denotation, where $E^{{\rho }_1}=\left\{⟨1⟩\right\},Q^{{\rho }_1}=\{⟨1,1⟩,⟨2,2⟩,⟨3,3⟩\}$
${\rho }_2$	$[\Sigma _1^{}{}_{|r}{}^{},D_1]$ r-denotation, where $E^{{\rho }_2}=\{⟨2⟩,⟨3⟩\}$, $Q^{{\rho }_2}=Q^{{\rho }_1}$.

Table 2. Table 2: Sample lexicons and constraints

${ℒ}_1$	$([{\Sigma }_1,D_1],{\rho }_1)$
${ℒ}_2$	$([{\Sigma }_1,D_1],{\rho }_2)$
$c_1$	a literal $Q(r,s)$ over lexicon ${ℒ}_1$
$c_2$	a literal $Q(r,s)$ over lexicon ${ℒ}_2$
$c_3$	a literal $\neg E\left(s\right)$ over lexicon ${ℒ}_2$
$c_4$	a literal $\neg E\left(2\right)$ over lexicon ${ℒ}_2$.

Table 3. Table 3: Solvers Categorization

Solver	Language
clingcon Gebser et al. (2009)	ASPT(IL)∗
mingo Liu et al. (2012)	ASPT(IL)†
	ASPT(L)†
dingo Janhunen et al. (2011)	ASPT(DL)
ezcsp Balduccini (2009)	ASPT(IL)∗
	ASPT(IL)
	ASPT(L)
ezsmt Susman and Lierler (2016)	ASPT(IL)
	ASPT(L)

Equations

$$\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}$$

$$\begin{array}[]{l}a\leftarrow B\end{array}$$

$$b_1\wedge \dots \wedge b_{\ell }\wedge \neg b_{\ell +1}\wedge \dots \wedge \neg b_m\wedge \neg \neg b_{m+1}\wedge \dots \wedge \neg \neg b_n\to a$$

$$b_1\wedge \dots \wedge b_{\ell }\wedge \neg b_{\ell +1}\wedge \dots \wedge \neg b_m\wedge \neg \neg b_{m+1}\wedge \dots \wedge \neg \neg b_n.$$

$$b_1\wedge \dots \wedge b_{\ell }$$

$$\begin{array}[]{l}\{switch\}.\\ lightOn\leftarrow\ switch,not\ am.\\ \leftarrow not\ lightOn.\\ \{am\}.\\ \end{array}$$

$$\begin{array}[]{l}switch\leftarrow not\ not\ switch.\\ am\leftarrow not\ not\ am.\end{array}$$

$$\begin{array}[]{l}switch.\\ lightOn\leftarrow\ switch.\\ \end{array}$$

$$a\to \underset{a\leftarrow B\in \Pi }{\bigvee }B$$

$$\begin{array}[]{l}\neg\neg switch\rightarrow switch,\\ switch\wedge\neg am\rightarrow lightOn,\\ \neg lightOn\rightarrow\bot,\\ \neg\neg am\rightarrow am,\\ switch\rightarrow\neg\neg switch,\\ lightOn\rightarrow switch\wedge\neg am,\\ am\rightarrow\neg\neg am.\\ \end{array}$$

$$\begin{array}[]{l}lightOn\leftrightarrow switch\wedge\neg am,\\ lightOn.\\ \end{array}$$

$$T_{\Pi }(I)=\{a\mid a\leftarrow B\in \Pi ,IsatisfiesB\}.$$

$$T_{\Pi }\uparrow 0=\varnothing$$

$$T_{\Pi }\uparrow (i+1)=T_{\Pi }(T_{\Pi }\uparrow i)$$

$$P(t_1,\dots ,t_n),$$

$$\neg P(t_1,\dots ,t_n),$$

$$\neg E(s),\neg E(2),Q(r,s)$$

$$f(t_1,\dots ,t_n{)}^{\nu ,\varphi }=f^{\varphi }(t_1^{\nu ,\varphi },\dots ,t_n^{\nu ,\varphi }).$$

$$⟨(t_1,\dots ,t_n),P^{\rho }⟩.$$

$$a_1{x}_1+\cdots +a_n{x}_n,$$

$$+(\times (a_1,x_1),+(\times (a_2,x_2),\cdots +(\times (a_{n-1},x_{n-1}),\times (a_n,x_n))\dots ),$$

$$\bowtie (e,k)$$

$$\Pi \cup (X\cap \iota ).$$

$$\begin{array}[]{l}lightOn\leftarrow\ switch,not\ am.\\ \leftarrow not\ lightOn.\\ \end{array}$$

$$\{\gamma (a)\mid a\in X\cap {\sigma }_i\}\cup \{\neg \gamma (a)\mid a\in (At(\Pi )\cap {\sigma }_i)\setminus X\}.$$

$${\Sigma }_2$$

$$P_1=⟨{\Pi }_1,{\mathcal{B}}_{{\mathcal{L}}_3},{\gamma }_1⟩$$

$$\begin{array}[]{l}\{switch\}.\\ lightOn\leftarrow\ switch,not\ am.\\ \leftarrow not\ lightOn.\\ \{am\}.\\ \leftarrow not\ am,|x<12|.\\ \leftarrow am,|x\geq 12|.\\ \leftarrow|x<0|.\\ \leftarrow|x>23|.\\ \end{array}$$

$$\{switch,lightOn,|x\ge 12|\}$$

$$\begin{array}[]{c}\{\gamma_{1}(|x\geq 12|),\neg\gamma_{1}(|x<12|),\neg\gamma_{1}(|x<0|),\neg\gamma_{1}(|x>23|)\}\\ =\\ \{x\geq 12,\neg x<12,\neg x<0,\neg x>23\}\end{array}$$

Full text

Under consideration in Theory and Practice of Logic Programming (TPLP).

KEYWORDS: constraint answer set programming, constraint satisfaction processing, satisfiability modulo theories

1 Introduction

Constraint answer set programming (CASP) Elkabani et al. (2004); Mellarkod et al. (2008); Gebser et al. (2009); Balduccini (2009); Lierler (2014) is a promising research direction that integrates answer set programming, a powerful knowledge representation paradigm, with constraint processing. Typical answer set programming tools start their computation with grounding, a process that substitutes variables for passing constants in respective domains. Large domains often form an obstacle for classical answer set programming. CASP enables a mechanism to model constraints over large domains so that they are processed in a non-typical way for answer set programming 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. Acyclicity programs Bomanson et al. (2015) (or logic programs modulo acyclicity constraints) form another recently investigated formalism that parallels satisfiability modulo graphs framework developed within SMT Gebser et al. (2014).

This work attempts 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 is 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 CASP and SMT, and (ii) between constraint formulas and SMT formulas. We are able to then provide a formal description relating a family of distinct constraint answer set programming formalisms.

We show 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 the design of CASP solvers and possibly SMT solvers. For example, theoretical results of this work establish a simple method for using SMT systems for computing answer sets of a broad class of tight constraint answer set programs. Susman and Lierler (2016) utilized this method in implementing an SMT-based solver for such programs. In the conclusion of this work, we rely on the concept of level ranking by Niemelä (2008) to develop a translation for nontight constraint answer set programs to SMT formulas so that an SMT solver can be used to compute answer sets of such programs.

Paper Outline

Section 2 is on preliminaries. It reviews concepts of logic programs, completion, (input) answer sets, and level ranking. Section 2.2 presents the details of generalized constraint satisfaction problem and links this notion to classical constraint satisfaction. The section on preliminaries concludes with formal definitions of linear and integer linear constraints. Section 3 introduces constraint answer set programs and constraint formulas. Next, in Section 4 we present satisfiability modulo theories and specify a class of uniform theories. Section 5 defines SMT formulas and ASPT programs. Uniform theories provide us with a ground to establish a formal link between CASP and SMT in Section 6 by relating SMT formulas with constraint formulas and ASPT programs with constraint answer set programs. Section 6 concludes by characterizing a family of distinct constraint answer set programming formalisms using the uniform terminology proposed in this work. Section 7 utilizes the generalization of level ranking to propose a method of using SMT solvers for computing answer sets of constraint answer set programs with integer constraints. Finally, we list the conclusions.

2 Preliminaries

This section starts by reviewing logic programs and the concept of an answer set. It also introduces programs’ completion. Next, the generalized constraint satisfaction problems are introduced and related to the classical constraint satisfaction problems studied in artificial intelligence.

2.1 Logic Programs and Completion

Syntax

A vocabulary is a set of propositional symbols also called atoms. As customary, a literal is an atom $a$ or its negation, denoted $\neg a$. A (propositional) logic program, denoted by $\Pi$, over vocabulary $\sigma$ is a set of rules of the form

[TABLE]

where $a$ is an atom over $\sigma$ or $\bot$, and each $b_{i}$, $1\leq i\leq n$, is an atom in $\sigma$. We will sometimes use the abbreviated form for rule (1)

[TABLE]

where $B$ stands for $b_{1},\ldots,b_{\ell},\ not\ b_{\ell+1},\ldots,\ not\ b_{m},\ not\ \ not\ b_{m+1},\ldots,\ not\ \ not\ b_{n}$ and is also called a body. Syntactically, we identify rule (1) with the propositional formula

[TABLE]

and $B$ with the propositional formula

[TABLE]

Note that (i) the order of terms in (4) is immaterial, (ii) not is replaced with classical negation ($\neg$), and (iii) comma is replaced with conjunction ($\wedge$). Expression

[TABLE]

in formula (4) is referred to as the positive part of the body and the remainder of (4) as the negative part of the body. Sometimes, we interpret semantically rule (1) and its body as propositional formulas, in these cases it is obvious that double negation $\neg\neg$ in (3) and (4) can be dropped.

The expression $a$ is the head of the rule. When $a$ is $\bot$, we often omit it and say that the head is empty. We write $\mathit{hd}(\Pi)$ for the set of nonempty heads of rules in $\Pi$.

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 the set of facts $\{a.\mid a\in X\}$.

Semantics

We say a set $X$ of atoms satisfies rule (1), if $X$ satisfies the propositional formula (3), where we identify $X$ with an assignment over the atoms in  (3) in a natural way:

• •

any atom that occurs in $X$ maps to truth value $\mathit{true}$ and

• •

any atom in (3) but not in $X$ maps to truth value $\mathit{false}$.

We say $X$ satisfies a program $\Pi$, if $X$ satisfies every rule in $\Pi$. In this case, we also say that $X$ is a model of $\Pi$. We may abbreviate satisfaction relation with symbol $\models$ (to denote that a set of atoms satisfies a rule or a program or a formula).

The reduct $\Pi^{X}$ of a program $\Pi$ relative to a set $X$ of atoms is obtained by first removing all rules (1) such that $X$ does not satisfy negative part of the body $\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 with $a\leftarrow b_{1},\ldots,b_{\ell}$. A set $X$ of atoms is an answer set, if it is the minimal set that satisfies all rules of $\Pi^{X}$ Lifschitz et al. (1999).

Ferraris and Lifschitz (2005) showed that a choice rule $\{a\}\leftarrow B$ can be seen as an abbreviation for a rule $a\leftarrow\ not\ not\ a,B$ (choice rules were introduced by Niemelä and Simons (2000) and are commonly used in answer set programming languages). We adopt this abbreviation in the rest of the paper.

Example 1

Consider the logic program from Balduccini and Lierler (2017):

[TABLE]

Each rule in the program can be understood as follows:

• •

The action switch is exogenous.

• •

The light is on (lightOn) during the night (not am) when the action switch has occurred.

• •

The light must be on.

• •

It is night (not am) or morning (am)

*Choice rules $\{switch\}.$ and $\{am\}.$ in program (5) abbreviate rules *

[TABLE]

respectively. Consider set $\{switch,\ lightOn\}$ of atoms. The reduct of program (5) relative to this set follows:

[TABLE]

It is easy to see that set $\{switch,\ lightOn\}$ satisfies every rule of the reduct. Furthermore, this set is minimal among sets with this property. Thus, it is an answer set of program (5). In fact, it is the only answer set of this program. This answer set suggests that the only situation that satisfies the specifications of the problem is such that (i) it is currently night, (ii) the light has been switched on, and (iii) the light is on.

Completion

It is customary for a given vocabulary $\sigma$, to identify a set $X$ of atoms over $\sigma$ with (i) a complete and consistent set of literals over $\sigma$ constructed as $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 in $X$ and $\mathit{false}$ to every atom in $\sigma\setminus X$.

By $Bodies(\Pi,a)$ we denote the set of the bodies of all rules of $\Pi$ with head $a$. For a program $\Pi$ over vocabulary $\sigma$, the completion of $\Pi$ Clark (1978), denoted by $Comp(\Pi)$, is the set of classical formulas that consists of the rules (1) in $\Pi$ (recall that we identify rule (1) with implication (3)) and the implications

[TABLE]

for all atoms $a$ in $\sigma$. When set $Bodies(\Pi,a)$ is empty, the implication (6) has the form $a\rightarrow\bot$. When a rule (2) is a fact $~{}a.~{}$, then we identify this rule with the clause consisting of a single atom $a$.

Example 2

The completion of logic program (5) consists of formulas

[TABLE]

It is easy to see that this completion is equivalent to the set of formulas

[TABLE]

The set $\{switch,lightOn\}$ is the only model of (8). (Unless the signature of a formula is explicitly stated, we consider the set of atoms occurring in the formula to implicitly specify its signature.) Note that set $\{switch,lightOn\}$ coincides with the only answer set of program (5).

Tightness

Any answer set of a program is also a model of its completion. The converse does not always hold. Yet, for the large class of logic programs, called tight, their answer sets coincide with models of their completion Fages (1994); Erdem and Lifschitz (2001). Tightness is a syntactic condition on a program that can be verified by means of program’s dependency graph.

The dependency graph of $\Pi$ is the directed graph $G$ such that

• •

the vertices of $G$ are the atoms occurring in $\Pi$, and

• •

for every rule (1) in $\Pi$ whose head is not $\bot$, $G$ has an edge from atom $a$ to each atom in positive part $b_{1},\dots,b_{\ell}$ of its body.

A program is called tight if its dependency graph is acyclic.

For example, the dependence graph of program (5) consists of three nodes, namely, $am$, $switch$, and $lightOn$ and a single edge from $lightOn$ to $switch$. This program is obviously tight.

Level Rankings

Niemelä (2008) characterized answer sets of "normal" logic programs in terms of "level rankings". Normal programs consist of rules of the form (1), where $n=m$ and $a$ is an atom. Thus, such constructs as choice rules and so-called denials (rules with empty head) are not covered by normal programs. We generalize the concept of level ranking to programs considered in this paper that are more general than normal ones.

We start by introducing some notation. By $\mathbb{N}$ we denote the set of natural numbers. For a rule (2), by $B^{+}$ we denote its positive part and sometimes identify it with the set of atoms that occur in it, i.e., $\{b_{1},\dots,b_{l}\}$ (recall that $B$ in (2) stands for the right hand side of the arrow in rule (1)). For a program $\Pi$, by $\mathit{At}(\Pi)$ we denote the set of atoms occurring in it.

Definition 1

For a logic program $\Pi$ and a set $X$ of atoms over $\mathit{At}(\Pi)$, a function lr: $X\rightarrow\mathbb{N}$ is a level-ranking of $X$ for $\Pi$ when for each $a\in X$, there is $B$ in $Bodies(\Pi,a)$ such that $X$ satisfies $B$ and for every $b\in B^{+}$ it holds that $\hbox{lr}(a)-1\geq\hbox{lr}(b)$.

Niemelä (2008) observed that for an arbitrary normal logic programs, a model $X$ of its completion is also an answer set for this program when there is a level ranking of $X$ for the program. We generalize this result beyond normal programs.

Theorem 1

*For a program $\Pi$ and a set $X$ of atoms that is a model of its completion $Comp(\Pi)$, $X$ is an answer set of $\Pi$ if and only if there is a level ranking of $X$ for $\Pi$. *

Proof 2.2**.**

The proof largely follows the lines of the proof of Theorem 1 from Niemelä (2008) but utilizes the terminology used in this paper. We start by defining an operator $T_{\Pi}(I)$ for a program $\Pi$ and a set $I$ over $\mathit{At}(\Pi)\cup\{\bot\}$ as follows:

[TABLE]

For this operator we define

[TABLE]

and for $i=0,1,2,\dots$

[TABLE]

Left-to-right: Assume $X$ is an answer set of $\Pi$. We can construct a level ranking lr of $X$ for $\Pi$ using the $T_{\Pi^{X}}(\cdot)$ operator. As $X$ is an answer set of $\Pi$, we know that $X=T_{\Pi^{X}}\uparrow\omega$ and for each $a\in X$ there is a unique $i$ such that $a\in T_{\Pi^{X}}\uparrow i$, but $a\not\in T_{\Pi^{X}}\uparrow(i-1)$. We consider $\hbox{lr}(a)=i$. We now illustrate that lr is indeed a level ranking. For $a\in X$ there is a rule $a\leftarrow B$ of the form (1) such that $a\leftarrow b_{1},\ldots,b_{\ell}\in\Pi^{X}$ and $T_{\Pi^{X}}\uparrow(i-1)$ satisfies $b_{1}\wedge\ldots\wedge b_{\ell}$. Consequently, for every $b_{j}$ in $\{b_{1},\ldots,b_{\ell}\}$, $lr(b_{j})\leq i-1$. Thus, $\text{lr}(a)-1\geq\text{lr}(b_{j})$. Also, from the way the reduct is constructed it follows that $X$ satisfies body $B$ of rule $a\leftarrow B$.

Right-to-left: Assume that there is a level ranking lr of $X$ for $\Pi$. We show that then $X$ is the minimal model of $\Pi^{X}$, which implies that $X$ is an answer set of $\Pi$. Since $X$ is a model of the completion of $\Pi$ it follows that $X$ is also a model of $\Pi$. Indeed, recall the construction process of completion. From the construction of $\Pi^{X}$ it follows that $X$ is also a model of $\Pi^{X}$. Proof by contradiction. Assume that there is a set of atoms $X^{\prime}\subset X$ such that $X^{\prime}$ is a model of $\Pi^{X}$ and hence $X$ is not a minimal model of $\Pi^{X}$. Consider now an atom $a\in X\setminus X^{\prime}$ with the smallest level ranking $\hbox{lr}(a)$. Since lr is a level ranking of $X$ for $\Pi$, it follows that there is a rule $a\leftarrow B$ in $\Pi$ such that $X\models B$ and for every $b\in B^{+}$, it holds that $\hbox{lr}(b)<\hbox{lr}(a)$. As we considered atom $a$ in $X\setminus X^{\prime}$ with the smallest level ranking it follows that $b\in X^{\prime}$. By $\Pi^{X}$ construction, rule $a\leftarrow B^{+}$ belongs to $\Pi^{X}$. We derive that $X^{\prime}$ satisfies $B^{+}$, but does not contain $a$. This contradicts out assumption that $X^{\prime}$ satisfies $\Pi^{X}$ as it does not satisfy rule $a\leftarrow B^{+}$.

2.2 Generalized Constraint Satisfaction Problems

In this section we present a primitive constraint as defined by Marriott and Stuckey (1998, Section 1.1). We refer to this concept as a constraint, dropping the word “primitive”. We use constraints to define 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 form a special case of generalized constraint satisfaction problems. We finally introduce linear constraints and linear constraint satisfaction problems.

Signature, c-vocabulary, constraint atoms

We adopt the following convention: for a function $\nu$ and an element $x$, by $x^{\nu}$ we denote the value that function $\nu$ maps $x$ to, in other words, $x^{\nu}=\nu(x)$. A domain is a nonempty set of elements (or values). A signature $\Sigma$ is a set of variables, predicate symbols, and function symbols (or f-symbols). Predicate and function symbols are associated with a positive integer called arity. By ${\Sigma}_{|v}$, ${\Sigma}_{|r}$, and ${\Sigma}_{|f}$ we denote the subsets of $\Sigma$ that contain all variables, all predicate symbols, and all f-symbols respectively.

For instance, we can define signature $\Sigma_{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, ${{\Sigma_{1}}}_{|v}=\{s,r\}$, ${{\Sigma_{1}}}_{|r}=\{E,Q\}$, ${{\Sigma_{1}}}_{|f}=\emptyset$.

Let $D$ be a domain. For a set $V$ of variables, we call a total function $\nu:V\rightarrow D$ a $[V,D]$* valuation*. For a set $R$ of predicate symbols, we call a total function on $R$ an $[R,D]$ r-denotation, when it maps each $n$-ary predicate symbol of $R$ into an $n$-ary relation on $D$. For a set $F$ of f-symbols, we call a total function on $F$ an $[F,D]$ f-denotation, when it maps each $n$-ary f-symbol of $F$ into a function $D^{n}\rightarrow D$.

Table 1 presents sample definitions of a domain, valuations, and r-denotations. In the remainder of the paper we frequently refer to these sample valuations, and r-denotations.

A constraint vocabulary (c-vocabulary) is a pair $[\Sigma,D]$, where $\Sigma$ is a signature and $D$ is a domain. A term over a c-vocabulary $[\Sigma,D]$ is either

• •

a variable in ${\Sigma}_{|v}$,

• •

a domain element in $D$, or

• •

an expression $f(t_{1},\dots,t_{n})$, where $f$ is an f-symbol of arity $n$ in ${\Sigma}_{|f}$ and $t_{1},\dots,t_{n}$ are terms over $[\Sigma,D].$

A constraint atom over a c-vocabulary $[\Sigma,D]$ is an expression

[TABLE]

where $P$ is a predicate symbol from ${\Sigma}_{|r}$ of arity $n$ and $t_{1},\dots,t_{n}$ are terms over $[\Sigma,D]$. A constraint literal over a c-vocabulary $[\Sigma,D]$ is either a constraint atom (9) or an expression

[TABLE]

where $P(t_{1},\dots,t_{n})$ is a constraint atom over $[\Sigma,D]$.

For instance, expressions

[TABLE]

are constraint literals over c-vocabulary $[\Sigma_{1},D_{1}]$, where $\Sigma_{1}$ and $D_{1}$ are defined in Table 1.

It is due to notice that syntactically, constraint literals are similar to ground literals of predicate logic. (In predicate logic, variables as defined here are referred to as object constants or function symbols of arity [math].) The only difference is that here domain elements are allowed to form a term. For instance, an expression $E(2)$ is a constraint atom over $[\Sigma_{1},D_{1}]$, where $2$ is a term formed from a domain element. In predicate logic, domain elements are not part of a signature over which atoms are formed.

We now proceed to introducing satisfaction relation for constraint literals. Let $[\Sigma,D]$ be a c-vocabulary, $\nu$ be a $[{\Sigma}_{|v},D]$ valuation, $\rho$ be a $[{\Sigma}_{|r},D]$ r-denotation, and $\phi$ be a $[{\Sigma}_{|f},D]$ f-denotation. First, we define recursively a value that valuation $\nu$ assigns to a term $\tau$ over $[\Sigma,D]$ with respect to $\phi$. We denote this value by $\tau^{\nu,\phi}$ and compute it as follows:

• •

for a term that is a variable $x$ in ${\Sigma}_{|v}$, $x^{\nu,\phi}=x^{\nu}$,

• •

for a term that is a domain element $d$ in $D$, $d^{\nu,\phi}$ is $d$ itself,

• •

for a term $\tau$ of the form $f(t_{1},\dots,t_{n})$, $\tau^{\nu,\phi}$ is defined recursively by the formula

[TABLE]

Second, we define what it means for valuation to be a solution of a constraint literal with respect to given r- and f-denotations. We say that $\nu$ satisfies (is a solution to) constraint literal (9) over $[\Sigma,D]$ with respect to $\rho$ and $\phi$ when $\langle t_{1}^{\nu,\phi},\dots,t_{n}^{\nu,\phi}\rangle\in P^{\rho}$. Let $\mathcal{R}$ be an n-ary relation on $D$. By $\overline{\mathcal{R}}$ we denote complement relation of $\mathcal{R}$ constructed as $D^{n}\setminus\mathcal{R}$. Valuation $\nu$ satisfies (is a solution to) constraint literal of the form (10) with respect to $\rho$ and $\phi$ when $\langle t_{1}^{\nu,\phi},\dots,t_{n}^{\nu,\phi}\rangle\in\overline{P^{\rho}}.$

For instance, consider declarations of valuations $\nu_{1}$ and $\nu_{2}$, and r-denotations $\rho_{1}$ and $\rho_{2}$ in Table 1. Valuation $\nu_{1}$ satisfies constraint literal $Q(r,s)$ with respect to $\rho_{1}$, while valuation $\nu_{2}$ does not satisfy this constraint literal with respect to $\rho_{2}$.

Lexicon, constraints, generalized constraint satisfaction problem

We are now ready to define constraints, their syntax and semantics. To begin we introduce a lexicon, which is a tuple $([\Sigma,D],\rho,\phi)$, where $[\Sigma,D]$ is a c-vocabulary, $\rho$ is a $[{\Sigma}_{|r},D]$ r-denotation, and $\phi$ is a $[{\Sigma}_{|f},D]$ f-denotation. For a lexicon $\mathcal{L}=([\Sigma,D],\rho,\phi)$, we call any function that is $[{\Sigma}_{|v},D]$ valuation, a valuation over $\mathcal{L}$. We omit the last element of the lexicon tuple if the signature $\Sigma$ of the lexicon contains no f-symbols. A constraint is defined over lexicon $\mathcal{L}=([\Sigma,D],\rho,\phi)$. Syntactically, it is a constraint literal over $[\Sigma,D]$ (lexicon $\mathcal{L}$, respectively). Semantically, we say that valuation $\nu$ over $\mathcal{L}$ satisfies (is a solution to) the constraint $c$ when $\nu$ satisfies $c$ with respect to $\rho$ and $\phi$.

For instance, Table 2 presents definitions of sample lexicons $\mathcal{L}_{1}$, $\mathcal{L}_{2}$, and constraints $c_{1}$, $c_{2}$, $c_{3}$, and $c_{4}$ using the earlier declarations from Table 1. Valuation $\nu_{1}$ from Table 1 is a solution to $c_{1}$, $c_{2}$, $c_{3}$, but not a solution to $c_{4}$. Valuation $\nu_{2}$ from Table 1 is not a solution to $c_{1}$, $c_{2}$, $c_{3}$, and $c_{4}$. In fact, constraint $c_{4}$ 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 2.3**.**

A generalized constraint satisfaction problem (GCSP) $\mathcal{C}$ is a finite set of constraints over a lexicon $\mathcal{L}=([\Sigma,D],\rho,\phi)$. We say that a valuation $\nu$ over $\mathcal{L}$ satisfies (is a solution to) the GCSP $\mathcal{C}$ when $\nu$ is a solution to every constraint in $\mathcal{C}$.

For example, consider a set $\{c_{2},c_{3},c_{4}\}$ of constraints. Any subset of this set forms a GCSP, including subsets $\{c_{2},c_{3}\}$ and $\{c_{2},c_{3},c_{4}\}$. Sample valuation $\nu_{1}$ over lexicon $\mathcal{L}_{2}$ (where $\nu_{1}$ stems from Tables 1) satisfies the GCSP $\{c_{2},c_{3}\}$, but does not satisfy the GCSP $\{c_{2},c_{3},c_{4}\}$.

From GCSP to Constraint Satisfaction Problem

We now define a constraint satisfaction problem (CSP) as customary in classical literature on artificial intelligence. We then explain in which sense generalized constraint satisfaction problems generalize CSPs.

We say that a lexicon is finite-domain if it is defined over a c-vocabulary that refers to a domain whose set of elements is finite. Trivially, lexicons $\mathcal{L}_{1}$ and $\mathcal{L}_{2}$ defined in Table 2 are finite-domain lexicons. Consider a special case of a constraint of the form (9) over finite-domain lexicon $\mathcal{L}=([\Sigma,D],\rho)$, so that each $t_{i}$ is a variable. (For instance, constraints $c_{1}$, $c_{2}$, and $c_{3}$ satisfy the stated requirements, while $c_{4}$ does not.) In this case, we can identify constraint (9) over $\mathcal{L}$ with the pair

[TABLE]

A constraint satisfaction problem (CSP) is a set of pairs (11), where ${\Sigma}_{|v}$ and $D$ of the finite-domain lexicon $\mathcal{L}$ are called the variables and the domain of CSP, respectively. Saying that valuation $\nu$ over $\mathcal{L}$ satisfies (9) is the same as saying that $\langle t_{1}^{{\nu}},\dots,t_{n}^{{\nu}}\rangle\in P^{\rho}.$ The latter is the way in which a solution to expressions (11) 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 (11) in $C$.

In conclusion, GCSP generalizes CSP by

• •

elevating the finite-domain restriction, and

• •

allowing us more elaborate syntactic expressions (e.g., recall f-symbols).

2.2.1 Linear and Integer Linear Constraints

We now define “numeric” signatures and lexicons and introduce a set of constraints referred to as linear, which are commonly used in practice. A numeric signature is a signature that satisfies the following requirements

• •

its only predicate symbols are $<$, $>$, $\leq$, $\geq$, $=$, $\neq$ of arity 2, and

• •

its only f-symbols are $+$, $\times$ of arity $2$.

We use the symbol $\mathcal{A}$ to denote a numeric signature.

Symbols $\mathbb{Z}$ and $\mathbb{R}$ denote the sets of integers and real numbers respectively. Let $\rho_{\mathbb{Z}}$ and $\phi_{\mathbb{Z}}$ be $[\{<,>,\leq,\geq,=,\neq\},\mathbb{Z}]$ r-denotation and $[\{+,\times\},\mathbb{Z}]$ f-denotation respectively, where they map their predicate and function symbols into usual arithmetic relations and operations over integers. Similarly, $\rho_{\mathbb{R}}$ and $\phi_{\mathbb{R}}$ denote $[\{<,>,\leq,\geq,=,\neq\},\mathbb{R}]$ r-denotation and $[\{+,\times\},\mathbb{R}]$ f-denotation respectively, defined over the reals. We can now define the following lexicons

• •

an integer lexicon of the form $([\mathcal{A},\mathbb{Z}],\rho_{\mathbb{Z}},\phi_{\mathbb{Z}})$,

• •

a numeric lexicon of the form $([\mathcal{A},\mathbb{R}],\rho_{\mathbb{R}},\phi_{\mathbb{R}})$.

A (numeric) linear expression has the form

[TABLE]

where $a_{1},\dots,a_{n}$ are real numbers and $x_{1},\dots,x_{n}$ are variables over real numbers. When $a_{i}=1$ ($1\leq i\leq n$) we may omit it from the expression. We view expression (12) as an abbreviation for the following term

[TABLE]

over some c-vocabulary $[\mathcal{A},\mathbb{R}]$, where $\mathcal{A}$ contains $x_{1},\dots,x_{n}$ as its variables. For instance, $2x_{2}+3x_{3}$ is an abbreviation for the expression $+(\times(2,x_{2}),\times(3,x_{3})).$

An integer linear expression has the form (12), where $a_{1},\dots,a_{n}$ are integers, and $x_{1},\dots,x_{n}$ are variables over integers.

We call a constraint linear (integer linear) when it is defined over some numeric (integer) lexicon and has the form

[TABLE]

where $e$ is a linear (integer linear) expression, $k$ is a real number (an integer), and $\bowtie$ belongs to $\{<,>,\leq,\geq,=,\neq\}$. We can write (13) as an expression in usual infix notation $e\bowtie k$.

We call a GCSP a (integer) linear constraint satisfaction problem when it is composed of (integer) linear constraints. For instance, consider integer linear constraint satisfaction problem composed of two constraints $x>4$ and $x<5$ (here signature $\mathcal{A}$ is implicitly defined by restricting its variable to contain $x$). It is easy to see that this problem has no solutions. On the other hand, linear constraint satisfaction problem composed of the same two constraints $x>4$ and $x<5$ has an infinite number of solutions, including valuation that assigns $x$ to $4.1$.

3 Constraint Answer Set Programs and Constraint Formulas

In this section we introduce constraint answer set programs, which merge the concepts of logic programming and generalized constraint satisfaction problems. We also present a similar concept of “constraint formulas”, which merges the concepts of propositional formulas and generalized constraint satisfaction problems. First, we introduce input answer sets, followed by constraint answer set programs and input completion. Second, we present constraint formulas. Finally, we demonstrate the close connection between the constraint answer set programs and constraint formulas using the concept of input completion and tightness condition.

3.1 Constraint Answer Set Programs

We start by introducing a concept in spirit of an input answer set by Lierler and Truszczynski (2011).222Similar concepts to input answer sets have been noted by Gelfond and Przymusinska (1996), Oikarinen and Janhunen (2006), and Denecker and Vennekens (2007)). In particular, we consider input answer sets “relative to input vocabularies”. We then extend the definition of completion and restate the result by Erdem and Lifshitz (2001) for the case of input answer sets. The concept of an input answer set is essential for introducing constraint answer set programs. Constraint answer set programs (and constraint formulas) 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 3.4**.**

For a logic program $\Pi$ over vocabulary $\sigma$, a set $X$ of atoms over $\sigma$ is an input answer set of $\Pi$ relative to vocabulary $\iota\subseteq\sigma$ so that $\mathit{hd}(\Pi)\cap\iota=\emptyset$ when $X$ is an answer set of the program

[TABLE]

To illustrate the concept of an input answer set consider program

[TABLE]

This program has a unique input answer set $\{switch,lightOn\}$ relative to input vocabulary $\{switch,am\}$.

Let $\sigma_{r}$ and $\sigma_{i}$ be two disjoint vocabularies. We refer to their elements as regular and irregular atoms respectively.

Definition 3.5**.**

A constraint answer set program (CAS program) over the vocabulary $\sigma=\sigma_{r}\cup\sigma_{i}$ is a triple $\langle\Pi,\mathcal{B},\gamma\rangle$, where

• •

$\Pi$* is a logic program over the vocabulary $\sigma$ such that $\mathit{hd}(\Pi)\cap\sigma_{i}=\emptyset$,*

• •

$\mathcal{B}$* is a set of constraints over some lexicon $\mathcal{L}$, and *

• •

$\gamma$* is an injective function from the set $\sigma_{i}$ of irregular atoms to the set $\mathcal{B}$ of constraints.*

For a CAS program $P=\langle\Pi,\mathcal{B},\gamma\rangle$ over the vocabulary $\sigma=\sigma_{r}\cup\sigma_{i}$ so that $\mathcal{L}$ is the lexicon of the constraints in $\mathcal{B}$, a set $X\subseteq\mathit{At}(\Pi)$ is an answer set of $P$ if

$X$* is an input answer set of $\Pi$ relative to $\sigma_{i}$, and* 2. 2.

the following GCSP over $\mathcal{L}$ has a solution

[TABLE]

Note that $\neg{\gamma(a)}$ may result in expression of the form $\neg\neg P(t_{1},\dots,t_{n})$ that we identify with $P(t_{1},\dots,t_{n})$. (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, and

• •

allow for more general syntax of logic rules (e.g. choice rules are covered by the presented definition).

This is a good place to note a restriction $\mathit{hd}(\Pi)\cap\sigma_{i}=\emptyset$ on the form of the rules in a CAS program. This restriction states that an irregular atom may not form a head of a rule. There is a body of research including, for example, work by Bartholomew and Lee (2012),  Lifschitz (2012), and Balduccini (2013) that investigates variants of semantics of CAS-like programs, where analogous to irregular atoms are allowed in the heads. Lifting this restriction proves to be nontrivial. Traditional CASP systems, such as clingcon or ezcsp, restrict their attention to programs discussed here.

It is worthwhile to remark on the second condition in the definition of an answer set for CAS programs. This condition requires the existence of a solution to a constructed GCSP problem, and ignores a form of a particular solution to this GCSP or a possibility of multiple solutions. We now define a concept of an extended answer set that takes a solution to a constructed GCSP problem into account:

Definition 3.6**.**

For a CAS program $P=\langle\Pi,\mathcal{B},\gamma\rangle$ over the vocabulary $\sigma=\sigma_{r}\cup\sigma_{i}$ so that $\mathcal{L}$ is the lexicon of the constraints in $\mathcal{B}$, a set $X\subseteq\sigma$ and valuation $\nu$ from variables in the signature of $\mathcal{L}$ to the domain of $\mathcal{L}$, a pair $\langle X,\nu\rangle$ is an extended answer set of $P$ if $X$ is an answer set of $P$ and $\nu$ is a solution to GCSP (14).

CASP systems, such as clingcon or ezcsp, allow the user to select whether he is interested in computing answer sets or extended answer sets of a given CAS program. In the rest of the paper we focus on the notion of an answer set, but generalizing concepts and results introduced later to the notion of extended answer set is not difficult.

In the sequel we adopt the following notation. To distinguish irregular atoms from the constraints to which these atoms are mapped, we use bars to denote that an expression is an irregular atom. For instance, $|x<12|$ and $|x\geq 12|$ denote irregular atoms. Whereas inequalities (constraints) $x<12$ and $x\geq 12$, respectively, provide natural mappings for these atoms. We assume such natural mappings in this presentation.

Example 3.7**.**

Let us consider sample constraint answer set program. We first define the integer lexicon $\mathcal{L}_{3}$:

[TABLE]

Second, we define a CAS program

[TABLE]

over integer lexicon $\mathcal{L}_{3}$, where

• •

$\Pi_{1}$* is the program*

[TABLE]

The set of irregular atoms of $\Pi_{1}$ is $\{|x<12|,|x\geq 12|,|x<0|,|x>23|\}$. The remaining atoms form the regular set. The first four lines of program $\Pi_{1}$ are identical to these of logic program (5). The last four lines of the program state:

• –

It must be $am$ when $x<12$, where $x$ is understood as the hours.

• –

It is impossible for it to be $am$ when $x\geq 12$.

• –

Variable $x$ must be nonnegative.

• –

Variable $x$ must be less than or equal to $23$.

• •

$\mathcal{B}_{\mathcal{L}_{3}}$* is the set of all integer linear constraints over integer lexicon ${\mathcal{L}_{3}}$, which obviously includes constraints $\{x<12,x\geq 12,x<0,x>23\}$,*

• •

\gamma_{1}(a)=\begin{cases}\mbox{constraint x<12$over integer lexicon$\mathcal{L}{3}}&\mbox{if }a=|x<12|\\ \mbox{constraint x\geq 12$over integer lexicon$\mathcal{L}{3}}&\mbox{if }a=|x\geq 12|.\\ \mbox{constraint x<0$over integer lexicon$\mathcal{L}{3}}&\mbox{if }a=|x<0|\\ \mbox{constraint x>23$over integer lexicon$\mathcal{L}{3}}&\mbox{if }a=|x>23|.\end{cases}* *

Consider the set

[TABLE]

*over $At(\Pi_{1})$. This set is the only input answer set of $\Pi_{1}$ relative to its irregular atoms. Also, the integer linear constraint satisfaction problem with constraints *

[TABLE]

*has a solution. There are 12 valuations ${v_{1}}\dots v_{12}$ relative to integer lexicon $\mathcal{L}_{3}$ for $x$, which satisfy this GCSP: $x^{v_{1}}=12,\dots,x^{v_{12}}=23$. It follows that set (18) is an answer set of $P_{1}$. Pair $\langle\{switch,\ lightOn,|x\geq 12|\},\nu_{1}\rangle$ is one of the twelve extended answer sets of $P_{1}$. *

3.1.1 On Grounding

In practice, CASP languages similarly to ASP languages, allow for non-constraint variables. Gebser et al. (2009) present a program written in the language supported by CASP solver clingcon for the so called bucket problem. We list a rule from that program to illustrate the notion of non-constraint variables333A rule is taken form the site documenting system clingcon: http://www.cs.uni-potsdam.de/clingcon/examples/bucket˙torsten.lp .:

:- volume(B,T+1) $!= volume(B,T)$+ A, pour(B,T,A), bucket(B), time(T), amount(A).

Non-constraint variables of these rules are $B$, $T$, and $A$. The sign \$$ marks the irregular atoms. Rules of the kind are interpreted as shorthands for the set of rules without non-constraint variables, called *ground rules*. Ground rules are obtained by replacing every non-constraint variable in the rules by suitable terms not containing non-constraint variables. For instance, if suitable terms for non-constraint variable B$in the sample rule above range over a single value$a$; suitable terms for$T$range over two values [math] and$1$; and suitable terms for$A$range over two values$1$and$2$, then the clingcon rule above is instantiated as follows:

:- volume(a,1) $!= volume(a,0)$+ 1, pour(a,0,1), bucket(a), time(0), amount(1). :- volume(a,2) $!= volume(a,1)$+ 1, pour(a,1,1), bucket(a), time(1), amount(1). :- volume(a,1) $!= volume(a,0)$+ 2, pour(a,0,2), bucket(a), time(0), amount(2). :- volume(a,2) $!= volume(a,1)$+ 2, pour(a,1,2), bucket(a), time(1), amount(2).

To help to map these rules into the syntax used earlier, we rewrite the first one using notation of this paper:

[TABLE]

Expressions $volume(a,0)$, $volume(a,1)$, and $volume(a,2)$ stand for constraint variables in the signature of integer lexicon of this program. System clingcon supports integer linear constraints, where a constraint atom $|volume(a,1)\neq volume(a,0)+1|$ is naturally mapped into integer linear constraint $volume(a,1)\neq volume(a,0)+1$.

The process of replacing non-ground rules by their ground counterparts is called grounding and is well understood in ASP Gebser et al. (2007); Calimeri et al. (2008). The availability of non-constraint variables makes modeling in CASP an attractive and easy process. In fact, this feature distinguishes greatly CASP and SMT paradigms. An SMT-LIB language Barrett et al. (2015) is a standard language for interfacing major SMT solvers. This language does not provide a user with convenient modeling capabilities. There is an underlying assumption that code in SMT-LIB is to be generated by special-purpose programs.

Since grounding is a stand-alone process in CASP and a non-ground program is viewed as a shorthand for ground programs the focus of this paper is on the later.

3.1.2 Input Completion

Similar to how completion was defined in Section 2, we now define an input completion which is relative to an (input) vocabulary.

Definition 3.8**.**

For a program $\Pi$ over vocabulary $\sigma$, the input-completion of $\Pi$ relative to vocabulary $\iota\subseteq\sigma$ so that $\mathit{hd}(\Pi)\cap\iota=\emptyset$, denoted by $IComp(\Pi,\iota)$, is defined as the set of formulas in propositional logic that consists of the rules (3) in $\Pi$ and the implications (6) for all atoms $a$ occurring in $\sigma\setminus\iota$.

Example 3.9**.**

Here we illustrate the concept of input completion. Consider program $\Pi_{1}$ from Example 3.7. Its input completion relative to a vocabulary consisting of its irregular atoms $\{|x<12|,|x\geq 12|,|x<0|,|x>23|\}$ consists of formulas in (7) and formulas in

[TABLE]

It is easy to see that $IComp(\Pi_{1},\{|x<12|,|x\geq 12|,|x<0|,|x>23|\})$ is equivalent to the union of (8) and (19). The set $\{switch,lightOn,|x\geq 12|\}$ is the only model of this input completion. Note that this model coincides with the input answer set of $\Pi_{1}$ relative to the set of its irregular atoms.

The observation that we made last in the preceding example is an instance of the general fact captured by the following theorem.

Theorem 3.10**.**

For a tight program $\Pi$ over vocabulary $\sigma$ and vocabulary $\iota\subseteq\sigma$ so that $\mathit{hd}(\Pi)\cap\iota=\emptyset$, a set $X$ of atoms from $\sigma$ is an input answer set of $\Pi$ relative to $\iota$ if and only if $X$ satisfies the program’s input-completion $IComp(\Pi,\iota)$.

Furthermore, for any program any of its input answer sets is also a model of its input-completion.

Theorem 3.11**.**

For a program $\Pi$ over vocabulary $\sigma$ and vocabulary $\iota\subseteq\sigma$ so that $\mathit{hd}(\Pi)\cap\iota=\emptyset$, if a set $X$ of atoms from $\sigma$ is an input answer set of $\Pi$ relative to $\iota$ then $X$ satisfies the program’s input-completion $IComp(\Pi,\iota)$.

To prove these theorems it is useful to state the following lemma.

Lemma 3.12**.**

For a program $\Pi$ over vocabulary $\sigma$ and vocabulary $\iota\subseteq\sigma$ so that $\mathit{hd}(\Pi)\cap\iota=\emptyset$, a set $X$ of atoms over $\sigma$ is a model of formula $IComp(\Pi,\iota)$ if and only if it is a model of $Comp(\Pi\cup(X\cap\iota)).$

Proof 3.13**.**

Since we identify rules (2) in $\Pi$ with respective implications $B\rightarrow a$ we may write symbol $\Pi$ to denote not only a set of rules but also a set of respective implications.

We can write $IComp(\Pi,\iota)$ as the union of

[TABLE]

implications

[TABLE]

and

[TABLE]

Note that expression (22) can be written as

[TABLE]

Similarly, we can write $Comp(\Pi\cup(X\cap\iota))$ as a union of (20),

[TABLE]

[TABLE]

[TABLE]

Left-to-right: Assume $X\models IComp(\Pi,\iota)$. It consists of (20), (21), and (23) by construction. Trivially, $X$ satisfies (24). Thus we are left to show that $X$ satisfies (25) and (26). Note that (21) and (25) coincide since $Bodies(\Pi,a)=Bodies(\Pi\cup(X\cap\iota)),a)$ for all atoms $a\in\mathit{hd}(\Pi)$ as $\mathit{hd}(\Pi)\cap\iota=\emptyset$. Consequently, $X$ satisfies (25). Observe set (26) can be written as the union of set (23) and set

[TABLE]

Trivially, $X$ satisfies (27) as any atom that satisfies condition $a\in(\iota\setminus X)$ is such that $a\not\in X$. It also satisfies (23). Consequently, $X$ satisfies (26).

Right-to-left: Assume $X$ is a model of $Comp(\Pi\cup(X\cap\iota)).$ Set $X$ satisfies (20), (24), (25), and (26). Since $X$ satisfies (25), it satisfies (21) (as they coincide as argued above). Since $X$ satisfies (26), $X$ also satisfies (23) (Recall set (26) can be written as the union of set (23) and set (27)). Consequently, $X\models IComp(\Pi,\iota)$.

Proof 3.14** (Proof of Theorem 3.10).**

We are given that $\Pi$ is tight. Since $X\cap\iota$ only consists of facts, it follows that $\Pi\cup(X\cap\iota)$ is tight also.

Left-to-right: Assume $X$ is an input answer set of a program $\Pi$ relative to $\iota$. By Definition 3.4, $X$ is an answer set of $\Pi\cup(X\cap\iota)$. It is well known that an answer set of a program is also a model of its completion. Thus, $X$ is a model of $Comp(\Pi\cup(X\cap\iota))$. By Lemma 3.12, $X$ is a model of $IComp(\Pi,\iota)$.

Right-to-left: Assume $X\models IComp(\Pi,\iota)$. By Lemma 3.12, $X$ is a model of completion $Comp(\Pi\cup(X\cap\iota))$. By results by Fages (1994) and Erdem and Lifshitz (2001), $X$ is the answer set of the program $\Pi\cup(X\cap\iota)$. By Definition 3.4, $X$ is an input answer set of $\Pi$ relative to $\iota$.

Direction Left-to-right of the proof of Theorem 3.10 serves as a proof for Theorem 3.11 also.

3.2 Constraint Formula

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

For a propositional formula $F$, by $\mathit{At}(F)$ we denote the set of atoms occurring in it.

Definition 3.15**.**

A constraint formula over the vocabulary $\sigma=\sigma_{r}\cup\sigma_{i}$ is a triple $\langle F,\mathcal{B},\gamma\rangle$, where

• •

$F$* is a propositional formula over the vocabulary $\sigma$,*

• •

$\mathcal{B}$* is a set of constraints over some lexicon $\mathcal{L}$, and*

• •

$\gamma$* is an injective function from the set $\sigma_{i}$ of irregular atoms to the set $\mathcal{B}$ of constraints.*

For a constraint formula $\mathcal{F}=\langle F,\mathcal{B},\gamma\rangle$ over the vocabulary $\sigma=\sigma_{r}\cup\sigma_{i}$ such that $\mathcal{L}$ is the lexicon of the constraints in $\mathcal{B}$, a set $X\subseteq\mathit{At}(F)$ is a model of $\mathcal{F}$ if

$X$* is a model of $F$, and* 2. 2.

the following GCSP over $\mathcal{L}$ has a solution

[TABLE]

Example 3.16**.**

Similar to the CAS program $P_{1}$ from Example 3.7, we can define a constraint formula

[TABLE]

relative to integer lexicon $\mathcal{L}_{3}$. We understand $\Pi_{1}$, $\mathcal{B}_{\mathcal{L}_{3}}$, and $\gamma_{1}$ as in Example 3.7. Example 3.9 illustrates how input completion $IComp(\Pi_{1},\{|x<12|,|x\geq 12|,|x<0|,|x>23|\})$ is formed. The set

[TABLE]

*is the only model of $\mathcal{F}_{1}$. *

Following theorem captures a relation between CAS programs and constraint formulas. This theorem is an immediate consequence of Theorem 3.10.

Theorem 3.17**.**

For a CAS program $P=\langle\Pi,\mathcal{B},\gamma\rangle$ over the vocabulary $\sigma=\sigma_{r}\cup\sigma_{i}$ and a set $X$ of atoms over $\sigma$, when $\Pi$ is tight, $X$ is an answer set of $P$ if and only if $X$ is a model of constraint formula $\langle IComp(\Pi,\sigma_{i}),\mathcal{B},\gamma\rangle$ over $\sigma=\sigma_{r}\cup\sigma_{i}$.

We note that Example 3.7 and Example 3.16 demonstrate this property. In the future we will abuse the term "tight". We will refer to CAS program $P=\langle\Pi,\mathcal{B},\gamma\rangle$ as tight when its first member $\Pi$ has this property.

4 Satisfiability Modulo Theories

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. To be precise, a restriction formula corresponds to a conjunction of ground literals. The presented notions of interpretation and satisfaction are usual, but are stated in terms convenient for our purposes.

Definition 4.18**.**

An interpretation $I$ for a signature $\Sigma$, or $\Sigma$-interpretation, is a tuple $(D,\nu,\rho,\phi)$ where

• •

$D$* is a domain,*

• •

$\nu$* is a $[{\Sigma}_{|v},D]$ valuation,*

• •

$\rho$* is a $[{\Sigma}_{|r},D]$ r-denotation, and*

• •

$\phi$* is a $[{\Sigma}_{|f},D]$ f-denotation.*

For a signature $\Sigma$, a $\Sigma$-theory is a set of interpretations over $\Sigma$.

For signatures that contain no f-symbols, we omit the reference to the last element of the interpretation tuple. For instance, for signature $\Sigma_{1}$ from Table 1, consider the following sample interpretations:

[TABLE]

Any subset of interpretations $\{\mathcal{I}_{1},\mathcal{I}_{2}\}$ exemplifies a unique $\Sigma_{1}$-theory.

As mentioned earlier, in literature on predicate logic and SMT, the terms object constant and function symbol of arity [math] are commonly used to refer to elements in the signature that we call variables. Here we use the terms that stem from definitions related to constraint satisfaction processing to facilitate uncovering the precise link between CASP-like formalisms and SMT-like formalisms. It is typical for predicate logic signatures to contain propositional symbols (predicate symbols of arity [math]). It is easy to extend the notion of signature introduced here to allow propositional symbols. Yet it will complicate the presentation, which is the reason we avoid this extension.

A restriction formula over a signature $\Sigma$ is a finite set of constraint literals over a c-vocabulary $[\Sigma,\emptyset]$. A sample restriction formula over $\Sigma_{1}$ follows

[TABLE]

We now introduce the semantics of restriction formulas. Let $I=(D,\nu,\rho,\phi)$ be a $\Sigma$-interpretation. To each term $\tau$ over a c-vocabulary $[\Sigma,\emptyset]$, $I$ assigns a value $\tau^{\nu,\phi}$ that we denote by $\tau^{I}$. We say that interpretation $I$ satisfies restriction formula $\Phi$ over $\Sigma$, when $\nu$ satisfies every constraint literal in $\Phi$ with respect to $\rho$ and $\phi$. For instance, interpretation $\mathcal{I}_{2}$ satisfies restriction formula (29), while $\mathcal{I}_{1}$ does not satisfy (29).

We say that a restriction formula $\Phi$ over signature $\Sigma$ is satisfiable in a $\Sigma$-theory $T$, or is $T$-satisfiable, when there is an element of the set $T$ that satisfies $\Phi$. For example, restriction formula (29) is satisfiable in any $\Sigma_{1}$-theory that contains interpretation $\mathcal{I}_{2}$. On the other hand, restriction formula (29) is not satisfiable in $\Sigma_{1}$-theory $\{\mathcal{I}_{1}\}$.

To conclude the introduction to the concept of $\Sigma$-theory: from the semantical perspective, it is a collection of $\Sigma$-interpretations; from the syntactic perspective, the theory is the collection of restriction formulas satisfied by these models.

4.1 Uniform Theories and Link to Generalized Constraint Satisfaction Processing

The presented definition of a theory (Definition 4.18) places no restrictions on the domains, r-denotations, or f-denotations being identical across the interpretations defining a theory. In practice, such restrictions are very common in SMT. We now define “uniform” theories that follow these typical restrictions. We will then show how restriction formulas interpreted over uniform theories can practically be seen as GCSPs.

Definition 4.19**.**

For a signature $\Sigma$, we call a $\Sigma$-theory $T$ uniform over lexicon $\mathcal{L}=([\Sigma,D],\rho,\phi)$ when

all interpretations in $T$ are of the form $(D,\nu,\rho,\phi)$ (note how valuation $\nu$ is the only not fixed element in the interpretations), and 2. 2.

for every possible $[{\Sigma}_{|v},D]$ valuation $\nu$, there is an interpretation $(D,\nu,\rho,\phi)$ in $T$.

Example 4.20**.**

To illustrate a concept of a uniform theory, a table below defines sample domain $D_{2}$, valuations $\nu_{3}$ and $\nu_{4}$, and r-denotation $\rho_{4}$.

[TABLE]

We also note that valuations $\nu_{1}$ and $\nu_{2}$ from Table 1 can be seen not only as $[{\Sigma_{1}}_{|v},D_{1}]$ valuations, but also as $[{\Sigma_{1}}_{|v},D_{2}]$ valuations.

The set

[TABLE]

of $\Sigma_{1}$ interpretations is an example of a uniform theory over lexicon $([\Sigma_{1},D_{2}],\rho_{4})$. The set

[TABLE]

of $\Sigma_{1}$ interpretations is an example of a non-uniform theory. Indeed, the condition 1 of Definition 4.19 does not hold for this theory: the last interpretation refers to a different domain than the others. Also, recall interpretations $\mathcal{I}_{1}$ and $\mathcal{I}_{2}$ given in (28). Neither $\Sigma_{1}$-theory $\{\mathcal{I}_{1}\}$ nor $\{\mathcal{I}_{1},\mathcal{I}_{2}\}$ is uniform over lexicon $([\Sigma_{1},D_{1}],\rho_{1})$. In this case, the condition 2 of Definition 4.19 does not hold.

It is easy to see that for uniform theories we can identify their interpretations of the form $(D,\nu,\rho,\phi)$ with their second element – valuation $\nu$. Indeed, 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 $(D_{2},\nu_{1},\rho_{4})$ of uniform theory (30) as $\nu_{1}$.

For uniform $\Sigma$-theory $T$ over lexicon $([\Sigma,D],\rho,\phi)$, we can extend the syntax of restriction formulas by saying that a restriction formula is defined over c-vocabulary $[\Sigma,D]$ as a finite set of constraint literals over $[\Sigma,D]$ (earlier we considered constraint literals over $[\Sigma,\emptyset]$). The earlier definition of semantics is still applicable.

We now present a theorem that makes the connection between GCSPs over a lexicon $\mathcal{L}$ and restriction formulas interpreted using the uniform theory $T$ over the same lexicon apparent. As a result, the question whether a given GCSP over $\mathcal{L}$ has a solution translates into the question whether the set of constraint literals of a 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.

Theorem 4.21**.**

For a lexicon $\mathcal{L}=([\Sigma,D],\rho,\phi)$, a set $\Phi$ of constraint literals over c-vocabulary $[\Sigma,D]$, and a uniform $\Sigma$-theory $T$ over lexicon $\mathcal{L}$ the following holds

for any $[{\Sigma}_{|v},D]$ valuation $\nu$, there is an interpretation $\nu$ in $T$, 2. 2.

$[{\Sigma}_{|v},D]$* valuation $\nu$ is a solution to GCSP $\Phi$ over lexicon $\mathcal{L}$ if and only if interpretation $\nu$ in $T$ satisfies restriction formula $\Phi$,* 3. 3.

GCSP $\Phi$ over lexicon $\mathcal{L}$ has a solution if and only if restriction formula $\Phi$ is $T$-satisfiable.

Proof 4.22**.**

Statement 1 trivially follows from the condition 2 of the definition of uniform theories.

Proof of Statement 2. By Statement 1, interpretation $\nu$ is in $T$. By definition of a solution to GCSP, $[{\Sigma}_{|v},D]$ valuation $\nu$ is a solution to GCSP $\Phi$ over lexicon $\mathcal{L}$ if and only if $\nu$ is a solution to every constraint in $\Phi$. In other words, $\nu$ satisfies every constraint literal in $\Phi$ with respect to $\rho$ and $\phi$. By definition of interpretations satisfying formulas, the previous statement holds if and only if interpretation $\nu$ in $T$ satisfies $\Phi$.

Proof of Statement 3. GCSP $\Phi$ over lexicon $\mathcal{L}$ has a solution if and only if there is a $[{\Sigma}_{|v},D]$ valuation $\nu$ that is a solution to GCSP $\Phi$ over lexicon $\mathcal{L}$. By statements 1 and 2, the previous statement holds if and only if there is an interpretation $\nu$ in $T$ that satisfies $\Phi$ and consequently $\Phi$ is $T$-satisfiable.

Such commonly used theories in SMT as linear real arithmetic, linear integer arithmetic, and integer difference logic are uniform.444For instance, the SMT solver cvc4 Barrett et al. (2011) supports all three mentioned arithmetics. To be more precise, recall notions of numeric, integer lexicons, and (integer) linear constraints presented in Section 2.2.1. Given these notions:

• •

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 linear integer arithmetic posing yet additional syntactic restrictions Nieuwenhuis and Oliveras (2005).

From Theorem 4.21, it follows that restriction formulas in linear real arithmetic can be seen as linear constraint satisfaction problems (and the other way around). Similar relation holds between restriction formulas in linear integer arithmetic and integer linear constraint satisfaction problems.

5 SMT Formulas and ASPT Programs

First, this section introduces SMT formulas that merge the concepts of propositional formulas and $\Sigma$-theories. Second, it introduces ASPT programs that merge the concepts of logic programs and $\Sigma$-theories. It turns out that if considered $\Sigma$-theories are uniform then formalisms of constraint formulas and SMT formulas coincide. A similar relation holds of constraint answer set programs and ASPT programs. This link is discussed in the next section.

As in Section 3.1, we understand $\sigma_{r}$ and $\sigma_{i}$ as two disjoint vocabularies and refer to their elements as regular and irregular.

Definition 5.23**.**

An SMT formula $P$ over vocabulary $\sigma=\sigma_{r}\cup\sigma_{i}$ is a triple $\langle F,T,\mu\rangle$, where

• •

$F$* is a propositional formula over $\sigma$,*

• •

$T$* is a $\Sigma$-theory, and*

• •

$\mu$* is an injective function from irregular atoms $\sigma_{i}$ to constraint literals over c-vocabulary $[\Sigma,\emptyset]$.*

For an SMT formula $\langle F,T,\mu\rangle$ over $\sigma$, a set $X\subseteq\mathit{At}(F)$ is its model if

$X$* is a model of $F$, and* 2. 2.

the following restriction formula

[TABLE]

is satisfiable in $\Sigma$-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 et al., 2008, Section 26.2.1.4) or (Barrett and Tinelli, 2014, Section 1.1), which, in their most commonly used case, coincide with SMT formulas discussed here.

We now define the concept of logic programs modulo theories.

Definition 5.24**.**

A logic program modulo theories (or ASPT program) $P$ over vocabulary $\sigma=\sigma_{r}\cup\sigma_{i}$ is a triple $\langle\Pi,T,\mu\rangle$, where

• •

$\Pi$* is a logic program over $\sigma$ such that $\mathit{hd}(\Pi)\cap\sigma_{i}=\emptyset$,*

• •

$T$* is a $\Sigma$-theory, and*

• •

$\mu$* is an injective function from irregular atoms $\sigma_{i}$ to constraint literals over c-vocabulary $[\Sigma,\emptyset]$.*

For an ASPT program $\langle\Pi,T,\mu\rangle$ over $\sigma$, a set $X\subseteq\mathit{At}(\Pi)$ is its answer set if

$X$* is an input answer set of $\Pi$ relative to $\sigma_{i}$, and* 2. 2.

the following restriction formula

[TABLE]

is satisfiable in $\Sigma$-theory $T$.

In the case of uniform theories, we can extend the definition of SMT formula given a constraint $\Sigma$-theory $T$ over lexicon $([\Sigma,D],\rho,\phi)$ as follows: an SMT formula $P$ over vocabulary $\sigma=\sigma_{r}\cup\sigma_{i}$ is a triple $\langle F,T,\mu\rangle$, where $F$ is a propositional formula over $\sigma$, $T$ is a $\Sigma$-theory, and $\mu$ is an injective function from irregular atoms $\sigma_{i}$ to constraint literals over c-vocabulary $[\Sigma,D]$. Note how the only difference in this definition is that function $\mu$ refers to domain $D$ of lexicon in place of an empty set. The definition of ASPT program can be extended in the same style. For the case of uniform theories, we will assume the definitions of SMT formulas and ASPT programs as stated in this paragraph.

6 SMT Formulas versus Constraint Formulas and ASPT versus CAS Programs

The framework of uniform theories brings us to a straightforward relation between SMT formulas over uniform theories and constraint formulas and between CAS programs and ASPT programs. We now formalize these statements.

Let $\mathcal{L}$ denote a lexicon $([\Sigma,D],\rho,\phi)$. By $\mathcal{B}_{\mathcal{L}}$ we denote the set of all constraints over $\mathcal{L}$. By $T_{\mathcal{L}}$ we denote the uniform $\Sigma$-theory over $\mathcal{L}$.

Theorem 6.25**.**

For a lexicon $\mathcal{L}=([\Sigma,D],\rho,\phi)$, a vocabulary $\sigma=\sigma_{r}\cup\sigma_{i}$, and a set $X$ of atoms over $\sigma$, set $X$ is a model of SMT formula $\langle F,T_{\mathcal{L}},\mu\rangle$ over $\sigma$ if and only if $X$ is a model of a constraint formula $\langle F,\mathcal{B}_{\mathcal{L}},\mu\rangle$ over $\sigma$ (where $\mu$ is identified with the function from irregular atoms to constraints over $\mathcal{L}$ in a trivial way.)

Proof 6.26**.**

Let $X$ be a subset of $\mathit{At}(F)$. Set $X$ is a model of an SMT formula $\langle F,T_{\mathcal{L}},\mu\rangle$ over $\sigma$ if and only if

$X$* is a model of $F$, and* 2. 2.

the following restriction formula

[TABLE]

is satisfiable in $\Sigma$-theory $T_{\mathcal{L}}$.

By the definition of a model of a constraint formula, to conclude the proof, we only have to illustrate that condition 2 holds if and only if the GCSP (31) over $\mathcal{L}$ has a solution. By Statement 3 of Theorem 4.21 we conclude that GSCP (31) has a solution if and only if restriction formula (31) is satisfiable in $\Sigma$-theory $T_{\mathcal{L}}$ (which is the case if and only if condition 2 holds).

This theorem illustrates that for uniform theories the languages of SMT formulas and constraint formulas practically coincide. In other words, constraint formulas is a special case of SMT formulas that are defined over uniform theories. It is obvious that a similar relation between CAS and ASPT programs holds.

Theorem 6.27**.**

For a lexicon $\mathcal{L}=([\Sigma,D],\rho,\phi)$, a vocabulary $\sigma=\sigma_{r}\cup\sigma_{i}$, and a set $X$ of atoms over $\sigma$, set $X$ is an answer set of ASPT program $\langle\Pi,T_{\mathcal{L}},\mu\rangle$ over $\sigma$ if and only if $X$ is an answer set of a CAS program $\langle\Pi,\mathcal{B}_{\mathcal{L}},\mu\rangle$ over $\sigma$ (where $\mu$ is identified with the function from irregular atoms to constraints over $\mathcal{L}$ in a trivial way.)

The proof for this theorem follows the lines of proof of Theorem 6.25.

Example 6.28**.**

Recall Examples 3.7 and 3.16. Let $T_{\mathcal{L}_{3}}$ denote the uniform theory over integer lexicon $\mathcal{L}_{3}$ defined in Example 3.7.

By Theorem 6.27, CAS program $P_{1}=\langle\Pi_{1},\mathcal{B}_{\mathcal{L}_{3}},\gamma_{1}\rangle$ from Example 3.7 is essentially the same entity as ASPT program $\langle\Pi_{1},T_{\mathcal{L}_{3}},\gamma_{1}\rangle$. These programs have the same answer sets.

Similarly, by Theorem 6.25, constraint formula

[TABLE]

from Example 3.16 is essentially the same entity as SMT formula

[TABLE]

We call any SMT formula $\langle F,T,\mu\rangle$ over $\sigma_{r}\cup\sigma_{i}$

• •

an SMT(IL)  formula if $T$ is the uniform theory over an integer lexicon and $\mu$ maps irregular atoms $\sigma_{i}$ into integer linear constraints;

• •

an SMT(DL) formula if $T$ is the uniform theory over an integer lexicon and $\mu$ maps irregular atoms $\sigma_{i}$ into difference logic constraints;

• •

an SMT(L)  formula if $T$ is the uniform theory over a numeric lexicon and $\mu$ maps irregular atoms $\sigma_{i}$ into linear constraints.

In the same style, we can define ASPT(IL), ASPT(DL), and ASPT(L) programs.

From Theorem 6.27, CAS programs of the form $\langle\Pi,\mathcal{B}_{\mathcal{L}},\gamma\rangle$, where $\mathcal{L}$ is a numeric lexicon and $\mathcal{B}_{\mathcal{L}}$ is the set of all linear constraints over $\mathcal{L}$, are essentially the same objects as ASPT(L) programs. Similarly, it follows that CAS programs of the form $\langle\Pi,\mathcal{B}_{\mathcal{L}},\gamma\rangle$, where $\mathcal{L}$ is an integer lexicon and $\mathcal{B}_{\mathcal{L}}$ is the set of all integer linear constraints over $\mathcal{L}$, are essentially the same objects as ASPT(IL) programs.

Obviously, Theorems 3.17 and 6.25 pave the way for using SMT systems that solve SMT(IL) and SMT(L) problems as is for solving tight ASPT(IL) and ASPT(L) programs respectively. It is sufficient to compute the input completion of the program relative to irregular atoms. Susman and Lierler (2016) utilized this method in implementing SMT-based solver for tight programs called ezsmt. A similar observation has been used 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.

6.1 Outlook on Constraint Answer Set Solvers

We now relate various constraint answer set solvers by specifying which ASPT languages these solvers support. We also provide a brief overview of a variety of solving techniques that they use.

Table 3 presents the landscape of current constraint answer set solvers. 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). Symbol $\dagger$ that annotates the languages supported by system mingo represents the fact that this solver supports lexicons that are not covered by our framework. Its variables within the same program can be of two different kind: either integer or real.

At a high-level abstraction, one may summarize the architectures of the clingcon and ezcsp solvers as ASP-based solvers plus theory solver. Given a CAS program $\langle\Pi,\mathcal{B},\gamma\rangle$, both clingcon and ezcsp first use an answer set solver to partially compute an input answer set of $\Pi$. 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(IL) and 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 ezsmt solver is only capable of processing tight programs. It computes clausified input completion for such CAS programs, encodes resulting SMT formula in SMT-LIB language Barrett et al. (2015) and is then able to invoke any SMT solver that supports SMT-LIB (for instance, SMT solvers z3 De Moura and Bjørner (2008) or cvc4 Barrett et al. (2011)) to compute its 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 clingcon 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 usually 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) and ASPT(IL) programs, hints that a similar strategy can be implemented for solving SMT(L) formulas. These ideas have been explored by King et al. (2014).

7 SMT Solvers for Nontight Programs via Level Rankings

As mentioned in section on preliminaries, Niemelä (2008) characterized answer sets of normal logic programs in terms of level rankings. He then developed a mapping from such programs to SMT(DL) formalism. Mappings of the kind were exploited in the design of solvers dingo Janhunen et al. (2011) and mingo Liu et al. (2012). In this section, we devise a similar mapping and show how it provides means for using SMT solvers for processing non-tight ASPT(IL) programs.

We start by defining level ranking relative to an input vocabulary and then lifting the result of Theorem 1 to the notion of input answer set.

Definition 7.29**.**

A function $\hbox{lr}:X\setminus\iota\rightarrow\mathbb{N}$ is a level ranking of $X$ for $\Pi$ relative to vocabulary $\iota\subseteq\sigma$ so that $\mathit{hd}(\Pi)\cap\iota=\emptyset$, when for each atom $a$ in $X\setminus\iota$ the following condition hold: there is $B$ in $Bodies(\Pi,a)$ such that $X$ satisfies $B$ and for every $b\in B^{+}\setminus\iota$ it holds that $\text{\hbox{lr}}(a)-1\geq\text{lr}(b)$.

Theorem 7.30**.**

For a program $\Pi$ over vocabulary $\sigma$, vocabulary $\iota\subseteq\sigma$ so that $\mathit{hd}(\Pi)\cap\iota=\emptyset$, and a set $X$ of atoms over $\sigma$ that is a model of input completion $IComp(\Pi,\iota)$, $X$ is an input answer set of $\Pi$ relative to $\iota$ if and only if there is a level ranking of $X$ for $\Pi$ relative to $\iota$.

Proof 7.31**.**

Consider a set $X$ of atoms over $\sigma$ that is a model of $IComp(\Pi,\iota)$. By Lemma 3.12 it follows that $X$ is a model of

[TABLE]

Left-to-right: Assume set $X$ is an input answer set of $\Pi$ relative to $\iota$. By the definition of an input answer set, $X$ is an answer set of the program

[TABLE]

By Theorem 1, it follows that there is a level ranking of $X$ for program (33). Thus, by Definition 1 there is a function lr: $X\rightarrow\mathbb{N}$ such that for each $a\in X$, there is $B$ in $Bodies(\Pi\cup(X\cap\iota),a)$ such that $X$ satisfies $B$ and for every $b\in B^{+}$ it holds that $\hbox{lr}(a)-1\geq\hbox{lr}(b)$. It is easy to see that for each atom $a$ in $X\setminus\iota$,

[TABLE]

Thus, for each atom $a$ in $X\setminus\iota$ there is $B$ in $Bodies(\Pi,a)$ such that $X$ satisfies $B$ and for every $b\in B^{+}$ it holds that $\hbox{lr}(a)-1\geq\hbox{lr}(b)$, and hence for every $b\in B^{+}\setminus\iota$ it holds that $\hbox{lr}(a)-1\geq\hbox{lr}(b)$. By Definition 7.29, lr (seen as a function from $X\setminus\iota$ to $\mathbb{N}$) is a level ranking of $X$ for $\Pi$ relative to $\iota$.

Right-to-left: Assume there is a level ranking lr of $X$ for $\Pi$ relative to $\iota$. By Definition 7.29, for each atom $a$ in $X\setminus\iota$ there is $B$ in $Bodies(\Pi,a)$ such that $X$ satisfies $B$ and for every $b\in B^{+}\setminus\iota$ it holds that $\hbox{lr}(a)-1\geq\hbox{lr}(b)$.

We now construct function $\hbox{lr}^{\prime}:X\rightarrow\mathbb{N}$ based of lr. We then illustrate that $\hbox{lr}^{\prime}$ is a level ranking of $X$ for program (33).

For every atom $a$ in $X\cap\iota$, $\hbox{lr}^{\prime}(a)=0$. For every atom $a$ in $X\setminus\iota$, $\hbox{lr}^{\prime}(a)=\hbox{lr}(a)+1$. It is easy to see that

[TABLE]

Thus $\hbox{lr}^{\prime}$ is a function from $X$ to $\mathbb{N}$. Consider two cases.

Case 1. Atom $a$ in $X\cap\iota$. Since $\mathit{hd}(\Pi)\cap\iota=\emptyset$, $a$ does not appear in any head in $\Pi$ (i.e., $a\not\in\mathit{hd}(\Pi)$) and thus it only appears as a fact in $\Pi\cup(X\cap\iota)$. Trivially, level ranking condition for this atom is satisfied.

Case 2. Atom $a$ in $X\setminus\iota$. It is easy to see that for such an atom equality (34) holds. We are given that there is $B$ in $Bodies(\Pi,a)$ such that $X$ satisfies $B$ and for every $b\in B^{+}\setminus\iota$ it holds that $\hbox{lr}(a)-1\geq\hbox{lr}(b)$. From $\hbox{lr}^{\prime}$ construction, it follows that for every $b\in B^{+}\setminus\iota$ it holds that $\hbox{lr}^{\prime}(a)-1\geq\hbox{lr}^{\prime}(b)$. On the other hand, for every atom $b$ in $B^{+}$ that it is not in $B^{+}\setminus\iota$, such $b$ is in $X\cap\iota$. By $\hbox{lr}^{\prime}$ construction, $\hbox{lr}^{\prime}(b)=0$ and $\hbox{lr}^{\prime}(a)=\hbox{lr}(a)+1$. Since lr is a mapping to natural numbers we derive that $\hbox{lr}(a)\geq 0$ and hence $\hbox{lr}^{\prime}(a)\geq 1$. Thus, $\hbox{lr}^{\prime}(a)-1\geq\hbox{lr}^{\prime}(b)$ holds. This concludes our illustration that for every atom $a\in X$ the level ranking condition holds given function $\hbox{lr}^{\prime}$.

By Theorem 1 we conclude that $X$ is an answer set of program (33). Consequently, $X$ is an input answer set of $\Pi$ relative to $\iota$.

We now present a mapping from a logic program to SMT(IL) formula inspired by the mapping introduced by Niemelä (2008). The mapping $T(\Pi,\iota)$ consists of input-completion $IComp(\Pi,\iota)$ and ranking-formula $R(\Pi,\iota)$ defined below. Sometimes, we refer to the set of formulas as a formula, where we understand such a formula as a conjunction of the members of its set.

In defining $R(\Pi,\iota)$, we will use the convention discussed earlier so that vertical bars mark the irregular atoms that have intuitive mappings into respective integer linear constraints. For instance, expression $|lr_{b}-1\geq lr_{a}|$ introduces an irregular atom that is intuitively mapped into integer linear constraint $lr_{b}-1\geq lr_{a}$, where $lr_{a}$ and $lr_{b}$ are variables over integers. Expression $R(\Pi,\iota)$ is a conjunction of formulas constructed as follows: for each atom $a\in\sigma\setminus\iota$

[TABLE]

By $\sigma_{i}^{R(\Pi,\iota)}$ we denote the set of all irregular atoms of the form $|lr_{a}-1\geq lr_{b}|$ in $R(\Pi,\iota)$. By $\Sigma^{R(\Pi,\iota)}$ we denote the set of all variables over integers occurring within $\sigma_{i}^{R(\Pi,\iota)}$. By $\gamma^{R(\Pi,\iota)}$ we denote a mapping from irregular atoms in $\sigma_{i}^{R(\Pi,\iota)}$ to integer linear constraints in accordance to their intuitive meanings. By $\mathcal{B}_{R(\Pi,\iota)}$ we denote the set of all integer linear constraints over integer lexicon defined over the signature $\Sigma^{R(\Pi,\iota)}$.

Theorem 7.32**.**

For a program $\Pi$ over vocabulary $\sigma$, vocabulary $\iota\subseteq\sigma$ so that $\mathit{hd}(\Pi)\cap\iota=\emptyset$, and a set $X$ of atoms over $\sigma$, $X$ is an input answer set of $\Pi$ relative to $\iota$ if and only if there is a model $X\cup X_{i}$ of a constraint formula (or SMT(IL) formula)

[TABLE]

over $\sigma\cup\sigma_{i}^{R(\Pi,\iota)}$ so that $X_{i}\subseteq\sigma_{i}^{R(\Pi,\iota)}$.

Proof 7.33**.**

Left-to-right: Assume $X$ is an input answer set of $\Pi$ relative to $\iota$. By Theorem 3.11 it follows that $X$ satisfies $IComp(\Pi,\iota)$. By Theorem 7.30 there is a level ranking lr of $X$ relative to $\iota$. Consider such lr. By the level ranking definition, for each atom $a$ in $X\setminus\iota$ the following condition holds, there is $B$ in $Bodies(\Pi,a)$ such that $X$ satisfies $B$ and for every $b\in B^{+}\setminus\iota$ it holds that $\text{\hbox{lr}}(a)-1\geq\text{lr}(b)$. We now construct set $X_{i}$ of atoms over $\sigma_{i}^{R(\Pi,\iota)}$ as follows: atom $|lr_{a}-1\geq lr_{b}|$ from $\sigma_{i}^{R(\Pi,\iota)}$ is in $X_{i}$ if and only if condition $\text{\hbox{lr}}(a)-1\geq\text{lr}(b)$ holds.

It follows immediately from the construction of $X_{i}$ that the GCSP which corresponds to $X\cup X_{i}$ (in accordance with the condition 2 in the definition of a model of a constraint formula) has a solution. Indeed, consider a valuation $\nu$ that assigns values to variables of the form $lr_{a}$ in $\Sigma^{R(\Pi,\iota)}$ based on level ranking function lr. In particular, $\hbox{lr}_{a}^{\nu}=\hbox{lr}(a)$.

We are now left to illustrate that $X\cup X_{i}$ is a model of $IComp(\Pi,\iota)\wedge R(\Pi,\iota)$. Since $X$ is a model of $IComp(\Pi,\iota)$, we are only left to show that $X\cup X_{i}$ is a model of $R(\Pi,\iota)$ or, in other words, that $X\cup X_{i}$ satisfies (35) for every atom $a\in\sigma\setminus\iota$.

Consider any atom $a\in\sigma\setminus\iota$.

Case 1. $a\not\in X$. Obviously, $a\not\in X_{i}$ since $X_{i}\cap\sigma=\emptyset$. Then, $X\cup X_{i}$ trivially satisfies (35).

Case 2. $a\in X\setminus\iota$. Since lr is a level ranking of $X$ relative to $\iota$ it follows that there is $B\in Bodies(\Pi,a)$ so that $X\models B$ and for every $b\in B^{+}\setminus\iota$ it holds that $\text{\hbox{lr}}(a)-1\geq\text{lr}(b)$. Take such $B$.

Case 2.1 $B^{+}\setminus\iota=\emptyset$. Then, $X$ satisfies (35) due to

[TABLE]

term in the right hand side of the implication (35) and the fact that $X$ satisfies considered $B$. Consequently, $X\cup X_{i}$ satisfies (35).

Case 2.2 $B^{+}\setminus\iota\neq\emptyset$. From the construction of $X_{i}$, it follows that for every $b\in B^{+}\setminus\iota$ there is an irregular atom of the form $|\text{\hbox{lr}}(a)-1\geq\text{lr}(b)|$ in $X_{i}$. Then, $X\cup X_{i}$ satisfies (35) due to

[TABLE]

term in the right hand side of the implication (35).

Right-to-left: Let $X\cup X_{i}$ be a model of constraint formula (36). It immediately follows that $X$ is a model of $IComp(\Pi,\iota)$. We now show that one can construct a level ranking lr of $X$ for $\Pi$ relative to $\iota$ using $X_{i}$. Indeed, consider a GCSP that corresponds to $X\cup X_{i}$ (in accordance with the condition 2 in the definition of a model of a constraint formula). Since $X\cup X_{i}$ is a model of (36) that GCSP has a solution. We use such a solution $\nu$ to construct level ranking lr for each atom $a$ in $X\setminus\iota$ as follows:

[TABLE]

To verify that lr is indeed a level ranking of $X$ for $\Pi$ relative to $\iota$ using $X_{i}$ we have to illustrate that for every atom $a\in X\setminus\iota$ there is $B\in Bodies(\Pi,a)$ such that $X$ satisfies $B$ and for every $b\in B^{+}\setminus\iota$ it holds that $\hbox{lr}(a)-1\geq\hbox{lr}(b)$. Consider any atom $a\in X\setminus\iota$. We are given that $X\cup X_{i}$ is a model of $R(\Pi,\iota)$. Thus, the right hand side of the implication (35) is satisfied for chosen atom $a$. It follows that there is $B\in Bodies(\Pi,a)$ such that $X\models B$ and for every $b\in B^{+}\setminus\iota$, $X_{i}$ contains the following irregular atom $|lr_{a}-1\geq lr_{b}|$. From the fact that $\nu$ is a solution to the GCSP that includes an integer linear constraint $lr_{a}-1\geq lr_{b}$ it follows that inequality $lr_{a}^{\nu}-1\geq lr_{b}^{\nu}$ holds. By lr construction we conclude that $\hbox{lr}(a)-1\geq\hbox{lr}(b)$.

By Theorem 7.30, $X$ is an input answer set of $\Pi$ relative to $\iota$.

Theorem 7.34**.**

Let $\mathcal{L}$ be an integer lexicon and $\mathcal{B}_{\mathcal{L}}$ be the set of all integer linear constraints over $\mathcal{L}$. For a CASP Program (or, an ASPT(IL) program) $P=\langle\Pi,\mathcal{B}_{\mathcal{L}},\gamma\rangle$ over vocabulary $\sigma=\sigma_{r}\cup\sigma_{i}$, and a set $X$ of atoms from $\sigma$, $X$ is an answer set of $P$ if and only if there is a model $X\cup X_{i}$ of a constraint formula (or SMT(IL formula))

[TABLE]

over $\sigma_{r}\cup\sigma_{i}\cup\sigma_{i}^{R(\Pi,\iota)}$ so that $X_{i}$ is the set of atoms over $\sigma_{i}^{R(\Pi,\iota)}$ and $\gamma^{\prime}$ is such that it coincides with $\gamma$ on atoms in $\sigma_{i}$ and with $\gamma^{R(\Pi,\iota)}$ on atoms from $\sigma_{i}^{R(\Pi,\iota)}$.

Proof of Theorem 7.34 follows the lines of proof for Theorem 7.32.

Theorem 7.34 paves the way for using SMT solvers for computing answer sets for arbitrary ASPT(IL) programs. Niemelä (2008) introduced the notions of strong level ranking and also illustrated how strongly connected components of a dependency graph of a normal program can be used to enhance the transformation from a normal program to an SMT(DL) formula. Similar ideas could be used for enhancing the proposed translation from ASPT(IL) to SMT(IL) formalism. Such enhancements are of essence when implementation of SMT-based solver for nontight ASPT(IL) programs is considered. Implementing such enhancements is the direction of future work.

8 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 uniform theories widely used in SMT practice. Given such theories, CASP and SMT solving share more in common than meets the eye. Based on this unification, we open the doors for writing programs in the CASP formalism, while allowing SMT solving technologies to be utilized. In these settings, CASP can be seen as a possible general-purpose declarative programming front-end for SMT technology. In the future, we would like to investigate a similar link to a related formalism of HEX-programs Eiter et al. (2012). Overall, 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.