Functional Stable Model Semantics and Answer Set Programming Modulo Theories

1 Introduction

In answer set programming (ASP), variables are understood in terms of grounding, and this limits answer sets to Herbrand models, under which interpretations of functions are pre-defined: every ground term represents itself, and is distinct from each other. Nonmonotonicity of the stable model semantics is related to minimizing the extents of predicates, but has nothing to do with functions, which forces us to represent the concept of nonBoolean fluents indirectly in terms of predicates, and not by functions. A drawback of such representation is that grounding often becomes a bottleneck in computation as the value domain of a nonBoolean fluent gets large.

There are two recent groups of work to extend the stable model semantics, each of which focuses only on one aspect of the issues above. One group is interested in enriching the modeling language by incorporating "intensional" functions [Cabalar, 2011; Lifschitz, 2012; Bartholomew and Lee, 2012; Balduccini, 2012]. Intensional functions are functions whose values can be described by other functions and predicates, rather than being pre-defined. Such semantics allow us to represent nonBoolean fluents by intensional functions without having to rely on predicates.

The other group of work focuses on improving the computational efficiency by integrating ASP with other declarative computing paradigms, such as constraint processing, satisfiability modulo theories, or mixed integer programming [Gebser et al., 2009; Balduccini, 2009; Janhunen et al., 2011; Liu et al., 2012], and exploiting the efficient constraint processing techniques on functions (or called "variables" in CSP/SMT) without having to generate a large set of ground instances. Constraint variables are functions that are mapped to values in their domains. In SMT with difference logic or linear constraints, arithmetic variables are functions that are mapped to numbers. However, these functions are not as expressive as intensional functions.

This paper combines the advantages of the two groups of work resulting in the framework of Answer Set Programming Modulo Theories (ASPMT)-a tight integration of answer set programming and satisfiability modulo theories, where functions are as expressive as predicates in answer set programming, and can be computed efficiently without having to ground w.r.t. their value domains. The existing languages in the second group can be viewed as special cases of this language. A fragment of ASPMT can be translated into the language of SMT, allowing SMT solvers to be used for computation.

Section 2 reviews the functional stable model semantics by Bartholomew and Lee [2012]. Section 3 presents a reformulation of this semantics in terms of grounding and reduct for infinitary ground formulas. In Section 4 we define the concept of ASPMT as a special case of the functional stable model semantics, and presents a syntactic class of ASPMT instances that can be translated into SMT instances, which in turn allows us to use SMT solvers to compute ASPMT. In Section 5 we compare ASPMT with other similar approaches, clingcon programs and ASP(LC) programs.

2 Functional Stable Model Semantics

2.1 Review of the Bartholomew-Lee Semantics

We review the stable model semantics of intensional functions from [Bartholomew and Lee, 2012]. Formulas are built the same as in first-order logic. A signature consists of function constants and predicate constants. Function constants of arity 0 are called object constants, and predicate constants of arity 0 are called propositional constants.

Similar to circumscription, for predicate symbols (constants or variables) u and c, expression u ≤ c is defined as shorthand for ∀x(u(x) → c(x)). Expression u = c is defined as ∀x(u(x) ↔ c(x)) if u and c are predicate symbols, and ∀x(u(x) = c(x)) if they are function symbols. For lists of symbols u = (u1, . . . , un) and c = (c1, . . . , cn), expression u ≤ c is defined as (u1 ≤ c1)∧· · ·∧(un ≤ cn), and similarly, expression u = c is defined as (u1 = c1) ∧ · · · ∧ (un = cn). Let c be a list of distinct predicate and function constants, and let ̂c be a list of distinct predicate and function variables corresponding to c. By cpred (cfunc , respectively) we mean the list of all predicate constants (function constants, respectively) in c, and by ̂cpred (̂cfunc , respectively) the list of the corresponding predicate variables (function variables, respectively) in ̂c.

For any formula F, expression SM[F; c] is defined as

where ̂c < c is shorthand for (̂cpred ≤ cpred ) ∧ ¬(̂c = c), and F ∗ (̂c) is defined recursively as follows.

