Answer Set Programming Modulo Theories and Reasoning about Continuous Changes

1 Introduction

The success of answer set programming (ASP) [Lifschitz, 2008; Brewka et al., 2011] is in part thanks to efficiency of ASP solvers that utilize (i) intelligent grounding-the process that replaces variables with ground terms-and (ii) efficient search methods that originated from propositional satisfiability solvers (SAT solvers). However, this method is not scalable when we need to represent functional fluents that range over large numeric domains. Since answer sets (a.k.a. stable models) are limited to Herbrand models, functional fluents are represented by predicates, but not by functions, as in the following example that represents the inertia assumption on Speed:

Here the subscripts 0 and 1 are time stamps, and x is a variable ranging over the value domain of fluent Speed. A more natural representation using functions which replaces Speedi (x) with Speedi =x does not work under the ASP semantics because (i) answer sets are Herbrand models (e.g., Speed1 = Speed0 is always false under any Herbrand interpretation), and (ii) nonmonotonicity of the stable model semantics has to do with minimizing the extents of predicates but has nothing to do with functions. On the other hand, grounding rule (1) yields a large set of ground instances when Speed ranges over a large integer domain. Moreover, a real number domain is not supported because grounding cannot be applied.

In order to alleviate this "grounding problem," there have been several recent efforts to integrate ASP with constraint solving and satisfiability modulo theories (SMT), where functional fluents can be expressed by variables in Constraint Satisfaction Problems or uninterpreted constants in SMT. Balduccini [2009] and Gebser et al. [2009] combine ASP and constraint solving in a way that is similar to the "lazy approach" of SMT solvers. Niemel¨a [2008] shows that ASP programs can be translated into a particular SMT fragment, namely difference logic. Janhunen et al. [2011] presents a tight integration of ASP and SMT. All these approaches aim at addressing the issue (i) above by avoiding grounding and exploiting efficient constraint solving methods applied to functions. However, they do not address the issue (ii) because, like the standard ASP, nonmonotonicity of those extensions has to do with predicates only. For instance, a natural counterpart of (1) in the language of CLINGCON [Gebser et al., 2009],

does not correctly represent inertia.

In this paper, we present a framework of combining answer set programming with satisfiability modulo theories, which we call Answer Set Programming Modulo Theories (ASPMT). Just as SMT is a generalization of SAT and, at the same time, a special case of first-order logic in which certain predicate and function constants in background theories (such as difference logic and the theory of reals) have fixed interpretations, ASPMT is a generalization of the standard ASP and, at the same time, a special case of the functional stable model semantics [Bartholomew and Lee, 2012] that assumes background theories. Like the known relationship between SAT and ASP that tight ASP programs can be translated into SAT instances, tight ASPMT programs can be translated into SMT instances, which allows SMT solvers for computing ASPMT programs.

These results allow us to enhance action language C+ [Giunchiglia et al., 2004] to handle reasoning about continuous changes. Language C+ is an expressive action description language but its semantics was defined in terms of propositional causal theories, which limits the language to express discrete changes only. By reformulating C+ in terms of ASPMT, we naturally extend the language to overcome the limitation, and use SMT solvers to compute the language. Our experiments show that this approach outperforms the existing implementations of C+ by several orders of magnitude for some benchmark problems.

Section 2 reviews the functional stable model semantics by Bartholomew and Lee [2012], and defines ASPMT as its special case. Section 3 reformulates language C+ in terms of ASPMT, and Section 4 shows how the reformulation can be used to represent continuous changes. The language is further extended in Section 5 to represent cumulative effects on continuous resources. Related work and the conclusion are presented in Section 6.

2 Functional SMand ASPMT

2.1 Review: Functional Stable Model Semantics

We review the semantics 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 the list of the corresponding predicate variables 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]: in the absence of intensional function constants, it reduces to the one in [Ferraris et al., 2011].

2.2 Answer Set ProgrammingModulo Theories

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].

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 inertia assumption on the speed of a car and the effect of acceleration assuming the theory of reals as the background theory.

