Planning for Temporally Extended Goals as Propositional Satisfiability

1 Introduction

In classical planning, a goal that an agent has to achieve is simply a property of a goal state to reach. TEGs are specifications not only stating desired properties of a final state but of a sequence of states, namely the execution of a plan satisfying the specification. Expressing these goals as formulae of an adequate temporal logic, one can impose more precise constraints on plans than one could with classical reachability goals. So for instance it is possible to specify maintenance goals (some property must be maintained indefinitely), goals stating how the agent should react to some environmental condition, and safety goals that impose a restriction on the agent's behavior not to change certain properties of the world state while trying to achieve a reachability goal.

In planning, temporal specifications are usually either regarded as extended goals or as a means of encoding domainspecific search control knowledge used to guide the planner. Different formalisms have been used, e. g. Temporal Action Logics (TAL) in TALplanner [Doherty and Kvarnstr¨om, Jussi Rintanen Australian National University National ICT Australia and Canberra, Australia Jussi.Rintanen@nicta.com.au

2001], and Metric Interval Temporal Logic (MITL) and Linear Temporal Logic (LTL) in TLPlan [Bacchus and Kabanza, 1996; 2000]. Recently, the Planning Domain Definition Language (PDDL) has been extended to express state trajectory constraints [Gerevini and Long, 2005]. Both TALplanner and TLPlan are forward-chaining planners, pruning the search space by progressing the temporal formula. Other approaches include compiling tasks including LTL goals into classical tasks [Cresswell and Coddington, 2004; Baier and McIlraith, 2006] before solving them by using a classical planner.

Bounded model-checking [Biere et al., 1999; Latvala et al., 2004], which is an extension of the planning as satisfiability approach [Kautz and Selman, 1992], can be viewed as a SAT-based technique for planning with TEGs. Since the efficiency of SAT-based planning techniques is often strongly dependent on the notion of partially ordered or parallel plans [Kautz and Selman, 1996; Rintanen et al., 2006], extending the SAT-based LTL model-checking/planning approach to parallel plans may in some cases be very critical to obtain efficient planning. The contribution of this paper is an encoding of constraints that preserve the semantics of LTL formulae under parallel plans.

In Section 2 we give a formal description of the problem to be solved. In Section 3 we present the propositional encoding, in which we use the base encoding of planning as satisfiability [Kautz and Selman, 1992] reproduced in Section 3.1 and the translation of LTL formulae to propositional logic [Latvala et al., 2004] reproduced in Section 3.2. Section 3.3 shows our adaption of the encoding of parallelism constraints given in [Rintanen et al., 2006] to tasks with TEGs. Our experiments are described in Section 4.

2 Planning for Temporally Extended Goals as Propositional Satisfiability

2.1 ProblemDescription

Notation

Let A be a set of propositional variables and Φ a propositional or temporal formula. We write Lit(A) as a shorthand for A ∪ {¬a | a ∈ A} and Lit(Φ) instead of Lit(var(Φ)), where var(Φ) is the set of variables in Φ. If Lit is a set of literals, we write Lit Φ := Lit ∩ Lit(Φ). If Φ is a propositional formula, then a occurs positively (negatively) in Φ iff there is an occurrence of a in Φ nested within an even (odd) number of negation signs. A negative literal ¬a occurs positively (negatively) in Φ iff a occurs negatively (positively) in Φ. A literal ℓ occurs in Φ if it occurs positively or negatively in Φ. We write pos(ℓ, Φ), neg(ℓ, Φ), and occ(ℓ, Φ), respectively.

Linear Temporal Logic

In order to specify TEGs, we have to choose a specification language. Here we use propositional LTL [Emerson, 1990] without next-time operator because it has a simple and welldefined semantics and it is sufficiently expressive for many qualitative TEGs.

The set of well-formed LTL-X formulae in negation normal form over a set A of propositional variables (LTL-X formulae for short) is inductively defined as follows: for all a ∈ A, a and ¬a are LTL-X formulae. If ϕ, ϕ1, and ϕ2 are LTL-X formulae, so are ϕ1 ∧ ϕ2, ϕ1 ∨ ϕ2, Fϕ ("eventually ϕ"), Gϕ ("always ϕ"), ϕ1Uϕ2 ("ϕ1 until ϕ2") and ϕ1Rϕ2 ("ϕ1 releases ϕ2").