• When F is an atomic formula, F ∗ is F ′ ∧ F where F ′ is obtained from F by replacing all intensional (function and predicate) constants c in it with the corresponding (function and predicate) variables from ̂c;
• (G∧H)∗ = G∗ ∧H∗ ; (G∨H)∗ = G∗ ∨H∗ ;
• (G→H)∗ = (G∗ →H∗ ) ∧ (G→H);
• (∀xG)∗ = ∀xG∗ ; (∃xF)∗ = ∃xF ∗ .

(We understand ¬F as shorthand for F → ⊥; ⊤ as ¬⊥; and F ↔ G as (F → G) ∧ (G → F ).) Members of c are called intensional constants.

When F is a sentence, the models of SM[F; c] are called the stable models of F relative to c. They are the models of F that are "stable" on c. The definition can be easily extended to formulas of many-sorted signatures.

This definition of a stable model is a proper generalization of the one from [Ferraris et al., 2011], which views logic programs as a special case of first-order formulas.

We will often write G ← F , in a rule form as in logic programs, to denote the universal closure of F → G. A finite set of formulas is identified with the conjunction of the formulas in the set.

Example 1 The following set F of formulas describes the capacity of a container of water that has a leak but that can be refilled to the maximum amount, say 10, with the action FillUp.

Here Amount1 is an intensional function constant, and x is a variable ranging over nonnegative integers. According to the semantics from [Bartholomew and Lee, 2012], the first rule is a default rule (or choice rule) standing for

and expresses that the amount at next time decreases by default. However, if FillUp action is executed (if we add FillUp as a fact), this behavior is overridden, and the amount is set to the maximum value.

Consider an interpretation I that has the set of nonnegative integers as the universe, interprets integers, arithmetic functions and comparison operators in the standard way, and has FillUpI = FALSE, AmountI0 = 6, AmountI1 = 5. One can check that I is a model of SM[F; Amount1]. Consider another interpretation I1 that agrees with I except that AmountI1 1 = 8. This is a model of F but not of SM[F; Amount1]. Another interpretation I2 that agrees with I except that FillUpI2 = TRUE, AmountI2 1 = 10 satisfies SM[F ; Amount1].

This example demonstrates the ability to assign a default value to an intensional function, which is different from the previous value of the function.

3 FSM in terms of Grounding and Reduct

Instead of relying on a transformation into second-order logic, the definition of a stable model in the previous section can be characterized in terms of grounding and reduct. While the definition in terms of second-order logic is succinct, the reduct-based definition is more familiar, and tells us some other insights.

3.1 Review: Infinitary ground Formulas

Since the universe can be infinite, grounding a quantified sentence introduces infinite conjunctions and disjunctions over the elements in the universe. Here we rely on the concept of grounding relative to an interpretation from [Truszczynski, 2012]. The following is the definition of an infinitary ground formula, which is adapted from [Truszczynski, 2012]. The main difference between them is that we do not replace ground terms with their corresponding object names, leaving intensional functions in grounding. This is essential for defining a reduct for the functional stable model semantics.

For each element ξ of the universe |I| of I, we introduce a new symbol ξ ⋄ , called an object name. By σI we denote the signature obtained from σ by adding all object names ξ ⋄ as additional object constants. We will identify an interpretation I of signature σ with its extension to σI defined by I(ξ ⋄ ) = ξ. 1

We assume the primary connectives to be ⊥, {}∧, {}∨, and →. Propositional connectives ∧, ∨, ¬,⊤ are considered as shorthands: F ∧ G as {F, G}∧; F ∨ G as {F, G}∨.

Let A be the set of all ground atomic formulas of signature σ. The sets F0,F1, . . . are defined recursively as follows:

• F0 = A∪ {⊥};
• Fi+1(i ≥ 0) consists of expressions H∧ and H∨, for all subset H of F0 ∪ . . . ∪ Fi, and of the expressions F → G, where F, G ∈ F0 ∪ · · · ∪ Fi.

We define Linf A = ⋃∞i=0 Fi. We call elements of Linf A infinitary ground formulas of σ.

