Abstract:
In recent years, there is a growing awareness of the importance of reachability and relevance-based pruning techniques for planning, but little work specifically targets these techniques. In this paper, we compare the ability of two classes of algorithms to propagate and discover reachability and relevance constraints in classical planning problems. The first class of algorithms operates on SAT encoded planning problems obtained using the linear and Graphplan encoding schemes. It applies unit-propagation and more general resolution steps (involving larger clauses) to these plan encodings. The second class operates at the plan level and contains two families of pruning algorithms: Reachable-k and Relevant-k. Reachable-k provides a coherent description of a number of existing forward pruning techniques used in numerous algorithms, while Relevant-k captures different grades of backward pruning. Our results shed light on the ability of different plan-encoding schemes to propagate information forward and backward and on the relative merit of plan-level and SAT-level pruning methods.

---

Extracted Text

Journal of Artificial Intelligence Research 14 {2001} 1-28 Submitted 2/00;
published 1/01
 On Reachability, Relevance, and Resolution in the Planning
 as Satisfiability Approach Ronen I. Brafman brafman@cs.bgu.ac.il Department
of Computer Science, Ben-Gurion University
 P.O.Box 653, Beer-Sheva 84105, Israel
 Abstract
 In recent years, there is a growing awareness of the importance of reachability
and
 relevance-based pruning techniques for planning, but little work specifically
targets these techniques. In this paper, we compare the ability of two classes
of algorithms to propagate
 anddiscover reachability and relevance constraints in classical planning
problems. The first
 class of algorithms operates on SAT encoded planning problems obtained using
the linear and Graphplan encoding schemes. It applies unit-propagation and
more general resolu-
 tion steps {involving larger clauses} to these plan encodings. The second
class operates at
 the plan level and contains two families of pruning algorithms: Reachable-k
and Relevant-
 k. Reachable-k provides a coherent description of a number of existing forward
pruning
 techniques used in numerous algorithms, while Relevant-k captures different
grades of back- ward pruning. Our results shed light on the ability of different
plan-encoding schemes to
 propagate information forward and backward and on the relative merit of