An LTL-X formula ϕ over A is evaluated along an infinite path in a state space over A. Formally, a Kripke model M = 〈Q,→, L〉 is a triple where Q is a set of states, →⊆ Q × Q is a reflexive binary relation over Q, the transition relation, and L : Q → 2A is a function assigning to each state a propositional valuation of the variables in A. A path in M is a function π : N → Q such that for all n ∈ N, π(n) → π(n +1). If π is a path inMand i ∈ N, then the ith suffix of π, πi : N → Q, is defined as πi (j ) := π(i + j ) for all j ∈ N.

For k, b ∈ N, k < b, a path π = u · vω consisting of a finite prefix u = π(0), . . . , π(k-1) and a loop v = π(k), . . . , π(b1), repeated infinitely often, is called a (b, k)-loop. It is called a b-loop if it is a (b, k)-loop for some k < b.

The truth of an LTL-X formula ϕ along a path π, symbolically π |= ϕ, is now inductively defined as follows:

If a given path π is a b-loop, the first b states of π together with the value of k contain all the information needed to evaluate ϕ along π. In the following, all paths we will deal with are of that type.

Let ¯ q = 〈q0, . . . , qb〉 be a finite sequence of states such that qi → qi+1 for all i ∈ {0, . . . , b - 1} and that there is a k ∈ {0, . . . , b - 1} with qb = qk. In order to be able to evaluate an LTL-X formula along ¯ q, we consider an infinite unraveling of ¯ q: If qb ∈ {q0, . . . , qb-1}, say qb = qk, let ¯ q∞ k : N → Q, where ¯ q∞ k (i) = qi, if i < b, and ¯ q∞ k (i) =

q[(i-b) mod (b-k)]+k, otherwise. Note that ¯ q∞ k is actually a path, i. e. consecutive states are related by →. An LTL-X formula ϕ is valid along such a finite sequence ¯ q, written as ¯ q |= ϕ, iff there is a k ∈ {0, . . . , b - 1} such that qb = qk and ¯ q∞ k |= ϕ.

We make sure that there is a k ∈ {0, . . . , b - 1} such that qb = qk by allowing idling in a final state (enforcing it if there is no other loop).

Planning

A planning task is a tuple P = 〈A, I,O, ϕ〉, where A is a finite set of Boolean state variables, I ∈ 2A is the initial state, O is a finite set of operators, and ϕ is an LTL-X formula with variables in A. Operators have the form o = 〈p, e, c〉, where p is a propositional formula over A, the precondition of o, e is a finite set of literals over A, the unconditional effects of o, and c is a finite set of pairs f ▷ d, consisting of a propositional formula f and a finite set of literals d. These pairs are the conditional effects of o.

The set of all effects of o will be written as [o]♦ := e ∪ ⋃{d | f ▷d ∈ c}, the set of unconditional effects as [o]□ := e, and the set of active effects in a state q as [o]q := e ∪ ⋃{d | f ▷d ∈ c and q |= f} for a single operator o and [S ]q := ⋃o∈S [o]q for a set S of operators.

A set S of operators is applicable in a state q if q |= p for all o ∈ S and [S ]q is consistent. We identify an operator o with the singleton set {o}, thus o is applicable in q if its precondition is satisfied and its active effects are consistent. For a set S of operators, possibly singleton for sequential plans or empty to model idling, and a state q such that S is applicable in q, the simultaneous application of S in q results in the state q′ obtained from q by making the literals in [S ]q true and leaving the other state variables unchanged. We then write q S-→q′ (or q o-→q′ if S = {o}). Let ¯ S = 〈S0, . . . , Sb-1〉 be a sequence of sets of operators and q0 a state such that q0 S0 -→q1 S1 -→. . . Sb-1 ---→qb is defined. Then the sequence of states exec(q0, ¯ S ) := 〈q0, . . . , qb〉 is called the execution of ¯ S in q0. Finally, let ¯ S = 〈S0, . . . , Sb-1〉 be a sequence of sets of operators, ¯≺ = 〈≺0, . . . ,≺b-1〉 a sequence of binary relations such that ≺t is a total ordering of St, say ot,0 ≺t · · · ≺t ot,|St|-1, for all t ∈ {0, . . . , b - 1}, and q0 a state. Assume that qt ot,0 --→q1 t ot,1 --→q2 t ot,2 --→. . . ot,|St|-1 -----→qt+1 is defined for all t ∈ {0, . . . , b - 1}. Then the sequence of states exec(q0, ¯ S, ¯≺) := 〈q0, q1 0, q2 0, . . . , q1, q1 1, q2 1, . . . , q2, . . . , qb-1〉 is called a linearized execution of ¯ S in q0.

