Reachability, Relevance, Resolution and the Planning as Satisfiability Approach

1 Introduction

The success of the planning as satisfiability (PAS) approach [Kautz and Selman, 1992; 1996] has led to various attempts to refine the initial methods used and to improve our under­ standing of its performance. In particular, various methods for generating formulas from planning instances have been com­ pared [Ernst et al., 1997], and various systematic alternatives to the original stochastic method have been examined (e.g., [Li and Anbulagan, 1997; Bayardo and Schrag, 1997]). Still, many issues surrounding this approach are poorly understood. In particular, little is known about the influence of the encod­ ing method on performance.

Concentrating on the two encoding methods proposed by [Kautz and Selman, 1996], the linear and the GRAPHPLAN­ based encodings, we examine their influence on the ability to propagate reachability and relevance information via unit propagation and, more generally, k-clause resolution. We do so by comparing the pruning ability of these techniques to that of variants of existing algorithms that operate on the original problem formulation [Boutilier et al., 1998].

Our work is motivated by unit resolution's central role in the Davis-Putnam algorithm [Davis et al., 1962] and many of its offsprings (e.g., [Freeman, 1995; Crawford and Auton, 1993; Li and Anbulagan, 1997; Gomes et al., 1998]), and its use as a preprocessing step when stochastic methods are ap­ plied. Moreover, a limited form of binary propagation is used in Crawford's COMPACT program for simplifying CNF for­ mulas and is utilized in the BLACKBOX planner [Kautz and Selman, 1998]. Reachability and relevance analysis play a major role in recent planning algorithms, most notably in the GRAPHPLAN planner [Blum and Furst, 1995].

Finally, motivated by some of our observations and by the fact that binary clauses form a significant fraction of the clauses within sat-encoded planning problems, we show that a simple and cheap preprocessing step based on limited binary resolution can yield nice savings in running time.

The paper is organized as follows: in Section 2, we discuss the Reachable-k algorithm and its counterpart, Relevant-k. We compare each algorithm's ability to prune possible actions to that of k-clause resolution. ·A number of theoretical re­ sults are presented as well as an empirical comparison of the various methods fork = 1. In Section 3, we motivate and explain the use of binary-binary resolution as a preprocess­ ing step and show its effect on two recent efficient systematic algorithms. The overhead of this preprocessing step is rela­ tively small, and in some cases it yields nice savings. We con­ clude with a discussion offuture and related work in Section 4. Throughout the paper we assume basic familiarity with the es­ sential ideas behind the PAS framework and the GRAPHPLAN algorithm. Proofs appear in a longer version of this paper, al­ though their central points are discussed here.

2 Reachability, Relevance, Resolution

Reachability and relevance analysis form an essential part of successful modem planning algorithms. The most notable example of reachability analysis is GRAPHPLAN's planning graph [Blum and Furst, 1995], and many recent planners em­ ploy either reachability analysis (e.g., [Bonet et al., 1997]), relevance analysis (e.g., [McDermoot, 1996; Nebel et al., 1997]), or both [Kambhampati et al., 1997]. The importance of reachability and relevance analysis has been noted in the context of decision-theoretic planning as well. For example, [Boutilier and Dearden, 1994] employ relevance analysis to reduce the state-space, and [Boutilier et al., 1998] describe a general method for reachability analysis for MDPs. Below, we discuss this method in a simplified form suitable for clas­ sical planning problems described using the STRIPS repre­ sentation language [Fikes and Nilsson, 1971]. We shall also present a counterpart of this method for performing relevance analysis and relate these algorithms to k-clause resolution in the context of sat-encoded planning problems.