plan-level and
 SAT-level pruning methods. 1. Introduction
 The success of the planningas satisfiability {PAS} approach {Kautz & 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 compared {Ernst, Millstein, & Weld, 1997},
and various sys-
 tematic alternatives to the original stochastic method have been examined
{e.g., Bayardo
 &Schrag, 1997; Li & Anbulagan, 1997}. Still, many issues surrounding this
approach are
 poorly understood. In particular, little is known about the influence of
the encoding method on performance.
 Concentratingon 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
 propagatereachability 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 a class of algorithms for reachability and relevance analysis that operate
on the original problem formulation: Reachable-k and Relevant-k. Reachable-k
is a simplifiedvariant of
 a similar algorithm for state pruning in Markov decisionprocesses {Boutilier,
Brafman, &
 Geib, 1998}, while Relevant-k isa natural counterpart used for relevance
analysis. Both algorithms provide a coherent framework for discussing different
grades of reachability and
 relevance-based pruningmethods that appear in the literature.
 Our work is motivated by the growing role that forward and backward pruningmethods
play in current planning algorithms and the important role of propagation
techniques in
 c
 fl2001 AI Access Foundation and Morgan Kaufmann Publishers. All rights reserved.Brafman
 all SAT solvers used in the planning as satisfiability approach. Unit propagation
plays
 a central role in the Davis-Putnam algorithm {Davis & Putman, 1960} and
many of its
 offsprings {e.g., Crawford & Auton, 1993; Freeman, 1995; Gomes, Selman,
& Kautz, 1998;
 Li & Anbulagan, 1997} and it is used as a preprocessing step when stochastic
methods are
 applied. Moreover, a limited form of binary propagation is used in Crawford's
Compact
 program for simplifying CNF formulas which is utilized in the Blackbox planner
{Kautz & Selman, 1999}. Our results shed some light on the relationship between
these pruning
 techniques.
 The paper is organized as follows. Section 2 provides background material,
describing
 the basic ideas of the PAS framework and the Graphplan algorithm. In Section
3, we
 discuss Reachable-k , an algorithm for performing reachability analysis,
and compare its
 ability to prune possible actions to that of k-clause resolution. In Section
4 we describe
 Relevant-k which is similar to Reachable-k and is applied to relevance analysis.
Again, we
 compareit to methods based on resolution. In Section 5 we empiricallycompare
the results
 of various methods for k =1; 2. We conclude with a discussion of future
and related work in Section 6. Proofs appear in the appendix, but their main
arguments are described in the
 body of the paper. 2. Background
 The Graphplan algorithm {Blum & Furst, 1997} and the Satplan algorithm {Kautz
& Selman, 1996} have profoundly altered the direction of research within
the planning community. Two of the main concepts studied in this paper, reachability
analysis and plan
 encodings, have become central to current planning research thanks to these
planners. We
 briefly discuss these planners, and in particular, their aspects pertaining
to our topic. 2.1 Reachability Analysis in Graphplan
 The purpose of reachability analysis is to discover unreachable states of
the world and
 infeasible actions, i.e., actions that cannot be performed in the course
of a successful plan.
 By discovering such actions ahead of time, we reduce the space that needs
to be searched to
 find a valid plan. In principle, full fledged reachability analysis requires
forward search in
 the space of possible states. This is a very expensive operation, and instead,
we can opt for sound, but incomplete methods. Such methods do not discover
all the actions that can be
 ruled out. However, any action that they rule out is infeasible and need
not be considered
 when searching for a plan.
 The Graphplan planner provides a good example of the utility of approximate
reach-
 ability analysis. Graphplan has two main stages: In the first stage, approximate
reach- ability analysis is conducted, yielding a data-structure called the
planning graph which
 represents a sound, but incomplete, approximation of the set of states reachable
from the
 initial state. In the second stage, Graphplan searches for a plan over this
structure. Graphplan's planning graph construction algorithm presents a particularly
good tradeoff
 between computational complexity and pruning power, and its utility in pruning
the search
 space is attested to by the planner's good performance.
 The planning graph construction algorithm can be viewed as generating a
list of anno-
 tated sets. The odd elements in this list contain sets of propositions.
The even elements
 2Reachability, Relevance, and Resolution
 in this list contain sets of actions. Each such set is annotated with mutual
exclusion con- straintson its members. Intuitively, the i
 th
 action set contains the list of actions that could be performed at the i
 th
 step of a concurrent action plan {i.e., a plan allowing for concurrent execution
of actions that do not interfere with each other}. The i
 th proposition set contains
 propositions that could hold after i 000 1 {sets of concurrent} actions
have been performed.
 The mutual exclusion constraints circumscribe these sets by indicating that
certain pairs of
 actions or propositions cannot occur at the same time at a particular stage.
Hence, if the
 propositions p; q appear in the i
 th proposition set, then it is possible {or more accurately
 { the algorithm does not rule out the possibility}that an i-step plan applied
at the initial state could lead to a world in which p and/or q hold. However,
if p and q are marked mutually exclusive then we know that p and q cannot
hold together after some i-step plan
 has been performed.
 The sets are constructed as follows: The first proposition set contains
the propositions
 that hold at the initial state. The first action set contains the actions
that can be performed
 at the initial state. In general, the i
 th set of propositions contains the effects of actions in
 the i-1 th
 action set, and the i
 th
 action set contains actions whose preconditions appear in the i-1
 th
 set of propositions, provided that their preconditions are not marked as
mutually exclusive. Mutual exclusion constraints are added as follows: Two
actions are marked
 mutually exclusive at the i
 th
 action set if their preconditions are marked mutually exclusive at the i-1
 th . Clearly, if all the preconditions of these actions cannot hold at this
time point, we cannot perform both actions together at this time point. Another
reason for
 marking actions as mutually exclusive is if they conflict. That is, if one
action destroys a
 precondition or an effect of the other action. Two propositions at the i
th
 proposition set are marked mutually exclusive if all pairs of actions in
the i-1
 th
 action set that have them as effects are mutually exclusive. When that is
the case, there is no way for us to achieve
 bothof these propositions together at this stage.
 The initial construction of the planning graph is terminated once all goal
propositions
 appear in the last proposition set. At that point, Graphplan performs a
form of regression-
 based search on the planning-graph structure. If this search fails, the
planning graph is
 extended by one additional layer of actions and one additional layer of
propositions and
 searched again. For more details, see the article by Blum and Furst {1997}.
 2.2 The Planning as Satisfiability Approach
 The Planning as Satisfiability approach {PAS for short}, works as follows:
given a planning
 problem and a bound n on the size of the plan, the plan enco der generates
a propositional
 formula in conjunctive normal form. This formula has the following property:
it is satisfiable
 iff the planning problem has a solution with at most n time steps. Intuitively,
the formula
 is composed of propositions describing the state of the world throughout
the execution of ann-step plan.
 The propositional language on top of which the formula is defined contains
a proposition for each possibleaspect of the world at each time point. For
example, supposewe are looking at the blocks' world domain where states are
described using the on and clear relations.
 In that case, for any pair of blocks x; y, and any time point 0 024 t 024
n we shall introduce a proposition p
 on{x;y;t}
 which corresponds to x being on top of y at time t. Similarly, for
 3Brafman
 every block x and time point 0 024 t 024 n, we shall introduce a proposition
p
 clear{x;t}
 which
 corresponds to x being clear at time t.
 A truth assignment to the language described above can be viewed as describingthe
state
 of the world during the execution of an n-step plan. For instance, if p
 on{A;B;3}
 is assigned true , then block A is on top of block B at time 3. Of course,
most truth assignments to this language would not correspond to anything
resembling the true state of the world
 during the execution of an actual plan. For example, both on{A,B} and on{B,A}
could be assigned true . The goal of the encoding scheme is to generate a
formula such that any
 assignment satisfying this formula will correspond to the true state of
the world during
 the execution of an actual plan that achieves the desired goal. Each axiom
in this formula
 places some constraint on the value of these propositions so that the combined
effect of
 these constraints is to ensure that the resulting formula has precisely
the desired truth
 assignments. For example, one type of axiom will be a conjunction of all
the propositions
 correspondingto the initial state. Any truth assignment satisfying this
axiom must ensure
 that these propositions hold at time 0. Another class of axioms could state
that if some
 action a is performed at time t then the world at time t 000 1 must satisfy
the preconditions of a. In the next sections we discuss two of the central
plan encodings in more detail.
 Once an appropriate formula has been generated, it is simplified using various
well
 known techniques. In particular, all simplifiers employ a unit-resolution
step {Genesereth & Nilsson, 1987}. Unit resolution {also known as unit prop
agation } works as follows: To
 satisfy a CNF formula, we must satisfy each of its clauses. In particular,
if one of the
 clauses contains a single literal {such a clause is known as a unit clause
} we immediately
 know that the variable appearing in this clause must be assigned an appropriate
value. Any
 clause containing the same literal will be satisfied now, and it can be
removed from the
 formula. Any clause c containing the negation of that literal can be resolved
against this unit clause, and the resulting clause {which is smaller than
c} can replace c. For example,
 suppose we have the formula {p} ^ {:q _ :p} ^ {r _ p}. The first disjunct,
{p} is a unit clause.
 Hence, p must be assigned true . This makes the third clause, {r _ p}, satisfied.
The second
 clause is now resolved with the first clause, and we replace {:q _ :p} by
{:q}. We now
 have a new unit clause, {:q}, and so the proposition q must be assigned
the value false . If
 we had additional clauses containing q or :q, we could remove them, or simplify
them, as
 appropriate. After simplification,we apply our favorite algorithm for finding
satisfying assignments, and if one is attained, a dec o der is used to obtain
an actual plan from this solution. If we
 do not find a satisfying assignment, we increase the value of n {the size
of the plan}, and
 try again.
 Finally, we note that the Blackbox planner {Kautz & Selman, 1999} combines
PAS
 with Graphplan's reachability analysis. It constructs a planning graph,
and uses it to
 generate a particular plan encoding.
 3. Reachability and Resolution
 Reachability and relevance analysis form an essential part of successful
modern planning
 algorithms. The most notable example of reachability analysis is Graphplan's
planning
 graph {Blum & Furst, 1997}, and many recent plannersemploy either reachability
analysis
 4Reachability, Relevance, and Resolution
 {e.g., Bonet, Loerincs, & Geffner, 1997}, relevance analysis {e.g., McDermoot,
1996; Nebel, Dimopoulos, & Koehler, 1997}, or both {Kambhampati, Parker,
& Lambrecht, 1997}. The
 importance of reachability and relevance analysis has been noted in the
context of decision-
 theoretic planning as well. For example, Boutilierand Dearden {1994} employ
relevance
 analysis to reduce the state-space, and Boutilier, Brafman, andGeib {1998}
describe a
 general method for reachability analysis for MDPs. Below, we discuss this
method in a
 simplified form suitable for classical planning problems described using
the Strips repre-
 sentation language {Fikes & Nilsson, 1971}. In Section 4, we 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.
 3.1 Propagating Reachability Information
 Reachable-k {Boutilier,Brafman, & Geib, 1998} is an algorithm for estimating
the states
 reachable from a given initial state. As formulated, it is quite general
and applies to do-
 mains with non-deterministic actions and conditional effects. In Figure
1, we present a
 simplified version of that algorithm, Reachable-k, which deals with deterministic,
uncondi-
 tional actions represented in the Strips representation language. A prolog
implementation
 of Reachable-k isavailable at www.cs.bgu.ac.il/~pdm.
 An important reason for our interest in Reachable-k isits similarity to
the influen-
 tial planning graph construction of the Graphplan planner {Blum & Furst,
1997}. In
 fact, it generalizes the ideas behind Graphplan's planning graph, which
is equivalent to
 Reachable-2. We use A i
 to denote the set of actions feasible i steps from the initialstate, S
 i
 to denote the corresponding set of propositions, and C S
 003
 i
 to denote constraints on these
 propositions, such that if fp 1
 ; : : : ; p m
 g 2 C S 003
 i
 then these propositions cannot co-occur after i steps. C A
 003 i
 denotes similarconstraints on actions. Here, 003 2 fL; P g, where L is
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
 003
 i and C A
 003 i
 are empty for all i 025 0. {Actually, as defined, C A
 L
 i
 is not empty even when
 k = 1, but it plays no real part in the algorithm, and it should be ignored}.
Finally, note
 that in this description, the set of possible actions contains all actions
of the form noop[l], where l is a literal.
 When k = 2, S
 i
 and A
 i
 represent the propositional and action levels of Graphplan's
 planning graph, and C S
 i
 and C A P
 i
 hold their respective mutual exclusion constraints. We have not stated a
termination condition for Reachable-k, but one can be formulated
 based on the content of S
 i
 or the index i itself. In the PAS framework, where the number
 of time-steps is fixed, one would opt for the second alternative. Reachable-k
givesus sets of actions and propositions, A j
 ; S
 j , that could occur after the performance of j actions {or j sets of concurrently
non-conflicting actions} from the initialstate. It is easy to see that
 Reachable-k is sound in the following sense: Theorem 1 If a set of prop
ositions or actions is excluded by Re achable-k at time j then
 there is no feasible plan in which, at time j , these prop ositions hold
or, resp e ctively, these
 actionsappe ar.
 5Brafman
*  S
 0
 = literals that hold in the initial state. 
*  C S
 0
 = fg.
 
*  A 0
 = actions all of whose preconditions are in S
 0 .
 
*  C A
 L
 0
 = ffa i
 ; a
 j
 gja
 i
 ; a j
 2 A
 0 ; i 6= j; neither a
 i
 nor a j
 are noops or a j
 is a noop whose effect is destroyed by a
 i
 g.
 
*  C A
 P
 0
 = ffa
 i
 ; a
 j
 gja
 i
 ; a)
action version of the algorithm, and we shall not mention noops explicitly
or obvious
 mutual exclusion constraints between propositions and their negations.
 In the context of Reachable-1, C S
 i
 and C A
 i
 are empty, for all practical purpose. We
 start with S
 0
 = f:p
 1 ; :p
 2
 ; :p
 3
 ; :p
 4
 g; Only the action affecting the first bit is applicable, and
 A
 0 = fa
 1
 g {and all the relevant noops}; We now have S
 1 = fp
 1
 ; :p
 1
 ; :p
 2
 ; :p
 3
 ; :p
 4
 g. Because the preconditions for both a 1
 and a
 2 appear in S
 1 , we have that A
 1
 = fa
 1 ; a
 2
 g. Consequently
 S
 2
 = fp
 1 ; :p
 1
 ; p
 2
 ; :p 2
 ; :p
 3
 ; :p
 4 g. Now, we can also apply a
 3
 , and we have A
 2
 = fa 1
 ; a
 2 ; a
 3
 g; S
 3
 = fp
 1
 ; :p 1
 ; p
 2
 ; :p
 2
 ; p 3
 ; :p
 3
 ; :p
 4 g. Finally, at this stage all preconditions of a
 4
 appear as
 well, and A 3
 =fa
 1
 ; a
 2
 ; a
 3
 ; a 4
 g.
 Next, consider Reachable-2. Again, S 0
 =f:p
 1
 ; :p
 2
 ; :p
 3 ; :p
 4
 g, C S
 0
 is empty, and A
 0
 =
 fa
 1
 g. In the next step we have: S
 1
 = fp
 1
 ; :p
 1
 ; :p
 2
 ; :p 3
 ; :p
 4
 g, withno interesting constraints
 in C S
 1
 , andA
 1 = fa
 1
 ; a
 2
 g. However, now C A i
 contains {a 1
 ; a
 2 }, which are interfering actions. S
 2
 = fp
 1
 ; :p
 1
 ; p
 2
 ; :p
 2 ; p
 3
 ; :p
 3
 ; :p 4
 g, as in the case of k = 1. However, C S 2
 contains
 {p
 1
 ; p
 2
 }. This follows from the fact that the only actions in A
 1
 capable of producing p 1
 are
 a
 1
 and noop[p
 1
 ], and the only action in A
 1
 capable of producing p
 2
 is a
 2
 . a
 2 interferes
 with both a
 1
 an noop[p 1
 ]. Therefore, because C S
 2
 contains {p
 1 ; p
 2
 }, a
 3
 is not applicable at this stage. Hence, A 2
 = fa
 1
 ; a
 2 g, which is one action less than the set A
 2
 in Reachable-
 1. S
 3
 = S
 2
 = fp 1
 ; :p
 1
 ; p
 2
 ; :p
 2
 ; p 3
 ; :p
 3
 ; :p
 4 g. However, nowC S
 3
 does not contain {p
 1 ; p
 2
 } {because noop[p
 2 ] can be used to achieve p
 2
 , and it does not conflict with, e.g., noop[p
 1
 ]}.
 Therefore, A
 3
 = fa 1
 ; a
 2 ; a
 3
 g. To see how k = 3 improves our ability to prune over k =2, suppose that
S 0
 =
 fp 1
 ; p
 2 ; :p
 3
 ; :p
 4
 g {i.e., the counter's value is 0011} and consider k =2 first. We have
 A
 0 = a
 3
 and S
 1
 = f:p1; p1; :p
 2
 ; p
 2
 ; :p
 3
 ; p 3
 ; :p
 4
 g, with {p 1
 ; p
 3 }; {p
 1 ; :p
 2
 }; {:p
 1 ; p
 2
 } and
 {p
 2
 ; p
 3
 } in C S
 1
 . Each of these mutual exclusion relations stems from the fact that a
 3
 is mutually exclusive with noop[p
 1 ] and noop[p
 2 ]. Therefore, A
 1
 = fa
 1 ; a
 3
 g. Again
 S
 2
 = S
 1
 = f:p1; p1; :p 2
 ; p
 2 ; :p
 3
 ; p
 3
 ; :p
 4
 g, but now C S
 2
 contains {p
 1
 ; p 2
 } only, and so
 A
 2
 = fa
 1
 ; a 2
 ; a
 3
 g. Now, C S
 3
 is empty, and so A
 3
 = fa 1
 ; a
 2 ; a
 3
 ; a 4
 g. However, if k = 3,
 C S 1
 contains the ternary constraint {p
 1
 ; p 2
 ; p
 3 }. This ternary constraint remains in C S
 2
 as
 well, and in C S
 3 . Because it is in C S 3
 for k = 3, we have that a
 4 62 A
 3
 .3.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., unitpropagation,
is an integral part of all
 ma jor 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
 7Brafman
 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
 unreachable propositions or k-tuples of propositions}. Hence, for example,
a constraint of
 the form a{t} _ a
 0
 {t} implies that one of the actions a or a
 0 must appear at time t in the plan. A constraint of the form :a{t} _ :a
0
 {t} implies that one of the actions a or a
 0
 must not
 appear in the plan. Similar constraints on the propositions holding at a
time point can also be derived. In principle, such constraints reduce our
search space and could help us attain
 a solution more quickly. However, the effectiveness of such deduced constraints
depends
 on the precise algorithm used. Moreover, comparisonover a very large class
of constraints
 seems quite difficult. Therefore, inthis article we concentrate on a very
concrete class of
 reachability information of the form :a{t}, i.e., the action a cannot be
performed at any
 statereachable via t steps. These are powerful constraint which can be utilized
effectively by almost all planners {perhaps with the exception of partial-order
planners}. Consequently,
 we shall say that an algorithm Alg
 1
 generates more reachability information than another
 algorithm Alg
 2
 if whenever Alg 2
 is able to determine that some action a cannot be performed at some time
t, Alg 1
 is able to reach this conclusion as well, and in addition, there are such
 conclusions which Alg 1
 can reach but which Alg
 2
 cannot reach. Hence, Alg
 1
 generates a
 strict superset of the constraints on actions {of the type we are interested
in} generated
 by the other algorithm. Note that this does not mean that Alg
 1
 is better than Alg
 2
 on
 every instance, only that it is always as good, andin some cases better.
In this section
 we shall compare the pruning ability of the two Reachable-k variants and
two encoding methods discussed by Kautz and Selman {1996}:
 2
 the linear encoding and the Graphplan
 encoding. 3.2.1 Linear Plan Encoding The linear plan encoding {Kautz & Selman,
1992} is a simple 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 axioms}; 4. there
is at least one action at each time point;
 5. there is at most one action at each time point.
 Because we have explicitframe axioms, noops are not needed in the linear