A plan of length b for P = 〈A, I,O, ϕ〉 is a tuple ¯ S = 〈S0, . . . , Sb-1〉 with St ⊆ O for all t ∈ {0, . . . , b - 1} together with a sequence ¯≺ = 〈≺0, . . . ,≺b-1〉 such that (a) ≺t is a total ordering of St for all t ∈ {0, . . . , b - 1} and (b) ¯ q = exec(I, ¯ S, ¯≺) is defined and ¯ q |= ϕ in the Kripke model induced by P.

2.2 Reduction to Satisfiability

Planning as satisfiability [Kautz and Selman, 1992] roughly works as follows: given a planning task P = 〈A, I,O, ϕ〉, propositional formulae Φ0, Φ1, Φ2, . . . are generated such that there exists a plan of length b for P if Φb is satisfiable.

The Φb are evaluated by using a SAT solver. If Φb is unsatisfiable, the evaluation will proceed to Φb+1, otherwise a plan for P can be extracted from a satisfying valuation v for Φb.

2.3 Solution Quality

The quality of a parallel plan ¯ S = 〈S0, . . . , Sb-1〉 can be measured with respect to its parallel plan length b or its sequential plan length ∑b-1 t=0 |St|. We will focus on finding plans with a low parallel plan length because the size of the largest propositional formula to be considered for a given task is roughly proportional to the parallel length of a plan corresponding to a satisfying valuation. As SAT solver running times grow exponentially in the formula size in the worst case, obtaining small formulae is particularly important.

3 Propositional Encoding

3.1 Base Encoding

We first give the base encoding llbracketPrrbracketbbase of the transition system induced by a planning task P = 〈A, I, O, ϕ〉 for a bound b on the plan length first proposed by [Kautz and Selman, 1992], omitting the reachability goal formula:

where Rt is the conjunction of precondition axioms ot → pt, effect axioms ot → ∧ et+1, conditional effect axioms ∧f▷d∈c ((ot ∧ ft) → ∧ dt+1) for all o = 〈p, e, c〉 ∈ O, and positive and negative frame axioms (¬at ∧ at+1) → ∨o∈O (ot ∧ (EPCa(o))t) and (at ∧ ¬at+1) → ∨o∈O (ot ∧ (EPC¬a(o))t), respectively, for all a ∈ A. In the frame axioms, EPCℓ(〈p, e, c〉) is defined as ⊤, if ℓ ∈ e, and as ∨{f | f ▷d ∈ c and ℓ ∈ d}, otherwise.

This encoding contains propositional variables at for all state variables a ∈ A and time points t ∈ {0, . . . , b} as well as ot for all operators o ∈ O and time points t ∈ {0, . . . , b - 1} with the intended semantics that a holds at time point t iff at is true, and that operator o is applied at time point t iff ot is true. Where sets of variables or propositional formulae are indexed with some t, this actually denotes the sets or formulae with variables indexed correspondingly.

The following theorem states the correctness of the propositional translation. A proof can be found in [Rintanen et al., 2006].

Theorem 1. Let P = 〈A, I,O, ϕ〉 be a planning task. Then there exists a sequence of sets of operators ¯ S = 〈S0, . . . , Sb-1〉 such that exec(I, ¯ S ) is defined iff the formula llbracketPrrbracketbbase is satisfiable.

3.2 Temporally Extended Goals

