Planning with SAT, Admissible Heuristics and A*

1 Introduction

We investigate the relations between two main approaches to finding optimal plans: state-space search with heuristic search algorithms such as A∗ , and the reduction to the propositional satisfiability problem SAT. Our optimality criterion is the minimality of the number of actions in a plan.

The theoretical limitations of the leading approaches to the optimal planning problem are well understood. A∗ [Hart et al., 1968] is the best-known optimal search algorithm, which is guaranteed to expand the smallest possible number of states of any algorithm that does search state-by-state. The performance of A∗ is determined by the heuristic it uses. With a perfect heuristic it expands only the states corresponding to one optimal action sequence from the initial state to a goal state. With less informed heuristics the memory consumption is typically much higher. For example, with the trivial heuristic h(s) = 0 it will expand all states with a distance < k - 1 from the initial state when k is the length of the shortest path to a goal state. For short (polynomially long) plans A∗ still requires an exponential amount of memory in the worst case.

Planning by reduction to SAT, as proposed by Kautz and Selman [1992], has slightly different computational limitations. The sizes of the required formulas are linearly proportional to the length of action sequences considered. These action sequences may have an exponential length with respect to the representation of the problem instance, and, similarly to A∗ , will in this case require an exponential amount of memory. However, for short plans (polynomial in the size of the representation), even when A∗ expands an exponential number of states, the corresponding SAT problem can be solved in polynomial space (simply because SAT∈NP and NP⊆PSPACE.) This optimal space bound is achieved by well-known algorithms for the SAT problem, including the Davis-Putnam-Logemann-Loveland procedure [Davis et al., 1962]. A counterpart of SAT in the state-space search domain is the iterative deepening A∗ (IDA∗ ) algorithm [Korf, 1985] which stores in the memory, at any given time, only one bounded-length path in the state-space, and not all visited states like A∗ does. Under mild assumptions, IDA* does not perform many more search steps than A∗ [Korf, 1985, Theorem 6.4]. Although the worst-case resource requirements of SAT and IDA∗ are the same, the results of our work show that there is a simple implementation of SAT-based planning that is guaranteed to never do worse than state-space search with IDA∗ , and will sometimes perform exponentially better.

Our first result shows that if a given heuristic is encoded in the SAT problem, the Davis-Putnam-Logemann-Loveland procedure [Davis et al., 1962] can simulate state-space search with IDA∗ [Korf, 1985], the iterative deepening variant of A∗ [Hart et al., 1968], within the same time and space bounds. Our second result shows that the opposite does not hold: we construct a planning problem that requires an exponential amount of computation by A∗ and IDA∗ , but only a short resolution proof which is constructed by the unit propagation procedure in linear time.

The structure of the paper is as follows. In Section 2 we present the background of the work in SAT. Section 3 relates the notion of admissibility to the SAT framework and shows that one of the best known admissible heuristics is implicit in it. Section 4 presents a simulation of IDA∗ with the DavisPutnam-Logemann-Loveland procedure for SAT. In Section 5 we show that both IDA∗ and A∗ are sometimes exponentially worse than SAT. We conclude by discussing related work in Section 6 and future research topics in Section 7.

2 Technical Background

Let Σ be a set of propositional variables. Formulas (over Σ) can be recursively constructed as follows. Every a ∈ Σ is a formula. If φ is a formula, then so is ¬φ. If φ1 and φ2 are formulas, then so are φ1 ∨ φ2 and φ1 ∧ φ2. We also use ⊤ for the constant true and ⊥ for false. For propositional variables x ∈ Σ, x and ¬x are literals. The complement l of a literal l is defined by x = ¬x and ¬x = x when x ∈ Σ. A finite disjunction of literals is a clause.

A valuation of Σ is a (total) function v : Σ → {0, 1}. A formula φ is satisfied by v (written v |= φ) if the following holds. If φ = x for some x ∈ Σ, then v |= φ iff v(x) = 1. If φ = ¬φ1, then v |= φ iff v¬ |= φ1. If φ = φ1 ∧ φ2, then v |= φ iff v |= φ1 and v |= φ1. If φ = φ1 ∨φ2, then v |= φ iff v |= φ1 or v |= φ2. The logical consequence relation φ |= φ′ holds if v |= φ implies v |= φ′ for all valuations v. We use these notations also for sets of clauses. A formula φ (over Σ) is satisfiable if and only if v |= φ for some valuation v of Σ.