• So = propositions that are true initially.
• CSo = {}.
• Ao = actions all of whose preconditions are in So.
• CA~ = {{a;,aj}la;,aj E Ao, i # j, neithera; noraj are noops or a j is a noop whose effect is destroyed by a;}.
• CA6 = {{a;,aj}la;,aj E Ao, i # j, and a; deletes a precondition or an effect of aj }.

We defineS; , A; inductively as follows:

• S; = literals that appear in the effects of A; -I ·
• A ; = actions whose precond.itions appear in S; and no subset of them appears in c s;.
• C St = k-tuples of literal appearing in S; such that some sub­ set of any set of actions from A; _ 1 that has these literals as their effects appears in CAL1 (where* E {£, P} as appropriate).
• CA{; = {{al , aj}ial , aj E Ao , l # j , neithera1 noraj are noops, or a j is a noop whose effect is destroyed by a1}.
• CAf = {{aj1 , ··· ,aj,}ll ~ k , aJ1>····aj1 E A;, Jm # Jn form # n, and either (1) ajm deletes a precondition or an effect of a]n for some m # n or (2) some subset of the preconditions of ail, ... , aj1 appears in CSt }.

Figure 1: Reachable-k

2.1 Propagating Reachability Information

Reachable-k [Boutilier et al., 1998] is an algorithm for esti­ mating the states reachable from a given initial state. As for­ mulated, it is quite general and applies to domains with non­ deterministic actions and conditional effects. In Figure 1, we present a simplified version ofReachable-k that deals with de­ terministic, unconditional actions represented in the STRIPS representation language. An important reason for our inter­ est in it is its similarity to the influential planning graph con­ struction of the GRAPHPLAN planner [Blum and Furst, 1995]. In fact, it generalizes the ideas behind GRAPHPLAN's plan­ ning graph, which is equivalent to Reachable-2. We use A; to denote the set of actions feasible i steps from the initial state, S; to denote the corresponding set of propositions, and c s; to denote constraints o·n these propositions, such that if {Pl , ... , Pm} E C Si then these propositions cannot co­ occur after i steps. C Ai denotes similar constraints on ac­ tions. Here, * E {L, P}, where Lis used when we restrict our attention to linear action sequences, and P is used when we allow concurrent non-conflicting actions (i.e., actions that do not destroy each others' effects or preconditions and whose preconditions are not constrained not to co-occur). Of course, for k = 1 the sets C s; and C Ai are empty for all i ~ 0. Fi­ nally, note that in this description, the set of possible actions contains ail actions of the form noop(l), where l is a literal.

When k = 2, S; and A; represent the propositional and action levels of GRAPHPLAN's planning graph, and C S; and CAf hold their respective mutual exclusion constraints. We have not stated a termination condition for this algorithm, but one can be formulated based on the content of S; or the in­ dex i itself. In the PAS framework, where the number of time-steps is fixed, one would opt for the second alternative. Reachable-k gives us sets of actions and propositions, Aj , Sj, that can occur after the performance of j actions (or j sets of concurrently non-conflicting actions) from the initial state. It is sound in the following sense: if a set of propositions or a set of actions is excluded by it at time j, we know that these cannot occur (resp. be executed) after j steps.

Sometimes, all actions that can be executed at a particu­ lar time point in which p holds have -,p as an effect. In that case, we can ignore the noop(p) action, as it will not be part of any useful plan. However, as formulated, p will appear in Reachable-k 's next level. We denote by Reachable* -k a vari­ ant in which noop(p) does not appear in such a case.

2.2 k-Clause Resolution and Reachability

k-clause resolution (or propagation) refers to the resolution of pairs of clauses one of whose length is k at most. The k = 1 variant, i.e., unit propagation, is an integral part of all major algorithms for generating satisfying assignments.

We wish to compare the type of reachability information derived by performing k-clause resolution on sat-encoded planning problems, with the information obtained by running the Reachable-k algorithm. By reachability information we mean constraints on the set of actions possible at a time point or constraints on world states (in the form of, e.g., sets of un­ reachable propositions or k-tuples of propositions). Our fo­ cus will be on the first type of constraints. We say that one al­ gorithm generates more reachability information than another if it always generates a superset of the constraints on actions generated by the other algorithm, and there are instances in which this is a strict superset. We compare the two Reachable variants with two encoding methods discussed in [Kautz and Selman, 1996]: 1 the linear encoding and the more interesting GRAPHPLAN encoding.

Linear Plan Encoding

The linear plan encoding [Kautz and Selman, 1992] is a sim­ ple and natural method for translating a planning problem into a formula that is satisfiable iff there is a valid plan of length n (for some given n). The clauses in the linear plan encoding fall into the following classes:

1. an action implies its preconditions prior to its execution;
2. an action implies its effects following its execution;
3. an action does not affect any other proposition (frame ax­ ioms);
4. there is at least one action at each time point;
5. there is at most one action at each time point.

Here, noop actions are not considered. In addition, the for­ mula contains unary clauses describing the initial and goal states. In analyzing reachability effects, we ignore informa­ tion about the goal state (discussed later in the section on rel­ evance).

Consider the mechanism by which resolution can yield reachability information: Given the propositions that hold at the initial state, we can derive the negation of actions whose preconditions do not hold using unit propagation on axioms of class 1. Propagating these unit clauses with the appropriate instance of axiom class 4, we will obtain a disjunction of all actions that can be executed at the first time point. So far, this is identical to what Reachable* -k provides. To propagate this information forward, we can resolve these action disjunctions with axioms of class 2 and 3. This, however, requires binary resolution. Hence, except for the unlikely case in which a sin­ gle action is possible, there is no more that we can derive using unit propagation alone. Reachable* -1, on the other hand, can provide us with a list of all possible effects of these actions and possibly prune out future actions whose preconditions do not appear in this list. We conclude:

1 The third (state-based) encoding method cannot be generated automatically.

Lemma 1 In the context of the linear encoding, Reachable*- 1 yields more reachability information than unit propagation.

Example: Consider a blocks' world domain with a single ac­ tion schema MOVE(object,source,destination). Its precondi­ tions are: ON(object,source), CLEAR(object), clear(destination) and its effects are: ON(object,destination), CLEAR(source), ·ON(object,source), ·CLEAR(destination) (except when the destination is the table which is always clear). If we have k stacks of blocks initially, k 2 actions can be performed at the initial state (i .e., moving a block from the top of a stack to the top of another stack or the ta­ ble). This will be discovered by both algorithms. In partic­ ular, unit propagation will yield a disjunction of all these ac­ tions. We know that all blocks that are 2 or more blocks be­ low the top cannot participate in the second MOVE action. Reachable-! will find this out due to the fact that they are not CLEAR. Suppose that A is one such block. All initially fea­ sible actions participate in a frame axiom of the form Move­ x 1\ ·clear(A , 0) -t ·clear(A, 1) , which, in clausal form is ·M ove-x V clear ( A , 0) V ·clear( A , 1). Resolving against ·clear( A , 0), we have ·M ove-xV·clear(A, 1). If we could deduce ·clear( A , 1 ), we could rule out all actions that have it as a precondition. But if we are restricted to unit propagation, this requires deducing M ove-x for some initially feasible ac­ tion, and we cannot make such a deduction. Precise numbers for a number of instances appear in Table 1.

If we propagated information forward using axioms of class 2 and 3 and binary resolution (i .e., as discussed before Lemma 1), we now have a set of disjunctions of the possible effects (including frame effects) of the initially allowable ac­ tions. The number of such disjuncts is 0( em), where e is the maximal number of effects of an action and m is the number of actions that can be executed initially. In some cases, these dis­ junctions could contain a single literal, e.g., when all initially allowable actions leave some proposition unchanged. When one of these disjunctions contains only literals that are nega­ tions of some action's precondition, we can deduce the nega­ tion of this action by resolving with axioms of class 1.

In the example considered above we would generate a dis­ junction of the form M ove-x 1 V M ove-x2 V · · · V M ove-xr, containing all time 0 actions whose negations have not been deduced. As discussed above, for all such actions, we can ob­ tain a clause of the form ·M ove-x; V ·clear( A , 1) . Resolv­ ing these binary clauses against the clause above, we obtain a unary clause ·clear(A , 1), that can be used in conjunction with class 1 axioms to deduce the negations of actions whose preconditions include clear(A, 1).

Using the effect disjunctions we deduce mutual exclusion constraints on actions, but these are already built into the en­ coding. In principle, one can resolve these effect disjunctions with each other, but any useful new resolvants already appear among them (simply based on the fact that an action cannot have a proposition and its negation as effects). Consequently, we have:

Lemma 2 In the linear encoding, binary resolution is suffi­ cient to conclude all possible reachability constraints.

Reachable* -k propagates information forward in a similar manner but does not consider interactions between more than k actions or propositions. Since such interactions can occur, we have:

Consequence 1 Reachable* -k yields less information than binary resolution.

The GRAPHPLAN Encoding

The GRAPHPLAN encoding differs from the linear encoding by its ability to consider multiple concurrent (non-interfering) actions, allowing one to obtain shorter plans which, in tum, can reduce the search space size. It constructs the following sets of clauses:

1. An action implies its preconditions;
2. An effect implies one of the actions that has this effect;
3. There is at least one action at each time-point;
4. Two conflicting actions cannot occur together.

Besides the obvious ability to consider multiple parallel (non­ interfering) actions, the important difference between the GRAPHPLAN and Linear encoding is in axiom class 2 (re­ ferred to in [Ernst et al., 1997] as explanatory frame axioms.) Clauses in this class will contain positive occurrences of ac­ tion literals and negative occurrences of state literals.

As in the linear case, using unit propagation we can in­ fer which actions cannot be applied at the initial state. Us­ ing axioms of class 2, we can propagate this information for­ ward, deducing the negation of all effects that cannot be pro­ duced by the initially allowable actions. This information en­ ables us to exclude actions whose preconditions cannot be produced. This forward propagation is essentially identical to Reachable- I. If we ignore the explicit constraints appearing in axiom class 4, we can conclude:

Lemma 3 In the context of the GRAPHPLAN encoding, unit propagation and Reachable-/ yield the same reachability in­ formation.

Notice that axioms from class 4 do not participate in unit prop­ agation because they contain pairs of negated actions. Resolv­ ing against them requires a positive action literal which can­ not be deduced using the given axioms (except for the unlikely case in which a single action is possible initially). In general, we can deduce only negated action literals, which can be re­ solved against axioms of class 2 to yield, at best, deduced ef­ fects , or against axioms of class 3 to yield a disjunction of pos­ sible actions. This is precisely what Reachable-! yields.

When k > 1, the mechanism remains the same, but now axioms of class 4 can play a part if we apply binary propaga­ tion. First, we will have binary constraints on co-occurring actions. These will propagate forward, possibly resulting in constraints on state propositions. These constraints need not necessarily be binary. Their propagation will require, in the general case, more than binary resolution. More generally, we observe that:

Lemma 4 In the context of the GRAPHPLAN encoding, for k > 1, k-clause resolution yields more information than Reachable-k.

As a special case, when k = 2 it has been observed [Kautz and Selman; 1998] that GRAPHPLAN's propagation of mu­ texes (which is equivalent to Reachable-2) is equivalent to a restricted form of binary resolution.

In general, one difference between these methods lies in the ability of k-clause resolution to yield disjunctions of more thank state propositions or actions, although these constraints cannot be propagated forward unless k is larger than the max­ imal size of clauses of class 2. As an example of how bi­ nary resolution can yield more reachability information than GRAPHPLAN's planning graph consider a situation where p can be produced only by actions a 1 , a 2 ; q can be produced only by a1, aa; and r can be produced only by a2, aa; but each pair of a1, a2 , a a is mutually exclusive. If a1, a2, a3 are the only possible actions, then we can derive the ternary constraint ·p V ·q V ·r. ·

2.3 k-Clause Resolution and Relevance

We formulate an algorithm similar to Reachable-k, which we call Relevant-k, with a sim­ ilar soundness property. Relevant-k prunes the search space by generating a set of propositions that could appear in states that precede the goal state by k steps in any execution of a valid plan. Actions whose preconditions are not among these propositions can be ruled out. This leads to a reduced search space. Relevant-k is described in Figure 2. 2 Fork = 1 we ig­ nore the sets C A; and C S;. Various existing algorithms use ideas similar to Relevant-! (e.g., [McDermoot, 1996; Nebel et al., 1997]).

For Relevant-k to work in practice we must make the fol­ lowing closure assumption: if a proposition appears in the ef­ fect of an action (possibly negated), it must also appear in its

2 We consider the parallel execution case only.

• So = propositions that are part of the goal.
• CSo = {}.
• Ao = actions, some of whose effects are in So.
• GAo = {{a;, a i }la; , a j E Ao, i :f. j, and a; deletes a precondition or an effect of a j }.

We defineS; , A; inductively as follows:

• S; = propositions that appear in the preconditions of A ;- 1 ·
• A; =actions whose effects appear inS; and no subset of them appears in C S;.
• C S; = k-tuples of propositions appearing inS; such that some subset of any set of actions from A;_1 that has these proposi­ tions as their preconditions appears in CA;- 1 ·
• CA; = {{aj1 , ..· , aJ 1 }II :S k , a j 11 ·.· , aj 1 E A ;, im :f. in form :f. nand either (I) aim deletes a precondition or an effect of a in for some m :f. n or (2) some subset of the effects of ah , ... , aJ 1 appears in CSi} .

Figure 2: Relevant-k

precondition (possibly negated). When propositions stand for path properties (e.g., see the TSP domain in the GRAPHPLAN distribution), one cannot enforce this condition. 3

We now compare the amount of relevance information that can be propagated backwards using k-clause resolution and the goal literals as opposed to Relevant-k. Consider unit prop­ agation first. In the context of the linear encoding, we see that all actions that destroy some goal condition will be ruled out. However, actions that are irrelevant because they produce ir­ relevant effects will not be pruned. This is incomparable to Relevant-!. There, irrelevant actions will be pruned out, but a relevant action that destroys some goal proposition will not be ruled out without modification to the algorithm.

In the context of the GRAPH PLAN encoding the relationship is clearer. From the goal propositions and axioms of class 2 we can deduce disjunctions of actions that must have produced these effects. Typically, these disjunctions will not contain unit clauses, and unit propagation cannot proceed farther. No­ tice that we cannot deduce the kind of information obtained via the linear encoding. That is, if an action destroys some goal proposition, we cannot conclude its negation using unit propagation. For example, if a has ·p as an effect and p is part of the goal, we have ·p -+ a V · · · as an instance of ax­ iom class 2. Since a appears positive in this axiom, we can­ not deduce its negation by resolving against it. Rather, deduc­ ing negated actions requires explicit effect axioms of the form p -+ ·a. Finally, while such information is not deduced nec­ essarily by Relevant-!, the simple relevance information de­ duced by Relevant-! cannot be deduced here either. That is, we have no way of deducing ·a if all of a's effects are irrel­ evant to the goal. We conclude (again, ignoring the explicit mutual exclusion information contained in axiom class 4):

Lemma 5 In the context of the GRAPHPLAN encoding, unit propagation yields less relevance information than Relevant-/.

3 With small modification, this assumption can be removed.

Some actual values appears in Table 1. In particular, in the examples we looked at, the GRAPHPLAN encoding could not prune any action. This follows from the (quite typical) fact that in these domains, each of the facts that hold at the final state can be achieved by a number of actions. Hence, unit propagation can deduce only disjunctions of possible actions, none of which are a unit clause. Since we have no way of de­ ducing negated actions, propagation stops at this point.

The general case is similar. In the linear encoding, having obtained a disjunction of allowable actions, we can generate a disjunction of allowable preconditions. This information is propagated backwards much like the forward case. Yet, as in the k = 1 case, all we can expect is a form of backwards reachability analysis from the goal state, rather than true rel­ evance analysis. In the context of the GRAPHPLAN encod­ ing, we will generate disjunctions of relevant actions, from which disjunctions of relevant preconditions can be deduced, etc. However, irrelevant actions will not be excluded explic­ itly (since more than one action is allowed at each step) and we will only conclude that some relevant action must appear. Nor can we exclude actions that destroy a goal proposition. On the other hand, using k-clause resolution we can deduce con­ straints of order greater than k, unlike Relevant-k. Therefore, no clear winner emerges. We hypothesize that Relevant-k would perform better, but this remains to be tested.

Finally, we note that (1) the GRAPHPLAN planner does not incorporate relevance analysis, but Mea-GRAPHPLAN, a more recent variant, does [Kambhampati et at., 1997]. (2) [Ernst et at., 1997] discuss an enhanced version of the GRAPHPLAN encoding which contains effects axioms as well (i.e., axioms of the form action -t effect). In terms of the ability to propagate reachability and relevance analysis we see here only an added ability to rule out actions that destroy needed propositions (as in the linear encoding.)

3 Binary Resolution Preprocessing

Specialized subroutines that exploit binary clauses in SAT problems have been considered in the past [Larrabee, 1992]. We believe that judicious use of binary resolution is a promis­ ing direction in the context of the PAS framework for a num­ ber of reasons: (1) GRAPHPLAN's mutexes are equivalent to binary clauses, and their propagation is equivalent to a limited form of binary resolution [Kautz and Selman, 1998]. ·(2) Bi­ nary resolution yields all the reachability information in the linear encoding (Lemma 2). (3) Binary clauses form a large fraction of the clauses within encoded formulas: In the linear encoding, all axioms of class 1 ,2,5 yield binary clauses, and in the GRAPH PLAN encoding, this is true of axioms of class 1,4. (4) 2-SAT problems can be solved in polynomial time.

Unlike unit propagation, binary propagation increases the size of the formula (although it yields clauses that are no larger than the clauses resolved). This increase can slow down the solution process considerably and the increased memory con­ sumption can lead to thrashing. Consequently, one must ei­ ther restrict the extent of binary propagation or devise fast, ef­ ficient methods for performing them.

We experimented with a simple preprocessing step which resolves pairs of binary clauses until no new clauses are de­ rived. This method can be used by systematic and stochastic methods as a simplification step, and it can be implemented ef­ ficiently. It is not always useful, as sometimes no or few unit clauses are deduced. Yet, the overhead it incurs is relatively low, especially when we consider the more complex exam­ ples, and it seems to be a useful enhancement. In Table 2, we see a comparison of the running time ofBayardo and Schrag's REL-SAT algorithm with and without the preprocessing step. We also show the time required for binary-binary resolution and the number of unit clauses derived. 4

We also experimented with the performance of the SATZ algorithm [Li and Anbulagan, 1997] on the above instances with and without bin/bin resolution. In Table 3 we give the running times for SATZ as applied to the original and the sim­ plified formula for those instances in which they differ. In ad­ dition, we conducted a number of experiments in which we attempted to resolve binary clauses with clauses of arbitrary size. We found the overhead of this method too large.

4 Conclusion

We have shown a connection between the scheme used to en­ code planning instances and the ability to propagate reach­ ability and relevance information from the initial and final steps to other time points. We compared this ability to that of the Reachable-k and Relevant-k algorithms, the first be­ ing a generalization of GRAPHPLAN's planning graph, and the second being a natural extension into relevance analysis. We also pointed out the fact that binary clauses form a major part among all clauses in sat-encoded planning problems, and we attempted to exploit this phenomena. Our initial experiments show nice improvements in instances where unit clauses can be derived from binary resolution, and a small overhead other­ wise. We are currently experimenting with various extensions of the Davis-Putnam procedure that perform limited amounts of binary resolution during the search process.

ftp://ftp.research.att.com/dist/aillogistics.tar.Z and

4 See satplan.data.tar.Z for the instances used.

This work is among the first attempts to theoretically an­ alyze different encoding schemes. We have concentrated on one particular aspect of such encodings, i.e., their ability to propagate concrete state information backwards and for­ wards. Naturally, this attempt is a-priori limited in its scope, as this ability is only one factor influencing the performance of various algorithms, and its influence is probably more signif­ icant in systematic methods based on the David-Putnam pro­ cedure than in methods based on stochastic local search.

Other authors have considered some of the ideas presented here, too. Kautz and Selman (1996) point to the ability to backward propagate information thanks to the encoding of effects in the GRAPHPLAN encoding. Kautz and Selman (1998) mention a relation between GRAPHPLAN's mutex con­ straints and binary propagation. Recent work on this planner employs Crawfords's COMPACT algorithm which uses are­ stricted form of binary propagation to reduce the size of the formula. Finally, [Ernst et al., 1997] discuss optimizations performed on sat-encoded planning problems, among them the use of type inference and a form of dataflow analysis that seems related to Reachable-!.

Acknowledgments

I wish to thank Craig Boutilier and Chris Geib for valuable discussions on reachability analysis and the anonymous re­ viewers for their useful comments. This work was partially funded by the Paul Ivanier Center for Robotics Research and Production Management.