In this subsection we reproduce the reduction of the bounded LTL/LTL-X model-checking problem to propositional satisfiability given in [Latvala et al., 2004], adding the constraint that a satisfying sequence of states must contain a loop: let P = 〈A, I, O, ϕ〉 be a planning task and b ∈ N. Then

with fresh auxiliary variables lt, bef t , t ∈ {0, . . . , b - 1} (with the intended semantics that there is a loop from qb-1 back to qt or back to some qt′ , t′ < t, respectively). The recursive translation llbracketϕrrbracket0b of ϕ is defined as

Notice that the translation llbracket·rrbrackettb is closely related to the formula progression procedures used in [Bacchus and Kabanza, 2000; Doherty and Kvarnstr ¨om, 2001].

The following theorem states the correctness and completeness of the propositional translation. A slightly different formulation as well as a proof can be found in [Latvala et al., 2004].

Theorem 2. Let P = 〈A, I,O, ϕ〉 be a planning task and b ∈ N. Then there exists a sequence of sets of operators ¯ S = 〈S0, . . . , Sb-1〉 such that ¯ q = exec(I, ¯ S ) is defined and ¯ q |= ϕ iff the formula llbracketPrrbracketbbase ∧ llbracketPrrbracketbbmc is satisfiable.

3.3 Parallel Plans

In this section we present our main contribution, being constraints which guarantee that the meaning of LTL-X formulae is preserved under parallel plans, and a propositional encoding of these constraints.

Theorem 2 tells us how to encode the requirement that there is a sequence ¯ S such that exec(I, ¯ S ) |= ϕ. But we have not yet made sure that ¯ S is in fact a plan, i. e. there is a sequence ¯≺ of corresponding total orderings such that exec(I, ¯ S, ¯≺) |= ϕ. For such a sequence ¯≺ to yield an admissible linearization, it must ensure that (a) ¯ q = exec(I, ¯ S, ¯≺) is defined and if so, that (b) ¯ q |= ϕ. In order to state how this can be achieved, we need some definitions. The first one and the subsequent lemma are due to [Lamport, 1983].

Definition 1. Let π = q0, q1, q2, . . . and ˜π = ˜ q0, ˜ q1, ˜ q2, . . . be two infinite (finite) paths in a Kripke model 〈Q,→, L〉. Then π and ˜π are called stuttering equivalent, π ∼ ˜π for short, if there are two infinite (finite) sequences of natural numbers 0 = i0 < i1 < i2 < . . . (< in) and 0 = j0 < j1 < j2 < . . . (< jn) such that for all 0 ≤ k (< n) : L(qik ) = L(qik+1) = . . . = L(qik+1-1) = L(˜ qjk ) = L(˜ qjk+1) = . . . = L(˜ qjk+1-1). A finite subsequence like qik , qik+1, . . . , qik+1-1 of π or ˜π consisting of identically labeled states is called a block.

Lemma 3. Let ϕ be an LTL-X formula, M = 〈Q,→, L〉 a Kripke model, where L : Q → 2A for some A ⊇ var (ϕ), and π, ˜π two infinite (finite) paths in Mwith π ∼ ˜π. Then π |= ϕ iff ˜π |= ϕ.

The following definition, adapted from a similar one by [Rintanen et al., 2006], is crucial for the rest of this section in that it describes under which circumstances an operator o may or may not be applied before an operator o′ in a linearization ≺ of a set of operators S if one wants to ensure that for all time points t the application of St in qt in the ordering given by ≺t is defined in the first place, and if so, that exec(I, ¯ S, ¯≺) |= ϕ.

Definition 2. Let P = 〈A, I,O, ϕ〉 be a planning task and o = 〈p, e, c〉, o′ = 〈p′ , e′ , c′ 〉 ∈ O. Then o affects o′ iff o ̸= o′ and either (1.) there is a literal ℓ over A such that (a.) ℓ ∈ [o]♦ and (b.) (i.) neg(ℓ, p′ ) or (ii.) occ(ℓ, f ′ ) for some f ′ ▷d′ ∈ c′ , or (2.) [o′ ]ϕ♦ \ [o]ϕ□ ̸= ∅.