For any interpretation I of σ and any infinitary ground formula F, the definition of satisfaction, I |= F, is as follows:

1 For details, see [Lifschitz et al., 2008].

• For atomic formulas, the definition is the same as in the standard first-order logic;
• I |=H∧ if for every formula G ∈ H, I |= G;
• I |=H∨ if there is a formula G ∈ H such that I |= G;
• I |= G→H if I ̸|= G or I |=H.

Let F be any first-order sentence of a signature σ, and let I be an interpretation of σ. By grI[F] we denote the infinitary ground formula w.r.t. I, which is obtained from F by the following process:

• If F is an atomic formula, grI[F] is F;
• grI[F ⊙G] = grI[F] ⊙ grI[G] (⊙ ∈ {∧, ∨,→});
• grI[∀xF(x)] = {grI[F(ξ ⋄ )] | ξ ∈ |I|}∧;
• grI[∃xF(x)] = {grI[F(ξ ⋄ )] | ξ ∈ |I|}∨.

Note that grI [F ] is an infinitary ground formula of σI .

Example 1 continued Consider again F in Example 1, and the same interpretation I there. grI(F) is the following set

3.2 Reduct-Based Definition of SM

For any two interpretations I, J of the same signature and any list c of distinct predicate and function constants, we write J <c I if

• J and I have the same universe and agree on all constants not in c;
• pJ ⊆ pI for all predicate constants p in c; and
• J and I do not agree on c.

The reduct F I of an infinitary ground formula F relative to an interpretation I is defined as follows:

• For each atomic formula F, F I = ⊥ if I ̸|= F and F I = F otherwise;
• (H∧)I = ⊥ if I ̸|= H∧; otherwise (H∧)I = {GI | G ∈ H}∧;
• (H∨)I = ⊥ if I ̸|= H∨; otherwise (H∨)I = {GI | G ∈ H}∨;
• (G → H)I = ⊥ if I ̸|= G → H; otherwise (G→H)I = GI →HI .

The following theorem states the reformulation of FSM in terms of grounding and reduct.

Theorem 1 Let F be a first-order sentence and c a list of intensional constants. For any interpretation I of σ, I |= SM[F; c] iff

• I satisfies F, and
• every interpretation J such that J <c I does not satisfy (grI [F ])I .

Example 1 continued Among the ground formulas in (2), only the implication

which stands for

has its antecedent satisfied by I, so the reduct (grI[F])I is equivalent to

No interpretation that is different from I only on Amount1 satisfies the reduct. On the other hand, the reduct (grI1 [F])I1 is equivalent to⊥∨¬⊥ ← Amount0=5+1,

and other interpretations that are different from I1 only on Amount1 satisfy the reduct. (grI2 [F])I2 is equivalent to

and I2 is the only interpretation that satisfies the reduct. In accordance with Theorem 1, I and I2 are the stable models of F relative to Amount1, but I1 is not.

4 Answer Set ProgrammingModulo Theories 4.1 ASPMT as a Special Case of FSM

Formally, an SMT instance is a formula in many-sorted firstorder logic, where some designated function and predicate constants are constrained by some fixed background interpretation. SMT is the problem of determining whether such a formula has a model that expands the background interpretation [Barrett et al., 2009].

The syntax of ASPMT is the same as that of SMT. Let σbg be the (many-sorted) signature of the background theory bg. An interpretation of σbg is called a background interpretation if it satisfies the background theory. For instance, in the theory of reals, we assume that σbg contains the set R of symbols for all real numbers, the set of arithmetic functions over real numbers, and the set {<,>,≤,≥} of binary predicates over real numbers. Background interpretations interpret these symbols in the standard way.

Let σ be a signature that is disjoint from σbg . We say that an interpretation I of σ satisfies F w.r.t. the background theory bg, denoted by I |=bg F, if there is a background interpretation J of σbg that has the same universe as I, and I ∪ J satisfies F. For any ASPMT sentence F with background theory σbg , interpretation I is a stable model of F relative to c (w.r.t. background theory σbg ) if I |=bg SM[F; c].