encoding {as
 opposed to the Graphplan encoding}. In addition, the formula contains unary
clauses
 describingthe initialand goal states. However, for the purpose of analyzing
reachability
 effects, we exclude the description of the goal state {which plays a role
in relevance analysis}.
 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 whose2. The third {state-based} encoding method cannot be generated
automatically.
 8Reachability, Relevance, and Resolution
 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, thisis
identical to
 what Reachable
 003
 -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
 {discussed below}. Hence, except for the unlikely case in which a single
action is possible,
 there is no more that we can derive using unit propagation alone. Reachable
 003
 -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:
 Lemma 1 In the context of the linear enco ding, Re achable 003
 -1 yields more re achability in-
 formation than unit prop agation.
 Example: Consider a blocks' world domain with a single action schema move{ob
ject,source,
 destination}.
 3 Its preconditions are: on{ob ject,source}, clear{ob ject}, clear{destination}
 and its effects are: on{ob ject,destination}, clear{source}, :on{ob ject,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 table}. This
will be discovered by both algorithms. In particular, unit propagation will
yield a disjunction of all these actions.
 We know that all blocks that are 2 or more blocks below the top cannot participate
in
 the second move action. Reachable-1 willfind this out due to the fact that
they are not clear. Suppose that A is one such block. All initially feasible
move actions participate in a frame axiom of the form move{o,s,d}^:clear{A;
0} ! :clear{A; 1}, which, in clausal
 form is :move{o,s,d}_clear{A; 0} _ :clear{A; 1}. Resolving against :clear{A;
0}, we have :move{o,s,d}_: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 move{o,s,d} for some initially feasible action, and we
cannot make such
 a deduction.If we propagated information forward using axioms of class 2
and 3 and used binary
 resolution {as discussed before Lemma 1}, we now have a set of disjunctions
of the possible
 effects {including frame effects} of the initiallyallowable actions. The
number of such disjuncts is O{e
 m
 }, 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 disjunctionscould
 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
negations of
 some action's precondition, we can deduce the negation of this action by
resolving with
 axioms of class 1.
 Example: In the example considered above we would generate a disjunction
of the form
 move{o
 1
 ; s
 1
 ; d 1
 } _ move{o
 2
 ;s
 2
 ; d
 2
 } _ move{o
 3
 ; s
 3
 ; d
 3
 }, containing all instances of the move
 action for time 0 whose negations have not been deduced. As discussed above,
for all such actions, we can obtain a clause of the form :move{o
 i
 ; s
 i
 ; d
 i
 }_:clear{A; 1}. Once we resolve
 these binary clauses against the clause above, we obtain a unary clause
:clear{A; 1}, that3. In fact, since we use plain Strips, we need three action
schemas: one for moving a block to a block, one
 for moving a block to a table, and one from moving a block from the table.
However, as this does not affect our analysis, we stick to a single move
action in this and the following examples.
 9Brafman
 can be used in conjunction with class 1 axioms to deduce the negations of
step 2 actions
 whose preconditions include clear{A; 1}.As we saw, the effect disjunctionsdiscussed
above allow us to rule out certain proposi-
 tions or combinations of propositions. These are analogous to mutual exclusion
constraints. These mutual exclusion constraints can be used to prune actions.
For example, if we de-
 duce:p
 1 _ 001 001 001 _ :p m
 and all the p i
 are preconditions of some action a, we can deduce :a using binary resolution
{by resolving precondition axioms with this disjunction}. However,
 as we show below, binary resolution has trouble propagating even binary
mutual exclusion
 constraints forward. We believe that this is generally true, i.e., k-clause
resolution will have trouble propagating k-ary constraints. We can show the
following: Lemma 2 Re achable-2 and binary resolution {in the case of the
linear enco ding} are in- comp ar able.
 W e prove this by providing two examples. One in which Reachable-2 is able
to prune anaction that binary resolution cannot, and one in which the converse
hold.
 First, considerthe 4-bit counter with initial value 0000 {i.e., :p
 1
 ; :p
 2
 ; :p
 3 ; :p
 4
 }. Af-
 ter four steps we obtain the following: S
 4 = f:p
 1
 ; p
 1
 ; :p
 2
 ; p
 2
 ; :p
 3 ; p
 3
 ; :p
 4
 g and C S
 4
 =
 f{p
 1
 ; p
 3
 }; {p
 2
 ; p
 3 }g. Therefore, A 4
 = fa
 1
 ; a
 2 ; a
 3
 g. This implies that S
 5 = S
 4
 . We claim
 that {p 2
 ; p
 3 } 2 C S
 5 as well, which means that a
 4
 62 A
 5
 . To see this, consider all pairs of
 actions that have p
 2
 and p
 3
 as effects. They are: {a
 2
 ; a 3
 }; {a 2
 ; noop[p 3
 ]}; {noop[p
 2
 ]; a 3
 }, and
 {noop[p
 2
 ]; noop[p
 3
 ]}. {a
 2
 ; a
 3
 } is a pair of real actions, which are always mutually exclusive
 inthe linear encoding. The preconditions of {a
 2
 ; noop[p 3
 ]} are mutually exclusive according
 to C S
 4 , and so are the preconditions of {noop[p
 2
 ]; noop[p
 3 ]}. Finally, {noop[p
 2
 ]; a
 3
 } are
 interfering actions. We conclude that {p
 2
 ; p 3
 } 2 C S 5
 and a
 4
 62A
 5
 .
 When we run a binary resolution procedure on the linear encoding of this
problem,
 we could not deduce a 4
 62 A
 5 . This stems from the fact that ternary resolution is needed
 to propagate the mutual exclusion of p
 2
 and p
 3
 . Recall that we obtain mutual exclusion
 constraints by resolving against a disjunction of actions that have not
been ruled out. In
 the above case, at time 4 we would have the following disjunction: a
 4
 1
 _ a
 4
 2
 _ a
 4
 3
 _ noop[:p
 1
 ] _
 001 001 001 _ noop[6= p
 4 ]. Our goal is to deduce :p
 5
 2
 _ :p
 5
 3 using :p
 4 2
 _ :p
 4 3
 and the various axioms.
 To do this, we willtry to deduce either :p
 5 2
 _ :p
 5 3
 from each of the actions in the disjunction.
 It is easy to deduce :p
 5
 2
 from a
 4
 3 and :p
 5
 2
 from a
 4 2
 . However, we believe that it is impossible
 to deduce :p
 5
 2
 _ :p
 5 3
 from a
 4 1
 and from some of the noops. 4
 The reason for this is that such
 a deduction involves the use of frame axioms, which are ternary. If we know
that, e.g., :p 4
 2
 holds, we apply unit resolution to the frame axioms and obtain a binary
clause. However,
 here we only know :p
 4
 2 _ :p
 4
 3
 . Once we resolve this against a frame axiom we remain with a ternary clause.
To get our desired result we must resolve two such ternary clauses.
 Finally, let us see an example in which we use binary resolution to derive
a ternary
 constraint. By definition, Reachable-2 cannot derive such constraints. Suppose
that the initial state is :p; :q; :r. We have four actions: a1 has p; r as
effects, a2 has q; r as effects,
 a3has p; q as effects, and a4 has p; q; r as preconditions. Using Reachable
 003
 -2 we deduce that
 a1; a2; a3 are possible at time 0. We get as their possible effects p; q;
r; :p; :q; :r {recall4. The fact that the deduction is impossible has been
verified. What we are hypothesizing here is the reason for it.
 10Reachability, Relevance, and Resolution
 that we must include all noop actions in Reachable-k in order to capture
frame effects}. No
 strict subset of p; q; r can appear in the set of constraints C S
 003
 1
 . Since we deal with binary constraints only, the set fp; q; rg does not
appear in C S
 003
 1
 . Therefore, we will consider a4
 possible at time 1, although, in fact, it is impossible. Using binary resolution,
we would
 haveobtained the constraint :p _ :q _ :r {referringto time 1} which would
have enabled
 us to deduce that a 4
 is impossible at time 1.3.2.2 The Graphplan Encoding
 The Graphplan encoding differs from the linear encoding by its ability to
consider multiple
 concurrent {non-interfering} actions, allowingone to obtain shorter plans
which, in turn,
 can reduce the search space size. It constructs the following sets of clauses:
1. An action implies its preconditions; 2. An effect impliesone 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 impor-
 tant difference between the Graphplan and Linear encoding is in axiom class
2 {referred
 to in {Ernst et al., 1997} as explanatory frame axioms.} Clauses in this
class will contain positive occurrences of action literals and negative occurrences
of state literals. As in the linear case, using unit propagation we can infer
which actions cannot be
 applied at the initialstate. Using axioms of class 2, we can propagate this
information for-
 ward, deducing the negation of all effects that cannot be produced by the
initiallyallowable
 actions. This information enables us to exclude actions whose preconditions
cannot be pro-
 duced. This forward propagation is essentially identical to Reachable-1.