Here, [o′ ]ϕ♦ is the restriction of [o′ ]♦, i. e. of the set of all conditional and unconditional effect literals of o′ , to those literals occurring (positively or negatively) in ϕ. Similarly, for o = 〈p, e, c〉, [o]ϕ□ = e ∩ Lit (ϕ).

The cases correspond to different problems that can potentially arise if o is applied before o′ in a linearization, namely to o falsifying the precondition of o′ [(1.a.) + (1.b.i.)], o affecting the set of active effects of o′ [(1.a.) + (1.b.ii.)], and o and o′ putting at risk the stuttering equivalence of exec(I, ¯ S ) and exec(I, ¯ S, ¯≺) [(2.)]. The definition gives rise to a condition on the admissibility of a sequence ¯≺ of total orderings.

Lemma 4. Let P = 〈A, I,O, ϕ〉 be a planning task, ¯ S = 〈S0, . . . , Sb-1〉 a sequence of sets of operators such that exec(I, ¯ S) |= ϕ, and ¯≺ = 〈≺0, . . . ,≺b-1〉 a sequence such that ≺t is a total ordering of St for all t ∈ {0, . . . , b - 1}. If there are no operators o, o′ ∈ St such that o affects o′ and o ≺t o′ for any t ∈ {0, . . . , b - 1}, then ¯ S together with ¯≺ is a plan for P.

Proof sketch. We have to show that exec(I, ¯ S, ¯≺) is defined and exec(I, ¯ S, ¯≺) |= ϕ. As argued in [Rintanen et al., 2006], in order to show that exec(I, ¯ S, ¯≺) is defined, it suffices to show that no operator o ∈ St can disable another operator o′ ∈ St by potentially falsifying its precondition or altering its set of active effects for any t ∈ {0, . . . , b - 1}. These two possibilities are ruled out by condition (1.a.) together with (1.b.i.) and (1.b.ii.) of Definition 2 respectively (see [Rintanen et al., 2006] for a detailed proof of that claim). If exec(I, ¯ S, ¯≺) is defined, by using Lemma 3 it is sufficient to show that exec(I, ¯ S ) ∼ exec(I, ¯ S, ¯≺) in the Kripke model M = 〈Q,→, L〉, where Q and → form the state space induced by P and L : Q → 2var(ϕ) is defined by L(q) = q ∩ var(ϕ). To see that this is true, consider a single time point t ∈ {0, . . . , b - 1} first. Let ≺t be the total ordering of St and, say, ot,0 ≺t · · · ≺t ot,|St|-1. Then the subsequence of the linearized execution exec(I, ¯ S, ¯≺)

corresponds to the subsequence of the execution exec(I, ¯ S)

Note that condition (2.) of Definition 2 together with the fact that no operator affects an operator applied later in ≺t makes sure that for o ≺t o′ , [o′ ]ϕ♦ ⊆ [o]ϕ□ holds and thus all effects in [St]qt relevant to ϕ, i. e. those effects concerning a variable occurring in ϕ, are effects of ot,0. Therefore, the operators ot,1, . . . , ot,|St|-1 do not have an additional effect on the labeling L. Thus, L(q1 t ) = L(q2 t ) = . . . = L(qt+1), and q1 t , q2 t , . . . , qt+1 form one block of the stuttering equivalence of exec(I, ¯ S, ¯≺) and exec(I, ¯ S ). The corresponding block in exec(I, ¯ S ) is the singleton {qt+1}. The other blocks are constructed analogously.

The next step is to find a propositional formula encoding the condition that at no time point t any two operators o, o′ such that o affects o′ and o ≺t o′ can be applied simultaneously. For that purpose we define the notion of a disabling graph [Rintanen et al., 2006] for a planning task P.

Definition 3. Let P = 〈A, I,O, ϕ〉 be a planning task. A directed graph G = 〈O, E〉, where E ⊆ O×O, is a disabling graph for P if E contains all edges (o, o′ ) such that (1.) there is a state q reachable from I with operators in O in which o and o′ are simultaneously applicable and (2.) o affects o′ .