Example 1 continued Formula F can be understood as an ASPMT formula with the theory of integers as the background theory. Arithmetic functions and comparison operators belong to the background signature. If I ′ is an interpretation of signature {Amount0, Amount1, FillUp} which agrees with I on these constants, We say that I ′ |=bg SM[F ; Amount1].

4.2 Turning ASPMT into SMT for Tight Programs

We say that a formula F is in Clark normal form (relative to the list c of intensional constants) if it is a conjunction of sentences of the form

and

one for each intensional predicate p and each intensional function f, where x is a list of distinct object variables, y is an object variable, and G is an arbitrary formula that has no free variables other than those in x and y.

The completion of a formula F in Clark normal form (relative to c) is obtained from F by replacing each conjunctive term (3) with

and each conjunctive term (4) with

An occurrence of a symbol or a subformula in a formula F is called strictly positive in F if that occurrence is not in the antecedent of any implication in F. The t-dependency graph of F (relative to c) is the directed graph that

• has all members of c as its vertices, and
• has an edge from c to d if, for some strictly positive occurrence of G → H in F ,
• c has a strictly positive occurrence in H, and
• d has a strictly positive occurrence in G.

We say that F is tight (on c) if the t-dependency graph of F (relative to c) is acyclic. For example,

is tight on {p, q, r} because its t-dependency graph has only one edge, which goes from p to r. On the other hand, the formula is not tight according to [Ferraris et al., 2011] because, according to the definition of a dependency graph in that paper, there is an additional edge that goes from p to itself.

Theorem 12 from [Bartholomew and Lee, 2012] extended the theorem on completion from [Ferraris et al., 2011] to allow intensional functions, but it was restricted to a class of formulas called c-plain formulas. The following theorem generalizes that theorem by removing that restriction and by referring to the weaker notion of tightness as described above.

Theorem 2 For any sentence F in Clark normal form that is tight on c, an interpretation I that satisfies ∃xy(x ̸= y) is a model of SM[F; c] iff I is a model of the completion of F relative to c.

Example 1 continued Formula (1) is strongly equivalent to

so that formula F in Example 1 can be turned into Clark normal form relative to Amount1:

and the completion turns it into

Using equality, the formula can be written without mentioning the variable x as

In the language of iSAT, this formula can be represented as

(Amt = Amt'+1) or (Amt'=10 and FillUp); FillUp -> Amt'=10;

and in the language of Z3, it can be represented as

(assert (or (= Amt0 (+ Amt1 1)) (and (= Amt1 10) FillUp))) (assert (=> FillUp0 (= Amt1 10))) .

Alternatively, according to the method in [Bartholomew and Lee, 2012], formula F in Example 1 can be turned into the input language of GRINGO by eliminating intensional functions in favor of intensional predicates.

Our first experiment has the bucket initially at capacity 5 and the goal is to get the bucket to capacity 10 at a certain fixed timepoint. The different instance sizes correspond to the maximum capacity of the bucket and the certain timepoint (they are both the same in each case). iSAT finds a model of bounded length k, where k starts from 0 and increases by 1 until a model is found. The run time reported is the total cumulative times for k = 0, 1, . . . , m where m is the instance size. The last step time is for the run when k = m. For other systems, we fixed the length k = m from the beginning. The results shown in Table 1 demonstrate that even for a relatively simple domain, ASP suffers a grounding bottleneck that is not present when using SMT solvers. We see that the number of atoms for CLINGO increases quadratically to the instance size while the number of variables for iSAT increases linearly.

Next, consider the Gears World domain in which we have two gears, Gear1 with radius 7 and Gear2 with radius 17. Each gear is connected to a motor that has integral running speeds which can be incremented by 1 using the corresponding action. The gears can also be moved close together so that both gears spin at the speed of the higher value (between M1Speed × Radius1 or M2Speed × Radius2). The goal is to have Gear1 spinning at a multiple of Gear2's radius. That multiple is the instance size in Table 2, so for example, instance size 3 means at the end, we want Gear1 spinning at a speed of 51(= 3 × 17). This domain can be expressed in the language of ASPMT with the theory of integers. Here is a part of the program that governs the speed of a motor. The speed does not change unless the increase action happens, in which case it is incremented by 1 unit.