2.1 Planning

Planning problems are expressed in terms of a set F of facts (Boolean state variables) and a set of actions. Each action has a precondition C ⊆ F, consisting of the facts that have to be true for the action to be possible, and a set P of facts that become true (the add effects) and a set N of facts that become false (the delete effects). We define prec(〈C, P, N〉) = C and eff(〈C, P,N〉) = P ∪ {¬f|f ∈ N}. An action is possible in state s (a valuation of F) if s |= C. The successor state s′ = succa(s) of s with respect to a = 〈C, P, N〉 satisfies the following: s′ |= l for all l ∈ eff(a) and s′ (f) = s(f) for all f ∈ F\(P ∪N).

A problem instance is 〈F, I,A,G〉, where F is a set of facts, I is a state, A is a set of actions, and G is a set of literals. The objective is to find a shortest sequence of actions such that succan (succan-1 (succa2 (succa1 (I)))) |= G.

2.2 Planning in the Propositional Logic

Planning was first represented in the propositional logic by Kautz and Selman [1992]. The idea is to look at the bounded length planning problem with time points 0, . . . , T . A propositional formula encodes the possible plans and their executions by describing how the state can change between two consecutive time points.

In this paper, we use a simple and efficient encoding based on explanatory frame axioms. The propositional variables we use are f@t for facts f ∈ F and t ∈ {0, . . . , T}, a@t for actions a ∈ A and t ∈ {0, . . . , T - 1}.

We translate the action a = 〈C, P,N〉 into the following propositional clauses for all t ∈ {0, . . . , T - 1}.

For every fact f and time t ∈ {0, . . . , T-1} we have frame axioms that state when facts remain unchanged.

Here ak1 , . . . , akm are all the actions that change f from false to true. and an1 , . . . , ans are all the actions that change f from true to false.

Additionally, at most one action can take place at a time, which is expressed by the clauses

¬a@t ∨¬a′@t for all a, a′ ∈ A, t ∈ {0, . . . , T -1}, (6)

and at least one action must take place, expressed by

For given sets of facts and actions and an integer T, we denote the set of all the above clauses by HT . The action sequences can be restricted to plans that reach some goals from some initial state by using HT with additional clauses.

For a given state s : F → {0, 1}, we define a clause set representing s by lits(s) = {f ∈ F|s(f) = 1} ∪ {¬f|f ∈ F, s(f) = 0}. For a clause set S over F, we define the set S@t in which every propositional variable f ∈ F has been replaced by its time-tagged variant f@t.

Let I be the initial state and G a set of literals that describes the goal states. The optimal planning problem can be defined as finding a T so that lits(I)@0∪HT ∪G@T is satisfiable and lits(I )@0 ∪ HT -1 ∪ G@(T - 1) is unsatisfiable. An optimal plan can be easily constructed from a valuation that satisfies the first clause set.

2.3 Resolution Proof Systems

The resolution rule defines one of the simplest proof systems for the propositional logic. It is used for showing that a set of clauses is unsatisfiable.

Definition 1 (Resolution) Let c1 = l1 ∨ · · · ∨ ln and c2 = l1 ∨ l′2 ∨ · · · ∨ l′m be two clauses. The resolution rule allows deriving the clause c3 = l2 ∨ · · · ∨ ln ∨ l′2 ∨ · · · ∨ l′m. We use the notation c1, c2 ⊢ c3 for this. As a special case, resolving the unit clauses l1 and l1 results in the empty clause.

Definition 2 (Derivation) Let S = {c1, . . . , cn} be a set of clauses. A resolution derivation of the clause c from S is any clause sequence c′1 , . . . , c′m with the following properties.

1. For every i ∈ {1, . . . ,m}, either c′i ∈ S or c′j , c′k ⊢ c′i for some 1 ≤ j < k < i.

Definition 3 (Refutation) Let S = {c1, . . . , cn} be a set of clauses. A resolution refutation of S (which shows S to be unsatisfiable) is any resolution derivation of the empty clause from S.