We can informally
 conclude:
 Lemma 3 In the context of the Graphplan enco ding, unit prop agation and
Re achable-1
 yield the same re achability information, if we ignore the explicit constr
aints appe aring in
 axiom class 4. If we use these constr aints, unit prop agation can yield
more re achability
 information. T o be precise we have to carefully define the notion of reachability
constraints in the context
 of the Graphplan encoding. For example, in the Graphplan encoding we can
derive a
 constraint that says that one of a group of actions must appear in the plan.
This constraint
 will not necessarily rule out any action because the Graphplan encoding
permits multiple actions at the same time point. 5
 However, in the linear encoding such a constraint will immediately rule
out all other actions because only a single action is allowed at each time
 point. As we mentioned earlier, in this paper we concentrate on strict exclusion
constraints5. However, because actions that interfere with each other cannot
occur concurrently, if we know that action a will occur then we can deduce
that any action a
 0
 that interferes with a will not occur. This is precisely
 where class 4 axioms enter the picture.
 11Brafman
 which lead to an immediate reduction in the search space by ruling out the
need for certain actions at certain time points. When k >1, the mechanism
remains the same. But now, axioms of class 4 can play
 a more prominent role because we can use them to exclude actions in more
cases than before. However, thesame problem of propagating mutual exclusion
constraints forward which we had with the linear encoding reappear here.
Consequently, k-clause resolution in
 the context of the Graphplan encoding and Reachable-k are incomparable.
 4. Relevance and Resolution
 Relevance analysis is a complex task and it can be performed to various
degrees. For
 instance, considering the last action level, one can exclude actions that
do not produce a
 literal in the goal. However, some actions producing a goal literal can
also be irrelevant.
 F or example, consider a blocks' world planning problem in which the color
of the blocks
 is specified as part of the goal. As observed by Nebel, Dimopoulos, and
Koehler {1997}, a
 paint-blo ck action is still, intuitively, irrelevant if the initial and
final colors of the blocks
 are the same. However, it does have a goal literal as an effect.
 In this section, we formulate an algorithm for relevance analysis, called
Relevant-k.
 Relev ant-k doesnot perform the deeper relevance analysis needed to determine
that the
 paint-blo ck action is irrelevant in the above example. Rather, Relevant-k
issimilar in its
 motivation and form to Reachable-k, and it has a similar soundness property.
Relevant-k
 prunes the search space by excluding states from which the goal is not reachable
within a given number of steps and actions that are not useful for achieving
the goal state within a
 given number of steps. Relevant-1 is similar to a number of existing components
of existing planners, such
 as McDermott's gre e dy re gr ession graph {McDermoot, 1996} and Nebel,
Dimopoulos, and Koehler's And-Or trees {Nebel et al., 1997}. Relevant-k generalizes
these ideas to arbitrary
 levels of interactions, taking into consideration mutual-exclusion constraints
that relevant states must satisfy. Relevant-k is slightly more complicated
then Reachable-k because the Strips formalism allows incomplete description
of goal states, and propagating this par- tial information raises some difficulties.
Naturally, if the goal state is partially specified,
 fewer constraints are available to start with, and so fewer constraints
will be derived. The
 algorithm is described in Figure 2. We are not aware of a similar, general
formulation of
 these ideas. Therefore, itis worthwhile going over the central points of
this algorithm,
 concentrating on the more interesting and complex case in which parallel
actions are al-
 lowed. However, before we do this, we point out an important assumption
we shall make
 on the action representation used: No propositionsymbol shall appear only
in the precon-
 ditions or only in the effects of an action. This restriction is not difficult
to enforce, as any
 Strips-based domain representation can be transformed into a description
in which this assumptions is satisfied. For example, if p is a precondition
of action a that does not appear
 in the effect of a, we can simply add it to the effect, as we know that
it must hold after
 the action is executed. If p appears in the effect of a but neither p nor
:p appear in the
 preconditions of a, we can decompose a into two versions of the a action,
one in which p is
 a precondition and one in which :p is a precondition. Note that in the worst
case, such a transformation can cause an exponential blow-up in the number
of actions. 12Reachability, Relevance, and Resolution
*  A
 r
 0 contains all actions that are useful and safe w.r.t. the goal.
 
*  A 0
 contains A
 r
 0
 and all noops that are safe w.r.t. the goal.
 
*  C A
 0
 contains all pairs of interfering actions in A
 0 .
 We define R i
 ; S
 i
 ; A
 r
 i
 ; A i
 inductively as follows: 
*  R
 i
 is the union of preconditions of actions in A
 r
 i0001 .
 
*  S
 i is the union of preconditions of actions in A
 i0001
 .
 
*  C S
 i contains sets S of literals such that S 032 S i
 , jS j 024 k and for any set of actions A 032 A
 i0001 whose preconditions contain S itis the case that A2 C A
 i0001
 . 
*  A
 r
 i contains all actions that are useful w.r.t. R
 i
 but no subset of their effects is contained in
 C S
 i
 .
 
*  A
 i
 contains A
 r
 i
 and all noops useful w.r.t. S
 i
 .
 
*  C A
 i contains all action sets A such that A 032 A
 i
 and either {1} A contains two interfering
 actions, or {2} Some subset of the set of effects of A is in C S
 i
 .
 Action descriptions must contain the same set of propositional symbols in
their precondition and
 effectlists.Figure 2: The Relevant-k Algorithm
 For k = 1 the algorithm is quite simple {and identical in the parallel and
linear cases}. In
 that case, we can ignore the sets S
 i
 ; C S i
 ; A
 i and C A
 i
 {as they are degenerate} and consider the sets R
 i
 and A
 r
 i
 only. Starting with the goal literals, at each stage we have a set of literals
from which we construct the next set of actions. This action set contains
actions
 with an effect in the current literal set. However, ifall the goal effects
of an action are all
 part of its preconditions, we can ignore that action as irrelevant. Next,
a new literal set is constructed, containing the set of preconditions of
the current set of actions, and we repeat
 the process with this new set. When k >1, the picture becomes a bit more
complicated. We start with the set
 of relevant actions, A
 r
 i
 . These are actions that achieve one of the desired literals. In
 particular, A
 r
 0
 contains only actions that have one of the goal literals as an effect {but
not
 as a precondition}. If the goal is partially specified, literals that are
not part of it could hold
 in the previous time step. Hence, we includethe appropriate noop actions
in a larger set,
 A
 i , which contains both A r
 i
 and noops that do not destroy needed propositions. A subset
 of the actions in A i
 is mutually exclusive if it contains interfering actions or actions whose
effects are mutually exclusive. Given the set A
 r i0001
 , we generate the set R
 i
 , which includes the preconditions of A
 r i0001
 . The set S
 i
 is defined as the set of preconditions of actions in A i
 .
 If the goal is a completely specified state, there is no the sets R
 i
 and S i
 and the sets A r
 i
 and A i
 are identical, and so we need not distinguish between them. 13Brafman
 To facilitate the description of the Relevant-k algorithm,it would be useful
to add a
 few simple definitions. First, we wish to revise the definitionof interfering
actions in the
 context of the Relevant-k algorithm. We say that actions a; a
 0
 interfere with each other if
 some effect of a conflicts with some precondition or effect of a
 0
 or {and this is beyond the
 previous definition of this term} if their preconditions are inconsistent.
An action a is useful
 w.r.t. {with respect to} some literal l if a is the noop action preserving
l or l is an effect,
 but not a precondition, of a. a is useful w.r.t. some set of literals if
it is useful w.r.t. one of the set's elements. A set A of actions is safe
w.r.t. some set of S of literals if no action in A has an effect that negates
an element of S .
 Relevant-k embodies the intuitions described above. Note that an increased
index cor-
 respondsto points earlier in time. The definition of the sets S i
 ; R
 i ; A
 i
 ; A r
 i
 is quite intuitive:
 S
 i
 contains the preconditions of the actions in the previous A
 i
 , and R i
 contains the precon- ditions of actions in A
 r
 i
 . A
 r
 i
 contains actions that have a useful, but not mutually exclusive, effects.
A
 i
 is defined much like A r
 i
 , butw.r.t. S
 i
 rather than R
 i
 . The set C S
 i
 contains literals that are mutually exclusive at a particular point. A set
L of literals is mutually
 exclusive if any set of relevant actions that have L among their preconditions
are mutually exclusive. The set C A i
 contains mutually exclusive sets of actions. A set of actions A is
 mutually exclusive if it contains interfering actions or if the set of its
effects is mutually
 exclusive. Example: In order to illustrate the Relevant-k algorithm,we shall
once again use the counter
 example used in Section 3.1, starting with a three bit counter and using
the propositions,
 p
 1 ; p
 2
 ; p 3
 . Each of the actions a
 1
 ; a
 2
 ; a
 3
 can change the value of a single bit from 0 to 1,
 provided the values of the lower bits are 1. We start with the final state
f:p
 1
 ; :p
 2
 ; p
 3
 g and k = 1. Since the final state is fully specified, there is no distinction