Let St be a set of operators. If the subgraph Gt = 〈St, Et〉, Et = E ∩ (St × St), of a disabling graph G = 〈O,E〉 for P induced by St is acyclic, then there is an ordering ≺t of St in which there are no two operators o ≺t o′ with o affecting o′ . In fact, ≺t can be an arbitrary topological ordering of 〈St,E-1 t 〉. As the strongly connected components (SCCs) of a directed graph form a directed acyclic graph, instead of ensuring the acyclicity of Gt, it is sufficient to ensure the acyclicity of the subgraphs of Gt induced by the SCCs Ci of G, i. e. of Gi t = 〈S i t , Ei t 〉, where S i t = St ∩ Ci and Ei t = Et ∩ (S i t ×S i t). This can be achieved as follows:

Let G = 〈O, E〉 be a disabling graph, C = {C1, . . . , Cm} the set of SCCs of G, and ≺i an arbitrary total ordering of Ci = {oi1 , . . . , oi|Ci| } for all i ∈ {1, . . . ,m}, say oi1 ≺i · · · ≺i oi|Ci| . For o1 , . . . , on ∈ O, E,R ⊆ O and ℓ ∈ Lit(A), we define formulae stating that there are no oi, oj ∈ {o1 , . . . , on }, i < j, such that oi ∈ E, oj ∈ R, and oi, oj are applied simultaneously (intuitively, operators in E can disable operators in R wrt ℓ):

where the ai,ℓ are fresh auxiliary variables. Now, the negation of (1) in Definition 2 translates to the conjunction of chain formulae for all time points, SCCs, and literals in ϕ, if we use the following sets Eℓ, Rℓ:

Similarly, the negation of (2) in Definition 2 translates to the conjunction of chain formulae with the sets E∼ ℓ ,R∼ ℓ :

So, the parallelism constraints can be encoded in the formula

Remark 1. If the valuation corresponding to a sequence of sets of operators ¯ S = 〈S0, . . . , Sb-1〉 satisfies llbracketPrrbracketblin , then for all time points t and SCCs Ci of the disabling graph G = 〈O, E〉 used in the construction of llbracketPrrbracketblin , all subgraphs Gi t = 〈S i t , Ei t 〉 are acyclic. 1 As the SCCs form an acyclic graph, there is a total ordering ≺C on C such that for all i, j ∈ {1, . . . ,m} with Ci ≺C Cj, there are no o ∈ Ci and o′ ∈ Cj such that (o, o′ ) ∈ E. Since Gi t is acyclic, there is a total ordering ≺it of S i t for each t ∈ {0, . . . , b - 1} and i ∈ {1, . . . ,m} (consistent with the ordering ≺i used in the construction of llbracketPrrbracketblin ) such that there is no pair o, o′ ∈ Ci with (o, o′ ) ∈ E and o ≺it o′ . The relations ≺it, i ∈ {1, . . . ,m}, and ≺C can be combined lexicographically, resulting in an ordering ≺t of St. It follows that there is no t ∈ {0, . . . , b - 1} and no o, o′ ∈ St such that o affects o′ and o ≺t o′ .

The following theorem combines the conclusions from Theorem 2 and Lemma 4 with the above Remark.

Main Theorem. Let P = 〈A, I,O, ϕ〉 be a planning task and b ∈ N. If llbracketPrrbracketbbase ∧ llbracketPrrbracketbbmc ∧ llbracketPrrbracketblin is satisfiable, then there is a plan of length b for P.

Proof sketch. From Theorem 2 we know that there exists a sequence of sets of operators ¯ S = 〈S0, . . . , Sb-1〉 such that ¯ q = exec(I, ¯ S ) is defined and ¯ q |= ϕ. In order to be able to use Lemma 4, we still need a sequence ¯≺ = 〈≺0, . . . , ≺b-1〉 of corresponding total orderings such that there is no time point t ∈ {0, . . . , b - 1} and no pair o, o′ ∈ St of operators with o affecting o′ and o ≺t o′ . The orderings ≺t constructed in Remark 1 form such a sequence. Thus, the precondition of Lemma 4 is satisfied and it follows that ¯ S together with ¯≺ is a plan for P, and in particular that exec(I, ¯ S, ¯≺) is defined and exec(I, ¯ S, ¯≺) |= ϕ.