Here x is a variable of sort R≥0; Speed0 , Speed1 and Duration are object constants with value sort R≥0 and Accelerate is an object constant with value sort Boolean. For interpretation I of signature {Speed0 , Speed1 ,Duration, Accelerate} such that AccelerateI = FALSE, SpeedI0 = 1, SpeedI1 = 1, DurationI = 1.5, we check that I |=bg SM[F; Speed1 ].

For another interpretation I1 of the same signature that agrees with I except that AccelerateI1 = TRUE, SpeedI1 1 = 5.5, we check that I1 |=bg SM[F; Speed1 ].

2.3 Review: Completion

We review the theorem on completion from [Bartholomew and Lee, 2013], which turns the functional stable model semantics into first-order logic.

A formula F is said to be 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 ∀x(p(x) ↔ G) and each conjunctive term (4) with ∀xy(f (x)=y ↔ G).

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, formula (1) is tight on its signature.

Theorem 1 [Bartholomew and Lee, 2013, 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.

Theorem 1 can be applied to formulas in non-Clark normal form if they can be rewritten in Clark normal form. The following theorem is often useful in splitting conjunctive formulas, and applying completion to subformulas.

Theorem 2 [Bartholomew and Lee, 2012, Theorem 1] For any first-order formulas F and G, if G has no strictly positive occurrence of a constant from c, SM[F ∧G; c] is equivalent to SM[F ; c] ∧ G.

Theorem 1 is applicable to ASPMT formulas as well. Since F in Example 1 is tight on Speed1 , according to Theorem 1, SM[F; Speed1 ] is equivalent to the following SMT instance with the same background theory:

3 Reformulating C+ in ASPMT

3.1 Syntax

We consider a many-sorted first-order signature σ that is partitioned into three signatures: the set σfl of object constants called fluent constants, the set σact of object constants called action constants, and the background signature σbg . The signature σfl is further partitioned into the set σsim of simple fluent constants and the set σsd of statically determined fluent constants.

We assume the same syntax of formulas as in Section 2. A fluent formula is a formula of signature σfl ∪ σbg . An action formula is a formula of σact ∪ σbg that contains at least one action constant and no fluent constants.

A static law is an expression of the form

where F and G are fluent formulas. An action dynamic law is an expression of the form (5) in which F is an action formula and G is a formula. A fluent dynamic law is an expression of the form

where F and G are fluent formulas and H is a formula, provided that F does not contain statically determined constants. A causal law is a static law, or an action dynamic law, or a fluent dynamic law. A C+ action description is a finite set of causal laws.

For any function constant f, we say that a first-order formula is f-plain if each atomic formula in it

• does not contain f, or
• is of the form f(t) = t1 where t is a list of terms not containing f, and t1 is a term not containing f.

For any list c of predicate and function constants, we say that F is c-plain if F is f-plain for each function constant f in c.

We call an action description definite if the head F of every causal law (5) and (6) is an atomic formula that is (σfl∪σact )- plain. Throughout this paper we consider definite action descriptions only, which covers the fragment of C+ that is implemented in the Causal Calculator (CCALC) 1 .

3.2 Semantics

In [Giunchiglia et al., 2004] the semantics of C+ is defined in terms of nonmonotonic propositional causal theories, in which every constant has a finite domain. The semantics of the enhanced C+ below is similar to the one in [Giunchiglia et al., 2004] except that it is defined in terms of ASPMT in place of causal theories. This reformulation is essential for the language to represent continuous changes as it is not limited to finite domains only.

For a signature σ and a nonnegative integer i, expression i : σ is the signature consisting of the pairs i : c such that c ∈ σ, and the value sort of i : c is the same as the value sort of c. Similarly, if s is an interpretation of σ, expression i : s is an interpretation of i : σ such that cs = (i : c)i:s .

For any definite action description D of signature σfl ∪ σact ∪ σbg and any nonnegative integer m, the ASPMT program Dm is defined as follows. The signature of Dm is 0 : σfl ∪ · · · ∪ m: σfl ∪ 0 : σact ∪ · · · ∪ (m-1) : σact ∪ σbg . By i : F we denote the result of inserting i : in front of every occurrence of every fluent and action constant in a formula F .

ASPMT program Dm is the conjunction of

for every static law (5) in D and every i ∈ {0, . . . ,m}, and for every action dynamic law (5) in D and every i ∈ {0, . . . ,m-1};

1 http://www.cs.utexas.edu/ tag/ccalc/

for every fluent dynamic law (6) in D and every i ∈ {0, . . . ,m- 1}.

The transition system represented by an action description D consists of states (vertices) and transitions (edges). A state is an interpretation s of σfl such that 0:s |=bg SM[D0; 0:σsd ]. A transition is a triple 〈s, e, s′ 〉, where s and s′ are interpretations of σfl and e is an interpretation of σact , such that

Theorems 3 and 4 below extend Propositions 7 and 8 from [Giunchiglia et al., 2004] to our reformulation of C+. These theorems justify the soundness of the language.

The definition of the transition system above implicitly relies on the following property of transitions:

The following theorem states the correspondence between the stable models of Dm and the paths in the transition system represented by D:

Theorem 4

It is not difficult to check that ASPMT programDm that is obtained from action description D is always tight. In view of Theorem 1, Dm can be represented in the language of SMT as the next section demonstrates.

4 Reasoning about Continuous Changes in C+

In order to represent continuous changes in the enhanced C+, we distinguish between steps and real clock times. We assume the theory of reals as the background theory, and introduce a simple fluent constant Time with value sort R≥0, which denotes the clock time, and an action constant Dur with value sort R≥0, which denotes the time elapsed between the two consecutive states. We postulate the following causal laws:

These causal laws are shorthand for

where t, t′ are variables of sort R≥0. (See Appendix B in [Giunchiglia et al., 2004] for the abbreviations of causal laws.)

Continuous changes can be described as a function of duration using fluent dynamic laws of the form

Notation: d, v, v′ , t, t′ are variables of sort R≥0 A, MS are real numbers.

Simple fluent constants: Domains: Speed, Distance, Time R≥0 Action constants: Domains: Accelerate, Decelerate Boolean Dur R≥0 caused Speed=v+A×t after Accelerate ∧ Speed=v ∧ Dur=t caused Speed =v-A×t after Decelerate ∧ Speed =v ∧ Dur = t caused Distance=d+0.5×(v+v′ )×t if Speed=v′ after Distance =d ∧ Speed =v ∧ Dur = t constraint Time=t+t′ after Time=t ∧ Dur=t′ constraint Speed ≤ MS inertial Speed exogenous Time, c for every action constant c

Figure 1: Car Example in C+

where (i) c is a simple fluent constant, (ii) c, c′ are lists of fluent constants, (iii) x, x′ are lists of object variables, (iv) G is a formula, and (v) f(x, x′ , t) is a term constructed from σbg , and variables in x, x′ , and t.

For instance, the fluent dynamic law

describes how fluent Distance changes according to the function of real time.

Consider the following problem by Lifschitz (http://www.cs.utexas.edu/vl/tag/continuous problem).

If the accelerator of a car is activated, the car will speed up with constant acceleration A until the accelerator is released or the car reaches its maximum speed MS, whichever comes first. If the brake is activated, the car will slow down with acceleration -A until the brake is released or the car stops, whichever comes first. Otherwise, the speed of the car remains constant. The problem asks to find a plan satisfying the following condition: at time 0, the car is at rest at one end of the road; at time K, it should be at rest at the other end.

A C+ description of this example is shown in Figure 1. The

Notation: x, d, v, v′ , t, t′ are variables of sort R≥0; y is a variable of sort Boolean. Intensional object constants: i :Speed for i > 0 i+1:Speed=x ← (x = v+A×t) ∧ i : (Accelerate ∧ Speed =v ∧ Dur = t) i+1:Speed=x ← (x = v-A×t) ∧ i : (Decelerate ∧ Speed =v ∧ Dur = t) i+1:Distance=x ← (x = d+0.5×(v′ +v)×t) ∧ i+1:Speed=v′ ∧ i : (Speed=v ∧Distance=d ∧Dur=t) ⊥←¬(i+1:Time=t+t′ ) ∧ i : (Time=t ∧Dur=t′ ) ⊥ ← ¬(i : Speed ≤ MS) i+1 : Speed =x ← ¬¬(i+1 : Speed =x) ∧ i : Speed =x i : Time = t ← ¬¬(i : Time = t) i : c=y ← ¬¬(i : c=y) for every action constant c

actions Accelerate and Decelerate has direct effects on Speed and indirect effects on Distance. For an object constant c that has the Boolean domain, we abbreviate c = TRUE as c and c=FALSE as ∼c. According to the semantics in Section 3.2, the description is turned into an ASPMT program with the theory of reals as the background theory, which can be further rewritten in Clark normal form. Some occurrences of ¬¬ can be dropped without affecting stable models, which results in the program in Figure 2.

The program can be viewed as F ∧ G where F is the conjunction of the rules that has intensional constants in the heads, and G is the conjunction of the rest rules. In view of Theorem 2, the stable models and F ∧ G are the same as the stable models of F that satisfies G. By Theorem 1, F can be turned into completion. For example, the completion on i+1:Speed yields a formula that is equivalent to

i+1:Speed=x ↔ (x = (i :Speed+A×i :Dur) ∧ i :Accelerate) ∨(x = (i :Speed-A×i :Dur) ∧ i :Decelerate) ∨(i+1:Speed=x ∧ i :Speed=x).

Variable x in the formula can be eliminated by equivalent transformations using equality:

i : Accelerate → i+1 : Speed = (i : Speed+A×i : Dur) i : Decelerate → i+1 : Speed = (i : Speed-A×i : Dur) (i+1 : Speed = (i : Speed+A×i :Dur) ∧ i : Accelerate) ∨(i+1 : Speed = (i : Speed-A×i :Dur) ∧ i :Decelerate) ∨(i :Speed = i+1:Speed) .

The whole translation can be encoded in the input language of SMT solvers. The shortest plan found by iSAT (http://isat.gforge.avacs.org) on this input formula when the road length is 10, A = 3,MS = 4,K = 4 is shown in Figure 3.

5 Reasoning about Additive Continuous Resources in C+

Additive fluents are fluents with numerical values such that the effect of several concurrently executed actions on it can be computed by adding the effects of the individual actions. Lee and Lifschitz [2003] show how to describe additive fluents in C+ by understanding "increment laws" as shorthand for some causal laws. However, some additive fluents are realvalued, and cannot be represented in the language described in [Lee and Lifschitz, 2003] as the language is limited to finite domains only. This made the discussion of additive fluents in [Lee and Lifschitz, 2003] limited to integer domains only. For example, the effect of firing multiple jets on the velocity of a spacecraft is described by "increment laws"

Fire(j) increments Vel(ax) by n//Mass if Force(j, ax)=n .

Mass stands for an integer constant, and the symbol // stands for integer division; the duration of firing action is assumed to be 1, and all components of the position and the velocity vectors at any time are assumed to be integers, and even the forces applied have to be integers. Obviously these are too strong assumptions.

These limitations are not present in our enhanced C+ and its SMT-based computation. The representation in [Lee and Lifschitz, 2003] can be straightforwardly extended to handle continuous motions by distinguishing between steps and real time as in the previous section. For example, we can describe the effect that firing multiple jets has on the velocity of a spacecraft by

In general, additive fluent constants are simple fluent constants with numerical values with certain restrictions. First, the heads of static and fluent dynamic laws are not allowed to contain additive fluent constants. Second, the effects of concurrent execution of actions on additive fluents are expressed by increment laws-expressions of the form

a increments c by f(x, t) if (d,Dur)=(x, t) ∧G (8)

where (i) a is a Boolean action constant; (ii) c is an additive fluent constant; (iii) d is a list of fluent constants, and x is a list of corresponding variables; (iv) f(x, t) is an arithmetic expression over x and the duration t; (v) G is a formula that contains no Boolean action constants.

Similar to [Lee and Lifschitz, 2003], the semantics of increment laws is described by a translation that replaces increment laws with action dynamic laws (5) and fluent dynamic laws (6) using additional action constants. This translation largely repeats the one in [Lee and Lifschitz, 2003] and we omit the details due to lack of space.

The C+ encoding of the spacecraft example is shown in Figure 4.

Notation: j ∈ {J1, J2}, ax ∈ {X, Y, Z} x, y, y′ are variables of sort R; t, t′ are variables of sort R≥0 Additive fluent constants: Domains: Vel(ax) R Other Simple fluent constants: Domains: Pos(ax) R Time R≥0 Action constants: Domains: Fire(j) Boolean Force(j, ax) R Dur R≥0

Fire(j) increments Vel(ax) by (x/Mass) × t if Force(j, ax) = x ∧ Dur = t caused Pos(ax)=x+(0.5×(y+y′ )×t) if Vel(ax)=y′ after Pos(ax)=x ∧ Vel(ax)=y ∧ Dur =t always Force(j, ax)=0 ↔∼Fire(j) constraint Time=t+t′ after Time=t ∧ Dur=t′ exogenous Time exogenous c for every action constant c

Table 1 compares the performance of SMT-based computation of C+ and existing implementations of C+: CCALC 2 and CPLUS2ASP. System CPLUS2ASP translates C+ into ASP programs and use GRINGO and CLASP for computation. For the sake of comparison, we assume that the duration of each action is exactly 1 unit of time so that the plans found by the systems are of the same kind. We assume that initially the spacecraft is rest at coordinate (0, 0, 0). The task is to find a plan such that at each integer time t, the spacecraft is at (t2 , t2 , t2 ). The experiment was performed on an Intel Core 2 Duo CPU 3.00 GHz with 4 GB RAM running on Ubuntu version 11.10. It shows a clear advantage of the SMT-based computation of C+ for this example.

Notation: x ∈ {Tap1 , Tap2 }; W(x), V, Low, High are real numbers;

t, t′ are variables of sort R≥0. TurnOn(x) causes On(x) ∧ Dur =0 TurnOff (x) causes ∼On(x) ∧ Dur=0 On(x) increments Level byW(x)×t if Dur=t Leaking increments Level by -(V×t) if Dur=t constraint (Low≤Level) ∧ (Level≤High) inertial On(x), Leaking exogenous c for every action constant c exogenous Time constraint Time=t + t′ after Time=t ∧ Dur=t′

The language C+ is flexible enough to represent the startprocess-end model [Reiter, 1996; Fox and Long, 2006], where instantaneous actions may initiate or terminate processes. Processes run over time and have a continuous effect on numeric fluents. They are initiated and terminated either by the direct action or by events that are triggered. This model can be encoded in C+ by introducing process fluents, which are Boolean-valued. Such a process fluent is assumed to be inertial, and is caused to be true or false by instantaneous events. Once true, the process fluent p determines the changes of additive fluents c by increment laws

Here, increments laws are defined similar to (8) except that p is a process fluent, instead of a Boolean action constant;

we require that G contain no process fluents and no Boolean action constants. For example,

specifies that, when the process fluent On(Tap1 ) is true, the process contributes to increasing the water level byW(Tap1 ) multiplied by duration.

Figure 5 describes the level of a water tank that has two taps with different flow rates and possible leaking.

6 RelatedWork and Conclusion

Besides the functional stable model semantics we considered in this paper, there are other approaches to incorporate "intensional" functions in ASP [Cabalar, 2011; Lifschitz, 2012; Balduccini, 2012].

Action language H [Chintabathina et al., 2005; Chintabathina and Watson, 2012] is similar to our enhanced C+ in that it can handle reasoning about continuous changes. One notable difference is there, each state represents an interval of time, rather than a particular timepoint. Language H does not have action dynamic laws, and consequently does not allow additive fluents.

The durative action model of PDDL 2.1 [Fox and Long, 2003] is similar to our C+ representation in Section 4. The start-process-stop model of representing continuous changes in PDDL+ [Fox and Long, 2006] is similar to the representation in Section 5. Our work is also related to [Shin and Davis, 2005], which used SMT solvers for computing PDDL+, and a recent work on planning modulo theories [Gregory et al., 2012].

Continuous changes have also been studied in the situation calculus, the event calculus and temporal action logics. In [Lee and Palla, 2012b; 2012a], these action formalisms were reformulated in ASP. We expect that the techniques we developed in this paper can be applied for more effective computation of these formalisms using SMT solvers.

Acknowledgements: We are grateful to Michael Bartholomew 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.