A simple special case of the resolution rule is unit resolution, which infers φ from a unit clause l and another clause l ∨ φ, where φ is a disjunction of literals. This rule leads to a very simple and efficient, but incomplete, inference procedure, which performs all unit resolution steps with a given clause set. This procedure can be implemented in linear time in the size of the clause set, and because there is (only) a linear number of possible unit resolution steps (each clause need to be involved at most once), it can be performed exhaustively. The fact that the clause c can be derived from S by unit resolution is denoted by S ⊢UP c. The unit propagation procedure is a component of virtually all systematic SAT algorithms, including the Davis-Putnam procedure [Davis et al., 1962] or the conflict-driven clause learning (CDCL) procedure [Mitchell, 2005].

3 Admissible Heuristics and Planning as SAT

Lower bound functions (heuristics) in algorithms such as A∗ are used for search space pruning. We denote a given lower bound for the distance from a state s to a goal g by hg (s).

Any admissible heuristic hg (s) is implicit in a logic formalization of planning, because admissibility means that the information given by the heuristic is a logical consequence of the formula that represent the planning problem: hg (s) is a true lower bound for the distance for reaching the goals from state s, not just an estimate. In this abstract sense, as far as only logical consequence is considered, all admissible heuristics are redundant.

Proposition 4 Let h be an admissible heuristic, s a state, g a formula, T and t ≤ T non-negative integers, and hg (s) = n. Then lits(s)@t∪HT |= ¬g@t′ for all t′ ∈ {t, . . . ,min(T, t+ n - 1)}.

The above is simply by the definition of admissibility and the properties of the formalization of action sequences in the propositional logic: If g cannot be reached by less than n actions, then g must be false in all time points before n.

Although logically redundant, the information in admissible heuristics may be useful for algorithms for SAT because of the pruning of the search space.

We propose a notion of an implementation of an admissible heuristic for the unit propagation procedure.

Definition 5 Let f be a fact. A clause set χT (for the plan length T ) implements the admissible heuristic hf (s) if for all t ∈ {0, . . . , T}, all states s, and all t′ ∈ {t, . . . ,min(T, t + hf (s) - 1)}, we have lits(s)@t ∪ HT ∪ χT ⊢UP ¬f@t′ .

The heuristic and χT may depend on a given initial state, but we have not expressed this possible dependency in the above definition. We don't discuss this issue further here.

Next we will show that HT , alone, encodes one of the best known (but by no means the strongest) admissible heuristics, with χT as the empty set. This is the hmax heuristic of Bonet and Geffner [2001]. It is implicit in the planning as SAT approach in the strong sense that it is inferred by the unit propagation procedure. The heuristic can be defined as follows.

Definition 6 (hmax [Bonet and Geffner, 2001]) The hmax heuristic for all f ∈ F is defined by the equation

for which a solution can be obtained as the least fixpoint of a procedure that starts with

and repeatedly performs updates hfmax (s) := min(hfmax (s), mina∈A,f∈eff(a)(1+maxf ′∈prec(a) hf ′max (s))) for every f ∈ F until no change takes place.

It is easier use the above fixpoint iteration to first identify all facts with lower bound 0, then those with lower bound 1, 2 and so on. We do this implicitly in the next proof.

Theorem 7 The empty clause set χT = ∅, for any T ≥ 0, implements hfmax for any fact f.

Proof: We have to show that lits(s)@t ∪HT ⊢UP ¬f@t′ for any state s, any T ≥ 0, any fact f, and any t and t′ such that t′ ∈ {t, . . . ,min(T, t + hfmax (s) - 1)}. The proof is by nested inductions, one with T which we leave implicit to simplify the presentation.

Base case hfmax (s) = 1: hfmax (s) = 1 implies s ̸|= f. Hence ¬f@t is one of the unit clauses in lits(s)@t, and we immediately have lits(s)@t ∪ HT ⊢UP ¬f@t.

Inductive case hfmax (s) > 1: We show by induction that lits(s)@t ∪ HT ⊢UP ¬f@(t + i) for all i ∈ {0, . . . , min(T - t, hfmax (s) - 1)}.

Base case i = 0: Proof of lits(s)@t ∪ HT ⊢UP ¬f@t for i = 0 is as in the base case.