(t is a step counter, which can be represented by an ASP variable to be grounded).

The ASPMT description of the Gears World is tight and can be turned into the input language of SMT solvers by completion. For example, the completion relative to M1Speedt is

The Gears World domain can also be computed by ASP solvers by eliminating the intensional functions in favor of intensional predicates as described in [Bartholomew and Lee, 2012]. Table 2 compares the two approaches and reveals that the SMT solvers iSAT and Z3 were able to perform comparatively very well as the instance size increased.

The experiments were performed on an Intel Core 2 Duo CPU 3.00 GHz with 4 GB RAM.

5 Comparison with Other Approaches to ASP Modulo Theories

5.1 Clingcon programs as a special case of ASPMT

A constraint satisfaction problem (CSP) is a tuple (V,D, C), where V is a set of constraint variables with the respective domains D, and C is a set of constraints that specify legal assignments of values in the domains to the constraint variables.

A clingcon program Π with a constraint satisfaction problem (V,D,C) is a set of rules of the form

where a is a propositional atom or ⊥, B is a set of positive propositional literals, N is a set of negative propositional literals, and Cn is a set of constraints from C, possibly preceded by not.

Clingcon programs can be viewed as ASPMT instances. Below is a reformulation of the semantics in terms of ASPMT. We assume that constraints are expressed by ASPMT sentences of signature V ∪ σbg , where V is a set of object constants identified with constraint variables V in (V,D,C), whose value sorts are identified with domains in D; we assume that σbg is disjoint from V and contains all values in D as object constants, and other symbols to represent constraints, such as +, ×, and ≥. In other words, we represent a constraint as a formula F(v1, . . . , vn) over V ∪ σbg where F(x1, . . . , xn) is a formula of the signature σbg and F(v1, . . . , vn) is obtained from F(x1, . . . , xn) by substituting the object constants (v1, . . . , vn) in V for (x1, . . . , xn).

For any signature σ that consists of object constants and propositional constants, we identify an interpretation I of σ as the tuple 〈I f ,X〉, where I f is the restriction of I on the object constants in σ, and X is a set of propositional constants in σ that are true under I.

Given a clingcon program Π with (V,D,C), and an interpretation I = 〈I f ,X〉, we define the constraint reduct of Π relative to X and I f (denoted by ΠXI f ) as the set of rules a ← B for each rule (5) is in Π such that I f |=bg Cn, and X |= N. We say that a set X of propositional atoms is a constraint answer set of Π relative to I f if X is a minimal model of ΠXI f .

Example 1 continued The rules

are identified with

under the semantics of clingcon programs. Consider I in Example 1, which can be represented as 〈I f , X〉 where I f maps Amount0 to 6, and Amount1 to 5, and X = ∅. X is the constraint answer set relative to I f because X is the minimal model of the constraint reduct relative to X and I f , which is the empty set.

Similar to the way that rules are identified as a special case of formulas [Ferraris et al., 2011], we identify a clingcon program Π with the conjunction of implications B∧N ∧Cn → a for all rules (5) in Π. The following theorem tells us that clingcon programs are a special case of ASPMT, in which the background theory is specified by (V,D,C), and intensional constants are limited to propositional constants only, and do not allow function constants.

Theorem 3 Let Π be a clingcon program with CSP (V,D,C), let p be the set of all propositional constants occurring in Π, and let I be an interpretation 〈I f ,X〉 of signature V ∪ p. Set X is a constraint answer set of Π relative to I f iff I |=bg SM[Π; p].

Note that a clingcon program does not allow an atom that consists of elements from both V and p. Thus the truth value of any atom is determined by either I f or X, but not by involving both of them. This allows loose coupling of an ASP solver and a constraint solver. On the other hand, [Gebser et al., 2009] sketches a method to extend clingcon programs to allow predicate constants of positive arity, possibly containing constraint variables as arguments. This however leads to some unintuitive cases under the semantics of CLINGCON programs, as the following example shows.

$domain(100..199). % Office numbers myoffice(a). % a is my office number, :- myoffice(b). % and b is not. :- not a $==b. % Nevertheless, a equals b.