1 We will not formally prove this here. A similar proof can be found in [Rintanen et al., 2006].

4 Experiments

4.1 Setting

We compared the cumulative SAT solver running times until the first satisfiable formula for (a.) the parallel encoding described in Section 3 and (b.) a sequential encoding derived from the parallel one by replacing the parallelism constraints by axioms demanding at most one operator per time point. The evaluation of the formulae corresponding to increasing plan lengths was performed sequentially. Additionally, we compared the (parallel) plan lengths of the resulting plans.

We used two types of planning tasks. First, we considered a simple hand-crafted logistics-like transportation task with three portables and trucks each. The goal was to find an infinite plan assuring that the portables are shipped back and forth between two locations indefinitely. The goal formula we used was ϕ = ∧2j=1 GF(∧3i=1 at(pi, dij)), where the pi are portables and the dij are locations.

The other tasks were adapted from the 2006 International Planning Competition. We modified the qualitative preferences tasks from the rovers domain by turning the soft temporal constraints (preferences) into hard constraints and by ignoring the metric function. When changing soft into hard constraints, it turned out that it was necessary to drop some of them in order to keep the tasks solvable. This was done by drawing uniformly at random κ constraints for each task and only retaining the ones drawn. 2 The constraints were translated to LTL-X as explained in [Gerevini and Long, 2005]. Unlike the first task above, the rovers tasks lacked explicit nesting of temporal operators 3 and could, if solvable at all, be solved by plans always yielding finite executions, apart from infinite idling in a final state. The reachability goals specified in the problem definitions were required to hold in such a final state.

The SAT solver we used was SIEGE V. 4 [Ryan, 2004]. The experiments were run on a PC with 1.8 GHz AMD ATHLON 64 CPU, 768 MB RAM, and a LINUX operating system.

4.2 Results

Table 1 contains results from the logistics task and the modified rovers tasks for κ = 3.

The second and third columns show the size M of the largest SCC of the computed disabling graph compared to its overall number of nodes |O|. The fourth column shows the parallel plan lengths bp obtained with our parallel encoding, compared to sequential plan lengths bs in column five. Where an interval (m, n] is given, the shortest sequential plan has length m < bs ≤ n, but we could not precisely determine bs because of SAT solver running times exceeding our time-out of 10 min. The values rp and rs are the cumulative SAT solver running times up to the first satisfiable formula in seconds in the parallel and sequential case, respectively. To obtain these values, we used a time-out of 120sec for each single satisfiability test, proceeding to the next formula after time-out. Rp denotes the overall running time needed for parallel planning (PDDL parsing, encoding, SAT solving, decoding) in seconds. The discrepancy between SAT solver and overall running times arises because we used an unoptimized SML program to do the encoding. In particular, for the construction of the disabling graph and the computation of invariants, a speed-up by an order of magnitude appears to be possible.

2 For κ = 3, the tasks r-03, r-05 and r-15 remained unsolvable.

3 There is an implicit nesting of depth two to three in the temporal operators sometime-after, sometime-before and at-most-once.

5 Conclusion

We combined existing techniques for planning as satisfiability, bounded LTL model-checking, and parallel planning in order to obtain an efficient method of planning for TEGs. The use of a disabling-graph-based encoding of constraints ensuring the stuttering equivalence of a parallel and at least one corresponding sequential plan execution allowed us to extend parallel planning to planning for TEGs. Our experimental results show that, like in classical SAT-based planning [Kautz and Selman, 1996] and in Graphplan [Blum and Furst, 1995], admitting parallelism can noticeably speed up planning for TEGs. By using the non-sequential formula evaluation strategies given in [Rintanen et al., 2006, Sections 5.2, 5.3], which are orthogonal to the contributions of the present paper, planner running times might be further reducible.

Acknowledgments

This work was partly supported by the DFG within SFB/TR 14 AVACS, by the EC under contract no. FP6-004250-CoSy, and by the BMBF through the DESIRE project. Jussi Rintanen's research was supported by National ICT Australia

(NICTA) in connection with the DPOLP project. NICTA is funded through the Australian Government's Backing Australia's Ability initiative, in part through the Australian National Research Council.