Inductive case i ≥ 1: Since hfmax (s) > i, for every action a ∈ A with f ∈ eff(a) we have hf ′max (s) > i - 1 for at least one f ′ ∈ prec(a). By the outer induction hypothesis we have lits(s)@t ∪ HT ⊢UP ¬f ′@(t + i - 1). By Formula 1 we have lits(s)@t ∪ HT ⊢UP ¬a@(t + i - 1). As this holds for all actions that make f true, by the frame axiom 4 and the inner induction hypothesis lits(s)@t ∪ HT ⊢UP ¬f@(t + i - 1) we have lits(s)@t ∪ HT ⊢UP ¬f@(t + i).

□

All admissible heuristics commonly used in planning are computable in polynomial time. The question of whether an admissible heuristic can be encoded compactly is essentially the question of circuit complexity of the corresponding lower bound functions [Balc´azar et al., 1988; Papadimitriou, 1994]. Since every polynomial time function can be represented as a polynomial circuit [Papadimitriou, 1994], all of these heuristics can indeed be expressed "compactly" as formulas. For some admissible heuristics it is obvious that their representation is so compact that it is practically usable, for example pattern databases, but for others it is less obvious.

4 Simulation of IDA∗ with SAT search

Next we give a simulation of a bounded horizon search with IDA∗ in the DPLL procedure [Davis et al., 1962], showing that with a very simple and natural branching rule, DPLL is at least as powerful as state-space search with IDA*. DPLL can be viewed as a resolution proof system, and it is one of the least powerful of such complete systems [Beame et al., 2004]. Hence this result shows that several other resolution proof systems, including conflict-driven clause learning [Beame et al., 2004; Pipatsrisawat and Darwiche, 2009], are more powerful than state-space search with IDA*.

To obtain the result, we limit the DPLL procedure to choose only action variables as branching variables, assign

• 1: procedure DPLL(S)
• 2: S := UP(S);
• 3: if {x, ¬x} ⊆ S for any x then return false;
• 4: x := any variable such that {x, ¬x} ∩ S = ∅;
• 5: if DPLL(S ∪ {x}) then return true;
• 6: return DPLL(S ∪ {¬x})

Figure 1: The DPLL procedure

all variables for time t before proceeding with time t+1, and always choose the truth-value true first.

The next lemma shows how unit propagation computes successor states with the encoding from Section 2.2.

Lemma 8 Let s and s′ be states, a1, . . . , ak a sequence of actions so that s′ = succak (· · · succa1 (s) · · · ). Let k ≤ n. Let La = ⋃n-1 i=0 A@i. Let L+a = {a1@0, . . . , ak@(k - 1)}. Then lits(s)@0 ∪ Hn ∪ L+a ∪ {¬a@t|a@t ∈ La\L+a } ⊢UP lits(s′ )@k.

The main result of the section shows that DPLL search trees never have more nodes than IDA∗ search trees.

Theorem 9 Let N be the size of a failed IDA∗ search tree with heuristic h and depth-bound T. Then there is a DPLL search tree of size less than 2N that shows lits(I)@0∪HT ∪ χT ∪ g@T unsatisfiable.

Proof: The DPLL procedure is given in Figure 1. It uses the unit propagation procedure UP(S), which resolves every unit clause l with clauses l ∨ φ to obtain φ (or the empty clause when resolving l and l) which is added to S. When no further clauses can be derived, the resulting clause set is returned.

We prove that the number of nodes in the DPLL search tree is at most that of the IDA* search tree, when the variable on line 4 is always chosen so that it is an action variable a@t and for all actions variables a′@t′ such that t′ < t, either a′@t′ ∈ S or ¬a′@t′ ∈ S.

The proof is by mapping IDA* search trees to DPLL search trees of slightly different structure, and showing that DPLL traverses the trees at most as far as IDA* does. The difference between the search trees of DPLL and state-space search with IDA* and DPLL is illustrated in Figure 2. The node in the IDA* tree on top has 4 successor nodes, corresponding to the actions A, B, C and D. The DPLL tree has binary branches only, with an action and its negation as the two arc labels, as required by the DPLL procedure. The last (rightmost) successor of any node does not have its action as a branching variables. In our example, D@t is not a branching variable. Instead, it is inferred from ¬A@t, ¬B@t, ¬C@t and the axiom 7 from Section 2.2. A node with n successors requires a total of 2n - 1 nodes in the corresponding DPLL search tree. Hence there are less than twice as many nodes in the DPLL tree. A full example of an IDA* search tree, with each branch cut-off after two actions, and the corresponding DPLL search tree are given in Figure 3.