between the sets S
 i
 and R
 i
 and between A
 r
 i
 and A
 i
 . A 0
 contains the action a
 3
 and the three relevant noops. S
 1 contains fp
 1 ; :p
 1
 ; p
 2
 ; :p
 2
 ; p
 3
 ; :p
 3 g,
 A
 1 now contains a
 1 ; a
 2
 ; a 3
 , and the appropriate noops, and the remaining sets look the same.
 If k = 2, A 0
 and S
 1 are as in the k = 1 case. However, C S
 1 contains {:p
 1
 ; p
 2 } and
 {p
 1
 ; :p
 2 }, which implies that a 2
 cannot be applied. Hence, A
 1
 contains a
 1
 and a 3
 , but not
 a 2
 , unlike the case of k =1. The action a
 2
 would be introduced only in the next step.
 Next, consider a partially specified goal, such as fp
 3
 ; p
 2
 g and with k = 2. A
 r
 0
 =
 fa
 2
 ; noop[p 2
 ]; noop[p
 3
 ]g because a
 2
 has p 2
 as an effect, anda
 2
 does not destroy p
 3
 ; whereas a
 1
 , for example, does not have an effect in the goal. A
 0
 would now contain A
 r
 0
 as well as
 the noops for p
 1
 and :p 1
 . R
 1 = fp
 1
 ; p
 2
 ; :p
 2
 ; p
 3
 g and S
 1
 = fp
 1 ; :p
 1
 ; p
 2
 ; :p
 2
 ; p
 3
 g. Next, A r
 1
 contains fa
 1
 ; a 2
 g, etc.
 Finally, suppose we have four bits, and the goal state is f:p
 1
 ; :p
 2
 ; p
 3
 ; p
 4
 g {i.e., the counter's bit value is 1100}. If k = 2, A
 0 contains a
 3
 and S
 1
 = fp
 1
 ; :p 1
 ; p
 2 ; :p
 2
 ; p
 3
 ; :p
 3
 ; p
 4
 g.
 However, C S
 1
 contains pairs such as {:p
 1
 ; :p
 3 }; {:p
 2
 ; :p
 3 } and others. A
 1
 contains a
 1
 ; a
 3
 and some noops. S
 2 = S
 1
 , butnow, C S
 2
 does not contain {:p
 1 ; :p
 3
 }, it does contain
 {:p
 2
 ; :p
 3
 }, though, and that precludes action a
 4
 from being in A
 2 . In the next step, we have S
 3
 = S
 2
 = S
 1
 , and C S
 3
 no longer contains {:p
 2
 ; :p
 3
 }. This implies that we can
 add a 4
 to A
 3 because its effects are no longer mutually exclusive. So overall, we have
 A
 0
 = fa
 3
 g; A
 1
 = fa 1
 ; a
 3 g; A
 2
 = fa
 1
 ; a 2
 ; a
 3 g, and A
 3 =fa
 1
 ; a
 2
 ; a 3
 ; a
 4 g. However, ifk =3, at
 14Reachability, Relevance, and Resolution
 C S 3
 we would still have a mutual exclusion constraint on {:p
 1
 ; :p 2
 ; :p
 3 }, which would not
 allow us to add a
 4
 . Hence, when k =3, A
 3 = fa
 1
 ; a
 2
 ; a 3
 g.We can prove the following soundness results:
 Theorem 2 Let s be some state from which the goal is re achable using an
m-step plan
 {where each step can contain a number of non-interfering actions}. Then
{1} the set of
 literals satisfied in s is a subset of S
 m
 , no subset of which is in C S
 m
 , and {2} there exists
 an m-step plan for re aching the goal from s such that if A is the set of
actions in the plan
 v steps befor e last then A 032 A
 v
 and no subset of A is in C A
 v
 .
 A corollary of this theorem is: Corollary 1 For any initial state s from
which the goal is re achable and any minimal {in the number of oper ators}
plan P = A
 0 m
 ; : : : A 0
 0
 {where the steps are number e d backwar ds} for
 re aching the goal from s, we have A
 0
 i
 032 A
 i
 and C A
 i
 does not contain any subset of A
 0 i
 .
 The complexity of Relevant-k is O{jAj
 k
 jLj + jLj
 k
 m
 k
 p jAj}, wherejAj is the number of actions,jLj is the number of proposition
in the language, and m p
 is the maximal number of preconditions of an action. For more details, see
Appendix B. 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
 propagation 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 irrelevant effects willnot be pruned.
 6
 On the other hand, Relevant-1 prunesboth
 actions that destroy some goal literal and actions that are simply irrelevant.
There is a slightly degenerate case in which all actions but one destroy
some goal proposition. In that
 case, usingunit propagation we will be able to deduce the previous state.
Consequently, we
 have: Lemma 4 In the context of the linear enco ding, unless there is a
single safe, final action,
 unit prop agation yields less relevanc e information than Relevant-1. In
the context of the Graphplan encoding the situation is often worse, and unit
prop-
 agation prunes even less than in the linear encoding. The goal propositions
appear only in
 class 2 {effect} axioms. Propagating them against these axioms, we obtain
disjunctions of
 positive action propositions explaining a particular goal proposition. If
we assume that all
 literals have more than one explanation, we see that no new unit clauses
emerge. Conse-
 quently, we can prune nothing.
 Example: Consider the blocks' world domain once again. Suppose that there
are three blocks A,B, and C, and that the goal is on{A,B}. Clearly, any action
that moves block C
 or moves another block on top of block C is irrelevant as a last action.
When we consider
 the Graphplan encoding, the only unit clause we have is on{A,B,t} {where
t is the last
 time point}. We can resolve it against the effect axiom that lists the the
possible causes for on{A,B,t}. Aside from the noop action, there are actions
such as moving A from C to B6. In general, proving that an action should
be ruled out means that we have shown that in all models, i.e.,
 all plans, this action does not appear. We cannot expect to be able to do
this for an irrelevant action since it could possibly be inserted into the
plan without affecting it.
 15Brafman
 and moving A from the Table to B. This yields a new ternary clause and no
additional unit clauses. There are no other axioms in which on{A,B,t} appears
negated. Notice that we have no means of excluding actions that destroy one
of the goal literals. For example, if our goal was clear{A,t}, we would not
want the action move{B,C,A,t-1} as
 alast action. However, asabove, all that we can deduce from clear{A,t} is:
move{B,A,C,t- 1}_move{B,A,Table,t-1}_ move{C,A,B,t-1}_move{C,A,Table,t-1}_
noop[clear{A; t0001}].
 If we could use binary resolution at this stage, we could deduce the negation
of any action
 with the effect :clear{A,t}, because any such action would be mutually exclusive
from any of the above five actions.If a goal literal l has a single explanation
it must be a noop action {which implies that
 there is no \real" operator that has it as an effect}. In that case, we
would be able to deduce
 that this noop action must hold, and using the precondition axioms, we would
deduce that
 l must hold at the previous step. Using the mutex axioms {class 4} we could
deduce the
 negation of any action that destroys l. However, we cannot deduce the negation
of any
 action that does not interact with l, whetherit is simply irrelevant or
it destroys some
 other goal literal.
 Example: Consider a domain such as the Rocket domain, where a rocket can
have fuel, butthere is no action for fueling a rocket. Suppose that the rocket
has fuel in the goal
 state. Hence, fuel{t} holds. Since the explanation axiom for fuel is a binary
clause {i.e.,
 :fuel{t} _ noop[fuel{t 000 1}]. Resolving this axiom with the fact fuel{t},
we derive a new
 unit clause noop[fuel{t 000 1}]. Using the precondition axioms, we can
derive fuel{t-1}.
 Using the mutex axiom, we can derive an action such as fly{t-1}, one of
whose effects is :fuel{t 000 1}. Notice, though, that we cannot deduce the
negation of an action that does
 not interact with the proposition fuel, whether or not it is irrelevant.
For example, if fuel is the only proposition in the goal, then an action
such as loading the rocket, whichdoes
 not affect the value of the proposition fuel need not be considered for
the final action of the plan. However, as before, there is no way of deducing
:load{t 000 1}.
 Because no action can produce fuel the same reasoning would apply to any
step, and
 we will be able to deduce the fact that fuel holds at each time point during
the plan.
 Using this fact, we will be able to prune out all actions that have :fuel
as a precondition.
 Relevant-1 will not be able to do so: If a has :fuel as a precondition but
a has an effect
 that is relevant at some point, a will be considered a relevant action.
7
 Lemma 5 In the context of the Graphplan enco ding, ifthere is an action
for chang- ing the value of every literal, then unit prop agation yields
less relevanc e information than
 Relevant-1.
 Some actual values appears in Section 5. 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 possible7. Of course, in this particular domain we do not have an action
whose precondition is :fuel, but the
 observation is still valid. For example, we may have a maintenance action
which can be performed only
 when the rocket is without fuel.
 16Reachability, Relevance, and Resolution
 actions, none of which are a unit clause. Since we have no way of deducing
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
 relevance analysis. Again, Relevant-k is likely to do a much better job
here, because it
 takes explicit relevance issues into account. However, as in the case of
reachability analysis, because of the ability of k-clause resolution to yield
constraints of order greater than k, we
 cannot show that Relevant-k is always better.
 In the context of the Graphplan encoding, we will generate disjunctionsof
relevant
 actions, from which disjunctions of relevant preconditions can be deduced,
etc. However,
 irrelevant actions will not be excluded explicitly {since more than one
action is allowed at
 each step} and we will only conclude that some relevant action must appear.
Nor can we excludeactions that destroy a goal proposition. Again, because
we can deduce constraints
 of order greater than k viak-clause resolution, we cannot provide a general
result here.
 Finally, we note that {1} the Graphplan planner does not incorporate relevance
anal-
 ysis, but Mea-Graphplan, a more recent variant, does {Kambhampati et al.,
1997}, as well as IPP {Nebel et al., 1997}. {2} Ernst, Millstein, and Weld
{1997} discuss an enhanced
 version of the Graphplan encoding which contains effects axioms as well
{i.e., axioms of the form action ! effect}. In terms of the ability to propagate
reachability and relevance
 information, we see an added ability to rule out actions that destroy needed
propositions
 {as in the linear encoding.}
 5. Empirical Evaluation
 In the previous sections we attempted to understand the mechanisms by which
resolution yields reachability and relevance information and to compare them
to a natural class of
 direct reachability and relevance algorithms. As we noted, the relationship
is not always
 that of subsumption, and it is of interest to examine the actual pruning
abilities of these
 algorithms. In this section we describe the performance of these algorithms
on a number of standard planning problems. Because of the limited number
of domains used, caution
 should be exercised in interpreting these results. However, some interesting
results emerge.
 Ourfirst set of experiments examined the performance of unary methods on
large blocks world and logistics domain problems. We used the blocks' world
problems bw-dir.a/b/c/d
 from the Satplan distribution
 8
 involving 9/11/15/19 blocks, respectively, and {minimal}
 plans of length 6/9/14/18. The logistics' domain problems are based on instances
described
 in {Brafman & Hoos, 1999} involving 8 packages and 3 cities, with minimal
plans of size 6/10/16, respectively. SAT-encodings were generated using the
Medic program {Ernst
 et al., 1997}. We used the crse options to obtain a linear encoding and
the erpe options
 to obtain a Graphplan-like encodings. However, the encoding obtained via
the erpe op-
 tionscontain explicit effect axioms, as in the linear encoding. These axiom
improve the
 Graphplan-encoding's ability to propagate relevance information.8. These
instances are part of the UCPOP distribution, maintained by the University
of Washington, or
 from http://www.research.att.com/ kautz/blackbox/index.html, the BlackBox
home page.
 17BrafmanjAjReachRelR+RU-rch{l}U-rel{l}log.a45652922617347640138log.b59413517680390544220log.c802150512782621460032bw.a388816974082105639300bw.b10890356583043951201440bw.c44100128182394152123141840bw.d1169642696352383220164825114Table
1: Pruning Effects of Unary Methods. jAj is the number of possible actions
in
 the course of a minimal length plan. The following entries hold the number
of
 actions pruned using: Reachable-1, Relevant-1, both combined, unit propagation
 on linear encoding using initial state, and using the final state. Unit
propagation in the Graphplan encoding using the final state yielded no pruning.
Execution times for the Reach/Relevant algorithms are 0240:01 seconds except
for bw.c {0.03
 sec.}, and bw.d {0.07 sec.}.
 In this set of experiments we measured the number of potential actions eliminated
by
 the following algorithms: Reachable-1, Relevant-1, Reachable-1 and Relevant-1
combined,
 reachability analysis via unit-resolution using the initial state, andrelevance
analysis via
 unit-resolution using the goal state. We did not consider the Graphplan
encoding for the
 following reasons: {1} Unit-propagation in the Graphplan encoding yields
as much information as Reachable-
 1. {2} For our particular experiments {and in most other cases}, unit-resolution
based on
 the final state in the Graphplan encoding prunes little, if any, actions
because for each fact appearing in the goal state there are a number of potential
producing actions. {3}
 The version of the Graphplan-encoding produced by Medic is basically equivalent
to the
 linear-encoding in terms of relevance information because it contains explicit
effect axioms.
 The actual numbers appear in Table 1. The first column provides the size
of the set of
 actions for the minimal plan length. The following columns provide the number
of actions pruned by the various methods tested. It is evident that Reachable-1
is extremely effective.
 Relevance analysis seems much less useful, although Relevant-1 does prune
a non-negligible number of actions. The results for unit-resolution are quite
disappointing, although in line
 with our theoretical analysis. Recalling that unit-resolution in the Graphplan
encoding
 is equivalent to Reachable-1, we see that there is a much greater potential
for pruning in the Graphplan encoding. Another interesting observation is
that there is little overlap
 between the reachability and relevance analysis. This stems from the fact
that the pruning
 effect of these algorithms is often quite shallow: most of the pruningis
done on the very
 first steps {in reachability} or very last steps {in relevance}. Finally,
we note that the k =1 algorithms are quite fast: Unit propagation is an important
heuristic in all SAT
 solution algorithms based on the David-Putnam algorithm {Davis & Putman,
1960}, and
 it is extremely fast, with negligible running times {i.e., < 0:01 seconds}.
Not surprisingly,
 18Reachability, Relevance, and ResolutionjAjRch1Rch2Rel1/2rch1{l}rch2{l}rch1{gp}rch2{gp}rel1/2{l/g}bw-sm.a1821228152221224bw-sm.b48687044447468706bw-sm.c1001992041849621019920412log-sm.a1839578144939441log-sm.b4211116518361411111263log-sm.c6619629226582441962205hanoi-33894972136117941189hanoi-468224230346628122428014hanoi-51104504605010855845055120Table
2: Effects of Unary and Binary Methods. jAj is the number of possible ac-
tions per step . The following columns hold the number of actions pruned
during
 the course of a minimal-length {or longer} plan using Reachable-1, Reachable-2,
 Relevant-1 and 2 {which yield the same value}, unitpropagation on the linear
 encoding using initial state, binarypropagation on the linear encoding using
ini-
 tial state, unit propagation on the Graphplan encoding using initial state,
and
 binary propagation on the Graphplan encoding using initial state. The final
 column correspond to propagation using the goal state. All methods {i.e.,
unit
 and binary} on both encodings yielded the same values. Reachable-1 and Relevant-1
are also extremely fast. Execution times for these algorithms
 were less than 024 0:01 seconds, except for bw.c {0.03 sec.}, and bw.d
{0.07 sec.}, for which
 these amount to a small fraction of the runningtimes required by modern
SAT algorithms.
 9
 The next set of experiments, shown in Table 2, introducesbinary pruning
methods as well. Here, we were limited by the slow performance of our prolog
implementation of
 Reachable-2and the Medic encoder {Ernst et al., 1997}. We looked at blocks
world prob- lems involving 3,4, and 5 blocks, respectively, and we looked
at logistics domain problems
 involving one package and two cities, three packages and two cities, and
three packages and
 three cities. In addition, we looked at three hanoi-tower problems with
3,4, and 5 disks.
 There are a number of points worth mentioning: 
*  In two domains{blocks' world and hanoi}, Reachable-2 is only slightly
more useful
 than Reachable-1. In the logistics domain, on the other hand, Reachable-2
is much
 more effective. However, we must remember that Reachable-2 yields mutual
exclusion constraints which we did not measure. These constraints can be
quite useful and they
 have an important role in the Graphplan planner.
 
*  No clear winner emerges. In the blocks-world domain, binary resolution
in the linear encoding prunes more than Reachable-2, whereas in the logistics
domain, Reachable-
 2 prunes more. Interestingly, binaryresolution in the Graphplan-encoding
is less9. These experiments were conducted on a PC with a PentiumII-200 processor.
 19BrafmanTime12345678910111213141516Reach-112345678910111213141516Reach-21223334444555556U-Res{lin}1161616161616161616161616161616B-Res{lin}1223344556677889U/B-Res{gp}12345678910111213141516Table
3: Reachability Analysis in a 16-bit Counter. Shown are the number of un-
 pruned actions per time step. Rows correspond to Reachable-1, Reachable-2,
unit
 resolution on the linear encoding, binary resolution on the linear encoding.
The
 last row corresponds to unit and binary resolution on the Graphplan encoding,
which had identical effect. effective than in the linear encoding. However,
the Graphplan-encoding allows for
 shorter plans, and consequently, smaller search spaces. Therefore, the Graphplan-
 encoding is still likely to be more efficient.
 
*  Relevant-2 has no advantage over relevant-1. In fact, thisbehavior was
observed when
 using resolution as well: unit and binary resolution on both the linear
and Graphplan
 encodings pruned the same amount of actions. Consequently, we present them
in one
 column. Indeed, we see from both sets of experiments reported in Tables
1 and 2, that relevance analysis contributes little. One obvious reason is
that the goal state is
 often incomplete and much less constrained than the initial state {at least
explicitly}.
 Therefore, the algorithms have difficulty deriving relevance constraints.
However,
 one's intuition seems to indicate that this should not be the case, atleast
not to
 the extent observed. There should be means of providing better relevance
analysis,
 although they may require more sophisticated derivation of state constraints.
 
*  As predicted, relevance analysis is much more useful at the state-space
level than at
 the truth-assignment level.
 
*  As expected, the Graphplan encoding is typically better than the linear
encoding.
 Finally, we ran some tests on a 16 bit version of the counter domains described
in
 the text. This is a very constrained domain in which only a single action
is applicable at each state and we wanted to see how much of this would be
discovered by the algo-
 rithms. The results are shown in Tables 3 and 4, where the number of permisable
actions is given as a function of the the time step. Table 3 presents the
results for forward pruning
 using Reachable-1, Reachable-2, andunit and binary propagation using the
Graphplan
 and linear encodings. Table 4 presents the results for backward pruning
using Relevant-1,
 Relev ant-2, and unit and binary propagation using the linear encodings.
 20Reachability, Relevance, and ResolutionTime12345678910111213141516Rel1/2,U/B-Res{gp}12345678910111213141516U-Res{l}1161616161616161616161616161616B-Res{l}1223344556677889Table
4: Relevance Analysis in a 16-bit Counter. Shown are the number of unpruned
actions per time step. The {identical} results for Reachable-1, Reachable-2,
unit-
 resolution on the Graphplan encoding, and binary-resolution on the Graphplan
 encoding appear in the first row. The next rows correspond to unit and binary
 resolution on the linear encoding, respectively.
 6. Conclusion
 We have shown a connection between the scheme used to encode planning instances
and the
 ability to propagate reachability and relevance information from the initial
and final steps
 to other time points. We hope that these results will serve to improve our
understanding of
 the factors contributing to the performance of different encoding methods.
In addition, we
 provided a crisp and general formulation of a class of reachability and
relevance algorithms
 that appear in various forms in different planning algorithms. We compared
the pruning ability of resolution-based propagation methods which operate
on encoded plans, to that of
 the Reachable-k and Relevant-k algorithms which operate at the plan level.
Our empirical results show a complex picture, where no clear winner emerges.
However, it seems that
 when the domain is constrained {making parallel actions less useful} binary
methods have
 littleadvantage over unary methods. In addition, they show that relevance
analysis is best
 conducted at the plan level. For SAT-based planning algorithms, this would
suggest the use of a simple plan-level relevance analysis stage prior to
the plan encoding. This observation
 is confirmed by recent results reported by Do, Srivastav a, and Kambhampati
{2000}. In {Brafman, 1999}, we pointed out that binary clauses form a large
fraction of the clauses in SAT-encoded planning problems. Given our results
regarding the utility of binary
 resolution, a natural idea is to augment standard clause simplification
techniques {e.g., unit
 propagation} with some limited form of binary clause preprocessing. Initial
results presented there indicated the utility of this idea: In instances
where unit clauses could be derived from
 this form of binary resolution, nice reductions in running time were demonstrated.
When
 unit clauses were not derivable via this method, only a small overhead was
incurred. A
 more principled,systematic, and efficient technique based on these ideas
is investigated in {Brafman, 2000}.
 This work is among the first attempts to theoretically analyze different
encoding schemes.
 We have concentrated on one particular aspect of such encodings, i.e., theirability
to propa-
 gate concrete state informationbackwards and forwards. Naturally, this attempt
is a-priori
 limited in its scope, as this ability is only one factor influencingthe
performance of various algorithms, and its influence is probably more significant
in systematic methods based on the David-Putnam procedure than in methods
based on stochastic local search. 21Brafman
 Other authors have consideredsome of the ideas presented here, too. Kautz
and Selman {1999} discuss the relation between Graphplan's mutex constraint
and a restricted form
 of binary propagation. In particular they show that mutex computation is
a limitedform
 of negative binary propagation. In mutex propagation, two assertions of
mutual exclusion
 yield a new one. Of course, each mutual exclusion statement is equivalent
to a binary
 clause {e.g., eitheraction a is not performed or action b is not performed},
hence we can
 view this process as a limited form of binary propagation: From f:p _ :qg
and fp _ :rg
 deduce f:q _ :rg. Graphplan performs this operation, but in an incomplete
manner. In
 addition, they tested additional limited inference methods such as the failed
literal strategy
 {attempting to prove that a particular literal is inconsistent using unit
propagation} and the binary failed literal strategy {attempting to prove
that a binary clause is inconsistent using unit propagation}. These methods
do not directly correspond to the methods considered in this paper. More
closely related is one of the options in the Medic system for encoding
 planning problems: a simple inference method which is referred to as simple
data-flow
 analysis {Ernst et al., 1997}. This method is basically an instance of Reachable-1.
 Haslum and Geffner {2000} present a parametrized class of admissible heuristics
func-
 tions H
 k
 . There is an interesting and important relation between the heuristic function
 generation technique discussed in that paper and the parameterized class
of reachability
 analysis algorithms discussed in this paper. When a heuristic function assigns
1 to some
 state s this means it believes that goal is not reachable from s. If the
heuristic function is admissible, then in fact, this is true. Thus, admissible
heuristic functions provide a sound
 tool for pruning { the goal is not reachable from any state to which they
assign the value
 1. In fact, the derivation of the heuristic functions of class H
 k
 is closely related to our
 computation of Reachable-k. In both cases, instead of analyzing actual states,
we analyze
 subsetsof states of size k and their interactions. However, in designing
heuristic functions, a greater emphasis is put on the distance from the current
state to a state in which some
 set of literals appears without mutual exclusion constraints {i.e., the
indices of the sets S
 i
 and C S
 i
 }.
 Finally, a recent paper by Do, Srivastav a, and Khambhampati {2000} examinesencoded
 planning problems generated by the Blackbox planner. Blackbox utilizes mutual
ex-
 clusion constraints derived from Graphplan's planning graph. The authors
show that
 these constraints are useful, despite the fact that they increase the size
of the encoding.
 In addition, the authors examine the utility of adding explicit mutual-exclusion
constraints
 stemming from {state-space based} relevance analysis. These constraints
appear to improve the planner's performance. In fact, it seems that the constraints
described by Do, Srivas-
 tav a, and Kambhampati {2000} are more powerful than those generated by
Relevant-2. We believe that Relevant-k canand should be strengthened, and
we hope to examine this issue
 more closely in the future.
 Acknowledgments
 I wish to thank Craig Boutilier and Chris Geib for valuable discussions
on reachability anal-
 ysis and the anonymous reviewers for very useful and detailed comments.
I am particularly
 grateful to Olga Rozenfeld who implemented the algorithms in Prolog, suggested
the use of
 22Reachability, Relevance, and Resolution
 the counter example for illustrating the algorithms, and provided important
corrections to previous drafts. This work was supported in part by the Paul
Ivanier Center for Robotics
 Research and Production Management.
 Appendix A. Proofs
 Theorem 1 If a set of prop ositions or actions is excluded by Re achable-k
at time j then
 there is no feasible plan in which, at time j , these prop ositions hold,or,
resp e ctively, these
 actions appe ar.
 Proof : This is immediate: Consider any valid plan and the states of the
world during the execution of this plan. It is straightforward to show that
both appear within the sets A
 i
 and S
 i
 without being constrained by virtue of this being a valid plan.Lemma 1 In
the context of the linear enco ding, Re achable 003
 -1 yields more re achability in-
 formation than unit prop agation.
 Proof : Given the definitions used earlier on, a more formal statement of
this lemma is as follows: Let k be some integer denoting the length of a
plan. Let A
 reach0001 be the set of
 actions pruned by Reachable
 003 -1 up to the k-th level given some planning domain and initial
 state. Let A
 u000res be the set of actions that are pruned by unit-resolution on the
linear
 encoding of this planning domain using k steps {i.e., actions for which
we can deduce a unit clause containing the negation of their corresponding
variable}, but without a goal state
 supplied. Then A
 reach0001
  A
 u000res
 , and for some planning instances A
 reach0001
 033 A
 u000res .
 First let us consider unit resolution. The unit clauses that are available
initially corre-
 spond to the propositions that hold at the initialstate. The only axioms
in which proposi- tions denoting the state at time 0 appear are those of
class 1 {precondition axioms} and 3 {frame axioms}. However, the clauses
in class 3 are ternary and contain at most one such
 proposition. These ternary frame clauses can yield a unit clause only if
we are able to rule out all actions but one, which we cannot, at this stage.
Therefore, unit clauses can only
 be derived by resolving the current unit clauses with class 1 clauses. Such
resolutions can
 yield new unit clauses containing negated actions. These negated actions
can be resolved
 against clauses containing positive action variables. Such variables appear
only in class 4
 {at-least-one-action} axioms. Now there are two cases to consider. First,
suppose that we have been able to rule out
 all actions but one. Using the frame and effect axioms, we can derive the
state at time 1.
 Our situation now is analogous to that in which we were at time 0 with knowledge
of the initial state. Since Reachable 003
 -1 puts us in the same position, our claim follows {using a simple inductive
argument}. Next, suppose that we cannot rule out all actions but one. In
 that case, we have no new unit clauses, and so unit propagation stops. Reachable
 003
 -1 will be
 able to rule out all actions ruled out by the unit propagation process.
Moreover, ifall the
 actions that are not ruled out have some common effect, that effect can
be deduced using
 Reachable- 003
 -1, and it can rule out actions that require its negation as a precondition.
This
 type of information is not obtained via unit propagation.23Brafman
 Lemma 3 In the context of the Graphplan enco ding, unit prop agation and
Re achable-1
 rule out the same sets of actions, if we ignore the explicit constr aints
appe aring in axiom
 class 4. If we use these constr aints, unit prop agation can yield more
re achability informa-
 tion.
 Proof : First, suppose we ignore the mutex axioms of class 4. Using unit
propagation, we
 deduce the negation of those actions whose preconditions are violated at
time 0. Negated action literals can be resolved against class 2 {effect explanation}
axioms. If we have been
 able to rule out all explanations of some time 1 proposition, we can deduce
its negation
 in this manner. The same mechanism will allow us to exclude this variable
when using
 Reachable-1. Similarly, negated action literals can be resolved against
class 3 {at-least-one- action} axioms, but this yields no more information.
Those time 1 variables we can deduce
 can be used to rule out time 1 actions.
 Notice the following. If we can deduce p at time 1, then one of the actions
that produce p
 must hold at time 0. This information is not explicit in the Reachable-1
algorithm {although
 it appear in the Graphplan's planning graph in the form of edges}. However,
it cannot
 beused to rule out other actions if we are restricted to unit resolution.
 Class 4 axioms can make a difference in the above case. Suppose we have
been able to conclude that a particular action a that produces p must occur
{i.e., by deducing p and
 ruling out all its causes except a}. In that case, allactions that are mutually
exclusive
 with a cannot occur. These actions may not affect p at all, and their negation
need not necessarily be derivable using Reachable-1.Theorem 2 Let s be some
state from which the goal is re achable using an m-step plan
 {where each step can contain a number of non-interfering actions}. Then
{1} the set of
 literals satisfied in s is a subset of S
 m
 , no subset of which is in C S
 m
 , and {2} there exists
 an m-step plan for re aching the goal from s such that if A is the set of
actions in the plan v steps befor e last then A 032 A
 v
 and no subset of A is in C A
 v
 .
 Proof : Recall that we assume that any proposition appearing in the effects
of an action appears in its preconditions as well. We can always enforce
this requirement by converting
 an action that does not satisfy it into an a set of actions that satisfy
it.
 Our proof proceeds by induction on the number of steps by which the goal
is reachable.
 Let S be some state from which the goal G is reachable by a single step.
Let A be the set
 of actions in such a one-step plan for reaching G from S . By definition,
A does not contain
 interfering actions. In addition, we know that if G is reachable from S
by performing A
 then the preconditions of A and G n Effects-Of {A} must hold in S .
 First, suppose to the contrary that for some literal l 2 S , we have that
l 62 S
 1
 . Notice that by definition of A
 0
 , we have that S
 1
 contains all literals that are consistent with
 G. Therefore, l must be inconsistent with G, i.e., :l 2 G. Since l 2 S ,
there must be
 some action a2 A with the precondition l and the effect :l {otherwise, l
wouldhold after performing A}. Such an action would be in A
 r
 0
 and its preconditions, l among them, would
 be in S
 1
 . We conclude that S 022 S
 1
 .
 Next, we want to show that there is a one-step plan for reaching G from
S all of whose actions are in A
 0 . From the discussion above we see that the plan A for reaching G from
 24Reachability, Relevance, and Resolution
 S containsan action from A
 r
 0 for changing the value of every proposition l that holds in
 S and that is inconsistent with G. Clearly, none of these actions can have
an effect that
 is inconsistent with G. Let A
 0 022 A denote the set of such actions. By applying A
 0
 at S
 we transform all literals inconsistent with G to their value in G and we
do not destroy the
 value of any literal consistent with G. Since A
 0 022 A, it constitutes a valid plan {i.e., its
 actions do not interfere with each other} that achieves G. By definition,
A
 0
 022A
 0
 .
 To conclude the proof of the base step, we must show that no subset of S
is in C S 1
 .
 Suppose, to the contrary that some subset S 0
 of S is in C S
 1
 . We have seen that for any such S
 0
 , there is some set of actions A
 0 032 A such that A 0
 032 A
 0 and each l 2 S
 0
 is either
 a precondition of some action in A
 0
 or l is consistent with G and is not destroyed by A 0
 .
 Denote by A
 00
 the set consisting of A
 0
 and any noop[] corresponding to those l 2 S 0
 that
 are not preconditions of an element in A
 0 . By definition of A 0
 , we have that A
 00
 2 A 0
 .
 However, if S
 0
 2 C S 1
 then A
 00
 2 C A
 0 which implies that A
 00
 contains interfering actions. We claim that this is impossible. First, all
the effects of A 00
 are either in G or consistent
 with G, by construction. In addition, all the preconditions of A
 00
 are in S 0
 and therefore in
 S . Because S is an actual state of the world, it cannot contain conflicting
literals. Hence,
 S 0
 62 C S
 1
 .
 Next, supposethat we have established our inductive hypothesis for all i
< m and let
 us prove that it holds for i = m. Hence, let S be some state for which there
exists an m-
 step plan A = A
 1
 ; : : : ; A
 m
 for attaining G. Let S
 +1
 denote the state obtained by applying
 A
 1
 to S . We know that there is an m 000 1 step plan for achieving G from
S
 +1 . By our
 inductive hypothesis, S
 +1
 satisfies the conditions of the Theorem. In particular, we know
 that S
 +1
 032 S
 m0001
 and no subset of S
 +1
 is in C S
 m0001
 . To complete our proof it would be sufficient to show that S +1
 is reachable by a one-step plan A
 0
 whose actions are in A
 m
 but
 not in C A
 m
 . The proof is similar to the base case.Corollary 1 For any initial state
s from which the goal is re achable and any minimal {in
 the number of oper ators} plan P = A
 0
 m ; : : : A
 0 0
 {where the steps are number e d backwar ds} for
 re aching the goal from s, we have A 0
 i
 032 A
 i
 and C A
 i
 does not contain any subset of A
 0 i
 .
 Proof : An inspection of the proof of the previous theorem shows that in
every step we
 have found some subset of the set of actions in each candidate plan that
satisfied the
 relevant conditions. In particular, consider a minimalplan, all its elements
must satisfy
 these conditions.Lemma 4 In the context of the linear enco ding, unless
there is a single safe, final action,
 unit prop agation yields less relevanc e information than Relevant-1. Initially
, our only unit clauses are goal literals. We can resolve then against the
effect
 axioms only. This would yield negation of various actions {i.e., unsafeactions}.
These negated action literals can be resolved only against the action disjunction
{axiom class 4}.
 However, ifthere is more than one safe final action, we will not obtain
a unit clause from
 this disjunction, and there is nothing farther that we can do. The same
information, and
 more, is easily obtainable from Relevant-1.25Brafman
 Lemma 5 In the context of the Graphplan enco ding, ifthere is an action
for chang-
 ing the value of every literal, then unit prop agation yields less relevanc
e information than
 Relevant-1. Proof : See text prior to this Lemma.Appendix B. The Complexity
of Reachable-k and Relevant-k
 The computational complexity of Reachable-k is O{njAjjLj
 k
 E k
 + njLjjAj
 k
 }, where n is the
 number of levels we generate, jAj is the number of possible actions, jLj
is the size of the propositional language used, and E is the maximal number
of actions that have a particular
 shared effect. As we explain below, the complexity is dominated by the time
required to
 producethe sets C S
 i
 and C A
 i
 .
 The set of possible effects, S
 i
 , is produced in O{jAj 001 m
 e
 } steps, where m
 e
 is the maximal number of effects.
 C S
 i
 requires examining all l-tuples of elements in S i
 , for l 024 k, and there are at most
 O{jLj
 k }such elements. For each such tuple we have to find the set of actions
that produce
 it. This can be done quickly, provided we maintained pointers to these actions.
The number
 of such sets of actions is O{E
 K
 } {since no more than k actionsare needed}. For each such
 set of actions we must check whether some subset of it is a member of C
A
 i0001 . Given an
 appropriate representation of C A
 i0001
 , this can be done in time O{jAj}. To accomplish this,
 we can use a binary tree whose leafs correspond to bit vectors. The depth
of this tree is jAj and its size is O{jC A
 i0001
 j}. Finally, we need to maintain C S
 i
 as a similar tree of bit- vectors. This can be done in O{jLj
 k } {or, if C S
 i is small, at a lower cost}. The overall cost
 of producing C S
 i
 is O{jLj
 k
 jE j
 k
 jAj}.
 To produce the set A
 i
 , we go over all actions and check whether their preconditions appear in
S
 i
 . This requires O{jAj 001 m
 p
 } steps {assuming a bit-vector representation of S
 i
 }, where m
 p
 is the maximal number of preconditions of an action. We also have to check
whether the preconditions appear in C S
 i
 . Since jA
 i
 j 024 jAj and we can check whether a subset of the set of preconditions
appears in C S
 i
 in time O{jLj}, thisrequires O{jAjjLj} steps.
 Finally, we need to produce the C A
 i
 . This requires generating all subsets of A
 i
 of size
 k or less, taking O{jAj
 k
 } steps. For each such subset we must check whether its precon-
 ditions contain an element of C S i
 . Again, provided an appropriate data-structure for C S i
 is maintained, this can be done in O{jLj} for each set of preconditions.
As in the case of C S
 k
 , we assumed C A
 i
 is maintained as a tree of bit-vectors, which can be generated in time O{jAj
 k }. The overall complexity of this step is O{jLjjAj
 k
 }.
 Note that for small values of k other data-structures are likely to provide
better perfor- mance.
 Next, we address Relevant-k. Our analysis is under the assumption that the
same
 set of variables appear in the preconditions and effects of each operator.
As we noted, transforming a set of operators that do not satisfy this property
into a set of operators that
 satisfy it may cause an exponential blow-up in the worst case. The complexity
of Relevant-k is O{jAj k
 jLj + jLj
 k
 m k
 p
 jAj}, wherejAj is the number of
 actions, jLj is the number of proposition in the language, and m
 p
 is the maximal number of
 26Reachability, Relevance, and Resolution
 preconditions of an action. The analysis is quite similar to the case of
Reachable-k, and we ignore the sets R
 i and A
 r
 i which are subsets of the larger S
 i
 and A
 i
 and whose generation
 contributes constant factors:
 The set of preconditions, S
 i
 , is produced in O{jAj 001 m
 p
 } steps. To compute C S
 i , we iterate over O{jLj
 k
 } sets of literals. For each such set we examine
 all sets of actions that have it as preconditions, and there are at most
O{m
 k
 p } such sets. For
 each such set of actions, we need to check that it is not in C A i0001
 . Each such check can be
 performed in O{jAj} steps. The overall complexity of this step is O{jLj
 k m
 k
 p
 jAj}.
 To produce the set A
 i , we go over all actions useful for S
 i
 , which require O{jLjE } {where
 asbefore, E is the maximal number of actions that have a particular effect}.
For each action, we check whether its effects are in C S
 i
 . Since we need to perform this check at most once
 for every action, the overall complexity of O{jLjE+ jLjjAj}.
 Finally, we need to produce the sets C A
 i
 . Interfering actions can be pre-computed with
 the cost amortized over all steps. In any case, theircomputation requires
no more than
 O{mjAj
 2
 } steps, where m is the maximal sum of preconditions and effects for an
action.
 Next, we have to examine the effects of all l-tuples of actions, where l
024 k, and see whether
 these effects have a subset in C S
 i . This takes O{jAj
 k
 jLj} steps.
 Again, for small values of k {and in particular, k =1; 2} a tighter analysis
is possible.
 References
 Bayardo, R.J., & Schrag, R. C. {1997}. Using CSP look-back techniques to
solve real-world
 SAT instances. In Pro c. AAAI-97, pp. 203{208. Blum, A., & Furst, M. L.
{1997}. Fast planning through planning graph analysis. Artificial
 Intel ligence, 90, 281{300.
 Bonet,B., Loerincs, G., & Geffner, H. {1997}. A robust and fast action selection
mechanism for planning. In Pro c. AAAI-97, pp. 714{719.
 Boutilier, C., Brafman, R. I., & Geib, C. {1998}. Structured reachability
analysis for markov
 decision processes. In Pro c. of 14th Conferenc e on Uncertainty in AI,
pp. 24{32.
 Boutilier, C., & Dearden, R. {1994}. Using abstractions for decision theoretic
planning with
 time constraints. In Pro c. of AAAI'94, pp. 1016{1022. Brafman, R. I. {1999}.
Reachability, relevance, resolution, and the planning as satisfiability
 approach. In IJCAI'99, pp. 976{981.
 Brafman, R. I., & Hoos, H. H. {1999}. To encode or not to encode - i: linear
planning. In
 IJCAI'99, pp. 988{993.
 Brafman, R. I. {2000}. A simplifierfor propositional formulas with many
binary clauses.
 Tech. rep. 00-04, Dept. of Computer Science, Ben-Gurion University.
 Crawford, J., & Auton, L. D. {1993}. Experimental results on the cross-over
point in
 satisfiability problems. In Pro c. AAAI'93, pp. 21{27.
 27Brafman
 Davis, M., & Putman, H. {1960}. A computing procedure for quantification
theory. Journal
 of the ACM, 7, 201{215.
 Do, M. B., Srivastav a, B., & Kambhampati, S. {2000}. Investigating the
effect of relevance
 and reachability constraints on sat encodings of planning. In Pro c. of
the Fifth Intl.
 Conf. on AI Planning and Scheduling Systems.
 Ernst, M. D., Millstein, T. D., & Weld, D. S. {1997}. Automatic SAT-compilation
of
 planning problems. In Pro c e e dings of the International Joint Conferenc
e on Artificial
 Intel ligence.
 Fikes, R., & Nilsson, N. {1971}. Strips: A new approach to the application
of theorem proving to problem solving. Artificial Intel ligence, 2 {3{4},
189{208.
 Freeman, J. W. {1995}. Improvements to Prop ositional Satisfiability Sear
ch Algorithms.
 Ph.D. thesis, U. Pennsylvania Dept. of Computer and Information Science.
Genesereth, M. R., & Nilsson, N. J. {1987}. Lo gic al Foundations of Artificial
Intel ligence. Kaufmann, Los Altos, CA.
 Gomes, C. P., Selman, B., & Kautz, H. {1998}. Boosting combinatorial search
through randomization. In Pro c. of 15th Nat. Conf. AI, pp. 431{437. Haslum,
P., & Geffner, H. {2000}. Admissible heuristics for optimal planning. In
Pro c. of
 the Fifth Intl. Conf. on AI Planning and Scheduling Systems, pp. 140{149.
 Kambhampati, S., Parker, E., & Lambrecht, E. {1997}. Understanding and exending
graph-
 plan. In Pro c. 4th Europ e an Conf. on Planning, pp. 260{272. Kautz, H.,
& Selman, B. {1992}. Planning as satisfiability. In Pro c. of the 10th Europ
e an Conf. on AI, pp. 359{363. Kautz, H., & Selman, B. {1996}. Pushing the
envelope: Planning, propositional logic, and
 stochastic search. In Pro c. of the 13th National Conferenc e on AI {AAAI'96},
pp.
 1194{1201.
 Kautz, H., & Selman, B. {1999}. Unifying sat-based and graph-based planning.
In Pro c.
 16th Intl. Joint Conf. on AI {IJCAI'99}, pp. 318{325.
 Li, C. M., & Anbulagan {1997}. Heuristics based on unit propagation for
satisfiability
 problems.In Pro c. IJCAI-97.
 McDermoot,D. {1996}. A heuristic estimator for means-ends analysis in planning.
In Pro c. 3r d Int. Conf on AI Planning Systems, pp. 142{149.
 Nebel, B., Dimopoulos, Y., & Koehler, J. {1997}. Ignoring irrelevant facts
and operators in plan generation. In Pro c. 4th Europ e an Conf. on Planning.
 28