System CLINGCON does not notice that this set of assumptions is inconsistent. This is because symbols a and b in ASP atoms and the same symbols in the constraint are not related. On the other hand, ASPMT, which allows first-order signatures, does not have this anomaly; there is no stable model under ASPMT.

5.2 Comparison with ASP(LC) Programs by Liu et al.

[Liu et al., 2012] considers logic programs with linear constraints, or ASP(LC) programs, comprised of rules of the form

where a is a propositional atom or ⊥, B is a set of positive propositional literals, and N is a set of negative propositional literals, and LC is a set of theory atoms-linear constraints

xi is an object constant whose value sort is integers (or reals), and each ci, k is an integer (or real).

An ASP(LC) program Π can be viewed as an ASPMT formula whose background theory bg is the theory of integers or the theory of reals. Let σp denote the set of all propositional atoms occurring in Π and σf denote all object constants occurring in Π that do not belong to the background signature. Theory atoms are essentially ASPMT formulas of signature σf ∪ σbg . We identify ASP(LC) program Π with the conjunction of ASPMT formulas B ∧ N ∧ LC → a for all rules (6) in Π.

An LJN-intepretation is a pair (X, T) where X ⊆ σp and T is a subset of theory atoms occurring in Π such that there is some interpretation I of signature σf such that I |=bg T ∪T, where T is the set of negations of each theory atom occurring in Π but not in T . An LJN-interpretation (X, T) satisfies an atom b if b ∈ X, the negation of an atom not c if c /∈ X, and a theory atom t if t ∈ T. The notion of satisfaction is extended to other propositional connectives as usual.

The LJN-reduct of a program Π with respect to an LJNinterpretation (X, T), denoted by Π(X,T) , consists of rules a ← B for each rule (6) such that (X, T) satisfies N ∧ LC. (X, T) is an LJN-answer set of Π if (X, T) satisfies Π, and X is the smallest set of atoms satisfying Π(X,T) .

The following theorem tells us that there is a one-to-many relationship between LJN-answer sets and the stable models in the sense of ASPMT.

Theorem 4 Let Π be an ASP(LC) program, and σp and σf are defined as above.

• (a) If (X, T) is an LJN-answer set of Π, then for any interpretation 〈I f ,X〉 of signature σp ∪ σf such that I f |=bg T ∪ T, we have 〈I f ,X〉 |=bg SM[Π; σp ].
• (b) For any interpretation I = 〈I f , X〉 of signature σp ∪σf , if 〈I f ,X〉 |=bg SM[Π; σp ], then an LJN-interpretation (X, T ) where

is an LJN-answer set of Π.

Example 2 Let F be

The LJN-interpretation L = 〈{a}, {x-z >0}〉 is an answer set of F since {(x-z > 0, ¬(x-y ≤ 0), ¬(y-z ≤ 0)} is satisfiable (e.g. take xI = 2, yI = 1, zI = 0) and the set {a} is the minimal model satisfying the reduct F L = (⊤ → a) ∧ c → b. On the other hand the interpretation I such that xI = 2, yI = 1, zI = 0, aI = TRUE, bI = FALSE, cI = FALSE satisfies I |=bg SM[F; abc].

As with clingcon programs, ASP(LC) programs are more restrictive than ASPMT. ASP(LC) programs do not allow theory atoms in the head of a rule, and like clingcon programs, cannot express intensional functions.

6 Conclusion

In this paper, we related the two lines of research on functions in answer set programming that originated from different motivations, leading to an expressive KR formalism called ASPMT, which can be efficiently computed by SMT solvers. The relationship between ASPMT and SMT is similar to the relationship between ASP and SAT. We expect that, in addition to completion, many results known between ASP and SAT can be carried over to the relationship between ASPMT and SMT.

Acknowledgements

We are grateful to Yunsong Meng for useful discussions related to this paper. We are also grateful to the anonymous referees for their useful comments. This work was partially supported by the National Science Foundation under Grant IIS-0916116 and by the South Korea IT R&D program MKE/KIAT 2010-TD-300404-001.