When IDA* has reached a node in depth n corresponding to an action sequence a1, . . . , an, the corresponding state is s′ = succan (· · · succa1 (I) · · · ). The clause set in the corresponding node in the DPLL search tree includes the same actions as literals a1@0, . . . , an@(n - 1) and the negations of all other action variables for time points ≤ n - 1. Hence by Lemma 8 DPLL has inferred the set lits(s′ )@(n - 1). If n + h(s′ ) > T, the node will be a cut-off node for IDA*. Because χT implements the heuristic h, by Definition 5 we have lits(s′ )@(n - 1) ∪ HT ∪ χT ⊢UP l@T for at least one goal literal l ∈ G. Hence DPLL will backtrack in this node, if it has not backtracked earlier (and sometimes it has, as shown by Theorem 10.) Therefore the DPLL search tree will not be expanded further than the IDA* search tree, and it is - in terms of the number of nodes - less than twice the size. □

The above theorem assumes that the IDA* search does not detect cycles. Cycles can be eliminated from the DPLL search by encoding a constraint that says that the states at any two time points are different. Eliminating the cycles, for both IDA* and DPLL, is not necessary for the correctness or the termination of the search, but may improve performance.

The above result is not specific to DPLL. A similar simulation is possible with other systematic proof methods for SAT, for example the CDCL algorithm. A close correspondence between the branches of a search tree (paths from the root to a leaf, as in Figure 3) and the clauses learned by CDCL can be easily established. To sketch the proof idea, note that every branch in the DPLL tree in Figure 3 corresponds to a clause, for example A@0 ∨ ¬B@0 ∨ F@1 ∨ ¬G@1. It can be learned by the CDCL algorithm, similarly to the unit resolution derivation in the proof of Lemma 8. Resolving these clauses, for example A@0 ∨ ¬B@0 ∨ F@1 ∨ ¬G@1 with A@0∨¬B@0∨F@1∨G@1, yielding A@0∨¬B@0∨F@1, and this clause further with A@0 ∨ ¬B@0 ∨ ¬F@1, and so on, will eventually derive the empty clause.

5 Exponential Separation of A∗ and SAT

We show that some problems that are trivial for SAT (in the sense that a simple unit-resolution strategy will solve them) are very difficult for state-space search with both A∗ and IDA∗ when employing the same heuristic.

Theorem 10 State-space search with A∗ and a heuristic h is sometimes exponentially slower than any algorithm for SAT that uses unit resolution, if the latter implements h.

Proof: We give an example for which unit resolution immediately proves the lack of plans of length n - 1 when n is the shortest plan length, and finds a plan of length n, but A∗ with hmax will visit an exponential number of states.

The idea is the following (illustrated in Figure 4.) The goals can be reached with the action sequence y1, . . . , yk+2 of length k + 2. Seemingly (as far as hmax is concerned), the goals can also be reached with a k + 1 step plan consisting of k actions from {x1, x′1 , . . . , xk, x′k } followed by bad. However, bad irreversibly falsifies one of the goals. The actions x1, x′1 , . . . , xk, x′k induce a very large state space with 2k+1 - 1 states, which will be exhaustively searched by A∗ , making its runtime exponential in k.

On the other hand, unit propagation will immediately infer that action bad cannot be taken and that y1, . . . , yk+2 is the only possible plan. If T < k + 2, a refutation is immediately found. If T = k + 2, the unit resolution procedure will find a satisfying assignment.

Next we formalize the example in detail. The state variables are p1, . . . , pk+1 (of which exactly one is true in any reachable state), r2, . . . , rk+2 (of which at most one is true in any reachable state), b1, . . . , bk (which can be independently true or false), and g1 and g2. Only g1 and p1 are initially true. All other variables are false. The goal consists of g1 and g2. The actions are given in Table 1.

The hmax estimate for the state reached by action y1 from the initial state is k + 1 (which is also the actual distance.)

The hmax estimate for all states reached from the initial state by a sequence of i actions from the set {x1, . . . , xk, x′1 , . . . , x′k } is k-i+1 (which always seems better than taking the action y1 first), although the goals cannot be reached this way: the action bad fools hmax to think that goals can be reached with bad as soon as pk+1 has been made true, but bad actually irreversibly falsifies one of the goals.

The A∗ algorithm generates 2k states with pk+1 true and different values for b1, . . . , bk, as determined by the choices between xi and x′i for i ∈ {1, . . . , k}.

Next we show that lits(I)@0∪Hk+1 ∪{g1@k+1, g2@k+ 1} is found unsatisfiable by unit propagation.

The frame axiom for g1 is g1@t ∨ ¬g1@(t + 1) because none of the actions makes g1 true. Hence from the goal literal g1@k+1 we can infer g1@k, g1@(k-1), . . . , g1@1 with unit resolution, and therefore the bad action can be inferred to be never possible: we get ¬bad@k, . . . , ¬bad@0.

From ¬r2@0 (initial state) and r2@0 ∨ ¬r2@1 ∨ y2@0 (frame axiom) and ¬y2@0∨r2@0 (precondition) we can infer ¬r2@1 with unit resolution. Similarly we can infer ¬ri@1 for all i ≥ 3, and, more generally, ¬ri@j and ¬yi@j and ¬g2@(j + 1) for all 1 < j < i ≤ k + 2. Since g2@k + 1 belongs to the clause set, we have derived the empty clause. The number of unit resolution steps is quadratic in k and linear in the size of the clause set.

When there are k+2 time points, the same reasoning shows that unit propagation yields y1@0, . . . , yk+2@(k + 1) and ¬g2@(k + 1). As yk+2 is the only action that can make g2 true, we get yk+2@(k + 1) by unit resolution from the frame axiom. The rest of the plan is obtained analogously. □

The above proof can be adapted to other admissible heuristics that use a delete-relaxation or other simplification that makes it seem that the action bad does not delete g2.

6 RelatedWork

The power of different limited inference methods for approximate reachability (e.g. planning graphs) have been investigated earlier [Brafman, 2001; Geffner, 2004; Rintanen, 2008]. All three works investigate ways of strengthening inference with SAT to derive the invariants/mutexes in planning graphs. None of them attempts to relate SAT to state-space search, and the only result that is directly related to ours is Brafman's Lemma 1 which shows that for a sequential encoding (one action at each time point) Reachable-1 - which is closely related to hmax - is stronger than unit propagation. This seems to conflict with our Theorem 7, which shows unit propagation to be at least as strong. This discrepancy is due to our use of explanatory frame axioms. Brafman's Lemma 3 for parallel plans uses explanatory frame axioms, and then unit propagation is at least as strong as Reachability-1.

7 Conclusions

We have shown that IDA∗ search for state-space reachability problems can be efficiently simulated by DPLL search. Our results also show that unit resolution is sometimes exponentially more efficient than state-space search with A∗ or IDA∗ : A∗ and IDA∗ need exponential time, but short resolution proofs are immediately found with unit resolution. The work complements recent experimental results that suggest that SAT-based methods for non-optimal planning are at least as strong as state-space search [Rintanen, 2010].

One could view Theorems 9 and 10 as suggesting a simple IDA∗ style state-space search algorithm extended with some (unit) resolution inferences. Such a procedure would in some cases improve IDA∗ , but would not fully benefit from the power of modern SAT algorithms. Much of that strength comes from the less rigid structure of the proofs, which would mostly be lost in a pure forward-chaining state-space search. The general challenge is to utilize this strength and guarantee a performance that typically exceeds A∗ and IDA∗ , also for problems that would seem to be more suitable for forwardchaining state-space search.

A more direct avenue to useful implementations is to enhance SAT-based optimal planning with encodings of more powerful admissible heuristics than hmax. Unlike state-space search algorithms, SAT-based methods can take advantage of lower bounds for arbitrary facts (not only goals) as additional constraints. This suggests that the more powerful lower bounding methods have much more to contribute than what is currently utilized by state-space search methods. This is an important topic for future work.