Computing Upper Bounds on Lengths of Transition Sequences

1 Introduction

Lower bounds on lengths of action sequences have been studied extensively in the AI literature [Culberson and Schaeffer, 1996; Korf, 1997; Haslum and Geffner, 2000; Bonet and Geffner, 2001; Dr¨ager et al., 2009], in connection with optimal search algorithms such as A⋆ [Hart et al., 1968]. Studies of upper bounds are less common and more limited. In this work, by upper bound N we mean that, if a solution to the problem exists, the length of an optimal solution is no greater than N. An exponential upper bound for a planning problem described using N Boolean state variables is 2N - 1. Tighter bounds are known for restricted cases. For example, if actions only have positive preconditions and effects, no action ever needs to be taken more than once. In that case the number of actions is an upper bound on the shortest plan [Bylander, 1994]. Despite this and other important insights about restricted classes of actions [Brafman and Domshlak, 2003; Gim´enez and Jonsson, 2012], a procedure for inferring upper bounds for a broad range of problems has remained elusive.

∗Also affiliated with the Institute for Integrated and Intelligent Systems, Griffith University, Australia, and the Helsinki Institute of Information Technology, Finland. This work was funded by the Academy of Finland (Finnish Centre of Excellence in Computational Inference Research COIN, 251170).

†Also affiliated with the Artificial Intelligence Group, Australian National University, and the Institute for Integrated and Intelligent Systems, Griffith University, Australia. NICTA is funded by the Australian Government as represented by the Department of Broadband, Communications and the Digital Economy and the Australian Research Council through the ICT Centre of Excellence program.

Charles Orgill Gretton†

Optimisation Research Group NICTA, Australia

There are several uses for upper bounds in solving reachability problems. First, there is the detection of (sub)problems that have no solution. In explicit state-space search, if for a state s the distance from s to a goal state has a lower bound l and an upper bound u with u < l, then the goal state is not reachable from s, and s can be pruned from the search. In the case of the planning as satisfiability approach [Kautz and Selman, 1996], a sequence of satisfiability tests, for example testing the existence of plans of lengths 1,≤ 2,≤ 3, and so on, is performed. Tight upper bounds yield a practical termination test for this procedure, because once we have tested at the upper bound, if no solution was found, then none exists.

A second application is limiting the search effort in approaches that reduce the overall reachability problem to a sequence of fixed-length reachability problems, as in planningas-SAT and related approaches. The efficiency of this type of plan search lies in the strategy used to focus search effort on different horizon lengths [Rintanen, 2004; Streeter and Smith, 2007]. These strategies benefit from having tight upper and lower plan length bounds. The Streeter and Smith procedure performs a binary search over horizon lengths, and relies on tight initial bounds. The algorithms by Rintanen do not require tight upper bounds, however they can avoid a great deal of unnecessary search where a tight upper bound is given.

In this paper we have taken the first step towards a general approach to computing such upper bounds. Section 2 formally defines the succinct reachability problem. In Section 3, we recall the simplest and best known exponential upper bounds obtained from the cardinality of the state space, discuss exponential upper bounds obtained from the cardinality of the action set, and discuss how invariants can inform better bounds. In Section 4 we propose a decomposition of the set of state variables according to a dependency graph. We describe an approach which analyzes that graph to compute plan length bounds. In Section 5 we evaluate that procedure with a number of planning benchmarks used in the International Planning Competitions (IPC) from 1998 to 2011. Finally, in Section 6 we conclude the paper by pointing to future research directions.

2 Preliminaries

We formalize the planning problem as a 4-tuple Π = 〈X, I,A,G〉 where X is a finite set of Boolean state variables, which induces a state space S(X) consisting of all states s : X → {0, 1} that are total functions from the state variables to 0 and 1, I : X → {0, 1} is the initial state, A is a finite set of actions (p, e) where the precondition p and the effects e are consistent sets of literals over X, and G, the goal, is a set of literals over X.

Given a state s, its successor s′ = execa(s) with respect to action a = (p, e) ∈ A is the state that satisfies s′ |= e and s′ (x) = s(x) for all x ∈ X such that x does not occur in e. This is defined iff s |= p. An action sequence a1, . . . , an is executable (in state s) if execan (execan-1 (· · · execa2 (execa1 (s)))) is defined. A plan for Π = 〈X, I,A,G〉 is a sequence a1, . . . , an of actions from A such that execan (execan-1 (· · · execa2 (execa1 (I)) · · · )) |= G.

We can project a planning problem Π = 〈X, I,A,G〉 to a subset X′ ⊆ X of state variables, obtaining Π ↓ X′ = 〈X′ , I ↓ X′ , {a ↓ X′ |a ∈ A},G ↓ X′ 〉, where I ↓ X′ = {(x, v)|(x, v) ∈ I, x ∈ X′} by limiting the state to variables in X′ , (p, e) ↓ X′ = (p′ , e′ ) obtained from (p, e) ∈ A by removing all literals with a state variable in X\X′ from both p and e. Finally G ↓ X′ is obtained from G by deleting literals with variables not in X′ .

Further, we can project an action sequence a1, . . . , an to a set X′ ⊆ X of state variables by projecting the actions to X′ , obtaining an ↓ X′ , . . . , an ↓ X′ and then deleting those projected actions that have empty effects (that is, the actions that do not have any effect on variables in X′ ).

Our method for deriving upper bounds is based on a decomposition of a directed graph into its strongly connected components (SCC). An SCC of a directed graph is a subgraph in which there is a directed path from each vertex to every other vertex. A successor of an SCC S is an SCC S′ so that, in the underlying graph, there is an arc from a vertex in S to a vertex in S′ . A predecessor of S is a component which has S as a successor. The ancestors of S are the SCCs, other than S, for which there is a directed path in the underlying graph from a vertex in the component to one in S. In this work we shall often identify an SCC with the set of vertices in that subgraph.

3 Plan Length Upper Bounds

A plan length upper bound can be obtained from the cardinality of the state space by observing that a shortest path in the transition graph never visits any state twice: if a state is visited twice, all the actions between these two occurrences of the state could be removed to obtain a shorter plan.

Lemma 1 For a problem over Boolean variables X s.t. N = |X|, the shortest plan cannot be longer than 2N - 1. That bound is tight: one can give a problem with N actions which increment an N-bit counter by one, depending on the number of least significant bits that are 1.

Another upper bound can be obtained from the number of actions. It may be useful when |X| is large relative to |A|, which is the situation when actions have preconditions and effects that refer to a high number of state variables.

Lemma 2 If there are m = |A| actions and a plan exists, then the length of the shortest plan is at most ∑mi=0 m! (m-i)! - 1. This bound is tight.

Proof: Any state reached by a (finite or infinite) sequence of actions from A is uniquely determined by the order of the last occurrences of each of the m actions. The truth value of any state variable, after taking a sequence of actions in the initial state, is the last value assigned to it, or if no action has affected it, its initial value. In other words, I and the order of last occurrence of each action determines the reached state uniquely. As there are at most m! relevant action sequences, there can be at most m! different states. When any i of the m actions are used, there are m! (m-i)! different action sequences, and we of course have to consider all i between 0 and m to account for all states reachable by plans that contain at most m different actions. For tightness, the reader can verify that, in the following example the bound equates to the number of reachable states, and that a plan in this example might be equal in length to the number of reachable states minus one. Take A = {a1, .., am} and X = {x1, .., xm} ∪ {yi,j|1 ≤ i < j ≤ m}. Actions are aj = (∅, {xj , yj,j+1, .., yj,m, ¬y1,j , .., ¬yj-1,j}) so that each action j sets xj = yj,k = 1 ∀k ∈ {j +1, ..., m} and yk,j = 0 ∀k ∈ {1, ..., j - 1}. □

Further assumptions about the properties of individual actions or their interrelations are needed to derive tighter upper bounds. We shall not explicitly consider actions with conditional (state-dependent) effects. Bounds based on the properties of state variables remain valid in that case, but those based on action set cardinality do not. With conditional effects it is possible to represent an increment action, which can be repeated 2N - 1 times to increase an N-bit counter from 0 to 2N - 1. Hence a small number of actions does not necessarily yield practically significant upper bounds.

3.1 Invariants

Invariants [Gerevini and Schubert, 1998; Rintanen, 2008] represent dependencies between state variables in the reachable state space. They characterize unreachable states, and have been used to derive compact state representations for explicit state-space search. Most invariants used in practice can be expressed as clauses with one or two literals (unit clauses l and binary clauses l ∨ l′ ). We employ 2-literal invariants to derive tighter plan length bounds.

Lemma 3 Let 〈X, I,A,G〉 be a problem instance so that ¬x∨¬x′ is an invariant for all {x, x′} ⊆ X such that x ̸= x′ . A shortest plan has at most n actions, where n = |X|.

Proof: The invariants imply that one state variable can be true at any state reachable from I. The number of reachable states is at most |X|+1 (including the state in which all of the state variables are false). A plan visiting a subset of these states, with no state visited twice, has at most |X| actions. 1 □

1 In many problems arising in practice there is a guarantee that at least one of the state variables is true, for example because any

The structure of the set of invariants in the above lemma is specific. For arbitrary sets of invariants, each taking the form of a 2-literal clause, looser upper bounds hold. Tractable exact model-counting is possible for sets of 2-literal clauses satisfying certain graph-theoretic properties [Luna et al., 2007], but these properties do not seem to be of practical relevance to 2-literal invariants arising in typical planning problems. In any case, we can employ general model-counting for Boolean 2SAT-i.e. clauses have at most 2 literals- to obtain upper bounds based on the cardinality of the state space by leveraging problem invariants.

4 Bounding via Dependency Graph Analysis

For many problems that occur in practice, the discussed bounds are impractically loose. We now describe how dependencies between problem variables can be expressed using a graph, and leverage problem decompositions suggested by that graph in order to obtain tight bounds. In particular, we shall describe and analyse a type of dependency graph that suggests a decomposition of the problem into subproblems. The concept of a dependency (often termed causal) graph was first described by [Knoblock, 1994] and [Williams and Nayak, 1997], and has since found myriad uses in both theoretical and practical works. Intuitively, dependency graphs express dependencies between state variables in terms of the ability of one variable to impact the value of another. For some classes of problems such graphs expose small subproblems with few interconnections, with the subproblems' size independent of parameters determining the overall problem size. We shall explore how upper bounds on the lengths of solutions to subproblems yield a bound for the underlying problem.

Definition 1 The dependency graph of a planning problem is the directed graph G = (V, E) that satisfies the following. The vertices V are the set of state variables. There is an arc (v, v′ ) ∈ E iff either

1. there is an actionwhose effect is described using a literal over v′ (i.e. using either v′ or ¬v′ ), and a literal over v is a precondition of that action; or
2. literals over v′ and v occur together in the description of an action effect, and v occurs both positively and negatively in the effects of problem actions.

Definition 1 departs from a number of other definitions of dependency graphs. In particular, the classical causal graph includes the arc (v, v′ ) if v′ and v occur together in the description of an action effect.

We illustrate Definition 1 in Figure 4, which depicts the dependency graph for a simple instance of the logistics benchmark from the IPC in 2000. The problem we consider has one package, p, one aeroplane, ap, three trucks, t1, t2, and t3, and three cities. Each city contains one of the airport locations, a1, a2, and a3, and one of the corresponding innercity locations c1, c2, and c3. The aeroplane can visit every airport location. The fact that ap is visiting a1 is expressed by the Boolean variable At(ap, a1) begin true. Each truck can visit the airport and downtown locations of its home city. For example, the truck t1 can be visiting either c1 or a1. The package can be transported between locations with the appropriate vehicles. For example, ap can transport p between any two airports, and trucks can transport p between an airport and its corresponding inner-city location. The edges of the dependency graph in Figure 4 capture the conditions for moving vehicles, and those for loading/unloading the package. For example, to move from location c1 to the airport a1, the truck t1 must be visiting c1. For package p to be loaded into a vehicle, to achieve In(p, t1) for example, both the vehicle and p have to be at the same location. Similarly, to unload p to a location, p must of be inside the vehicle we intend to unload, and that vehicle must be visiting the location.

action making a state variable false also makes another variable true. Hence the state with all variables in X false is not reachable, and the upper bound on actions is |X| - 1 instead of |X|.

We can decompose a dependency graph into its strongly connected components (SCC) in linear time [Tarjan, 1972]. 2 An SCC with no outgoing arcs induces an abstract planning problem with actions that change the state variables in that SCC only. Considering SCCs in a planning context more generally, exactly those actions belong to an SCC that change at least one variable in the SCC, and which add/delete only variables in the SCC and its successors.

2 Assuming that a symbol table for node names with linear-time access has been built, a O(n log n) computation.

Continuing with our logistics example, in Figure 4 we have labeled each vertex with its corresponding variable, and also with a number that indicates the SCC that vertex participates in. For example, variables At(p,ap) and In(p,c1) participate in an SCC labeled 1, while At(t1,c1) and At(t1,a1) participate in 2. Taking i, j ∈ {2..5} and i ̸= j, the reader can observe that for SCCs labeled i and j respectively, there are no directed paths between vertices in i and j. In other words, any action that alters the location of a vehicle cannot interfere with an action that alters the location of a different vehicle. If the problem goal is to rearrange the vehicles, then we can plan independently for each vehicle. The overall plan for our logistics problem in that case need not be longer than 5 steps.

A less contrived example of such independence occurs in the rovers benchmark from the IPC in 2006. Here, an autonomous planetary rover must acquire and transmit scientific data which can be acquired by visual analysis (image data), or otherwise by analysis of soil and rock. Acquisition of the former is independent of the latter, and in the SCC decompositions of graphs associated with rovers instances, there is one component with actions for soil/rock analysis, and another for image analysis. A plan for such problems can be the composition of a plan for acquisition and transmission of image data followed by a plan for the soil/rock task. In our work we exploit such independence to obtain upper bounds on the lengths of plans in rovers, and similar domains.

We must also consider the case where variables in an SCC are dependent on those from a different SCC. We shall proceed with the example in Figure 4 for the moment. Taking a conventional logistics goal, of delivering p to a particular location, we are left to address dependencies between the locations of vehicles and our ability to alter the location of p. In order to derive upper bounds for this case, we appeal to an abstraction refinement scheme suggested by the dependency graph, which was previously reported in [Knoblock, 1994]. Observe that there are no directed paths from a vertex in SCC labeled 1 to any vertex with SCC i ̸= 1. Let S1 be the set of variables associated with vertices with SCC label 1. If a plan for the logistics problem exists, then a plan shall correspond to a refinement of an abstract plan for the problem Π ↓ S1.

Definition 2 Given a problem Π, let π be an abstract plan for Π ↓ Z, and Z ′ a set of problem variables satisfying Z ⊂ Z ′ . A plan π′ for Π ↓ Z ′ is a refinement of π iff there exists a correspondence function c mapping each action in π to one in π′ , satisfying:

1. ∀a ∈ π, both c(a) and a are projections of the same action in Π.
2. If a1 precedes a2 in π, then c(a1) precedes c(a2) in π′ .
3. ∀a3 ∈ π′ where ∄a1 ∈ π s.t. c(a1) = a3, we have ∃a2 ∈ π, (p, e) = c(a2), a3 precedes c(a2) in π′ , there is a precondition literal x ∈ p whose subject is a variable from Z ′\Z, and in every deordering of the serial π′

into a valid partially ordered plan, there is a causal chain from a3 to the precondition x.

Generally, where Z are the variables/vertices in an SCC, a plan for the abstract problem Π ↓ Z can be, by a process of iterative refinement, extended into progressively less abstract plans. A bound on the length of the abstract plan for Π ↓ Z can be obtained using the insights of Section 3.1. Each step of iterative refinement adds actions from, and only from, the predecessor SCCs. Repeating the bounding exercise that we did for Π ↓ Z, we can calculate a bound on the length of such a refinement, and by induction a bound on the length of the plan refined to the point that it is part of a solution to Π.

In later sections we shall develop these ideas formally and algorithmically. For now we further illustrate the above scheme, to show more concretely how counting according to the variable dependencies of a problem can give significantly tighter bounds compared to those of Section 3.1. A package can only be at one place at a time, therefore by Lemma 3 an abstract plan for S1 in our logistics example has upper bound 9. 3 An abstract plan will be of the form a1, a2, .., a9 where each ai is a load/unload action. We must now consider inserting additional transportation actions into that abstract plan. A refinement will have the form σ1, a1, σ2, a2, .., σ9, a9, where σi terms are sequences of actions from SCCs with indices in 2..5, for example drive and fly actions. We have already seen that each σi is of length at most 5, therefore a plan length upper bound for our logistics example is 54.

4.1 Formalization

Where Π is a problem, we write ℓ(Π) for the length of the longest optimal execution in Π, that is, the maximum possible length of a shortest possible action sequence in Π from the initial state to another state in Π. Notice that ℓ(Π) is independent of the goals. Writing π(s) for the set of all executions in Π from the initial state I to s and |π| for the length of the plan π,

Lemmas 1, 2 and 3 provide bounds on ℓ(Π). For the longest plan, written ℓ(Π; G), we have

Note that ℓ(Π;G) ≤ ℓ(Π). Given a strongly connect component S, we write P(S) for the set of all vertices in the ancestors of S. Where S is an SCC with vertices Y , we write Π ↓ S to denote the underlying problem projected to Y .

Theorem 4 Let S be the set of components in the dependency graph for Π which have no successors. Then we have

Moreover, for each S ∈ S we have

3 A tighter bound of 6 might be observed, however that requires inference beyond the simple counting of Section 3.1.

Proof: A sketch of our proof follows. First, consider the situation where the dependency graph corresponds to a classical causal graph. In that case there is always an edge (v, v′ ) whenever literals over v and v′ occur in the same action effect. Every refinement of a plan π ↓ Z is an ordered refinement (see [Knoblock, 1994, Definition 4]) provided there is no directed path in that graph from a variable in Z to any variables added by that refinement. In this case our result follows from the fact that layered plan refinement prescribed by [Knoblock, 1994] never adds or deletes variables that occur in the abstract plan being refined. We are left to examine the following situation. Take an abstract plan π ↓ Z, and a refinement π ↓ Z ∪ Y so there is no directed path in the dependency graph from a variable in Z to any variable in Y . For some v ∈ Z, v′ ∈ Y we suppose: (a) both those variables occur together in one or more action effects, and (b) v occurs uniformly positive (negative) in action effects. By definition, the actions added by a legal refinement π ↓ Z ∪ Y of π ↓ Z cannot have a precondition that mentions v - otherwise there would be a precondition-effect edge from v to v′ violating our stated path condition. In the refinement problem the variable v cannot be a goal (because v ∈ Z) or precondition. Therefore, if there is a refinement π ↓ Z ∪ Y to π ↓ Z, it must be equal to a refinement π ↓ Z ∪ Y \v to π ↓ Z\v in terms of the actions and their ordering. Our result follows, because in bounding the number of actions added during a refinement from π ↓ Z to π ↓ Z ∪ Y , v need not be considered. □

Theorem 4 informs how we can obtain sub-exponential upper bounds in practice. The term ℓ(Π ↓ S) can be approximated using the insights presented in Section 3.1. We can approximate ℓ(Π ↓ P(S)) terms by examining the subgraph defined for vertices P(S). In particular, we can recursively use the above bounding expressions for the smaller problem Π ↓ P(S), and so on. The recursion terminates when the subgraph over P(S) has only one SCC S′ , in which case we approximate ℓ(Π ↓ P(S)) again following Section 3.1. 4

We have excluded some inter-effect arcs used in earlier definitions of causal graphs. This poses the question: Can we exclude all arcs that are purely inter-effect, in the sense that they are solely included in the graph due to Condition 2 of Definition 1, and still have Theorem 4? The following example shows that at least some of those arcs are required.

Example 1 Consider the actions below, described using the variables x0, .., xn-1, γ and y0, .., yn-1, ψ, ψ′ .

The actions defined over x1, .., xn-1 count (in binary) from 0 to 2n - 1. Setting the least significant bit of the counter to 0 has the effect γ = 1, requiring (if the goal is to be achieved) setting ψ to true with the action (∅, {¬γ, ψ}) before further such increments are possible. Setting the least significant bit of the counter to 1 sets the variable ψ′ true. Suppose ¬ψ, ¬ψ′ ∈ G, and notice that one of those literals must be false so that the plan can affect any of y0, .., yn-1. No plan prefix can include a state s s.t. s |= ψ ∧ ψ′ . Whenever ψ = 1 (resp. ψ′ = 1), it can only be made false by counting from 0 to 2n - 1 using the bits y0, .., yn-1. In other words, each increment of 1 in x0, .., xn-1 is followed by 2n - 1 increments in y0, .., yn-1. Hence every change in the first counter forces counting through all values of the second counter, inducing a shortest plan of length 2n - 1 + (2n - 1)2n = 22n - 1 for the problem with all variables false in the initial state and all variables except ψ and ψ′ true in the goal state. Without pure inter-effect arcs we would get two unconnected SCCs and a too low upper bound, which is the sum of the upper bounds for the two SCCs, and not their product as it should be. ■

4 If the ancestors of S do not mention goal propositions we have ℓ(Π ↓ S ∪ P(S); G) ≤ ℓ(Π ↓ S)ℓ(Π ↓ P(S)) + ℓ(Π ↓ S).

4.2 Algorithm

Our bounding procedure can be outlined as follows.

1. Let a vertex v be the subject of a goal literal l ∈ G iff l = v or l = ¬v. If v is not the subject of a goal literal, and if there is no directed path from v to a vertex which is the subject of a goal literal, then we remove v from the dependency graph. It is straightforward to see that any minimal length plan in the underlying problem Π is a minimal length plan in Π ↓ X\v and vice versa.
2. We associate with each SCC S a positive integer value vS. Intuitively, vS is equal the maximum length of a shortest (abstract) execution which only changes the values of state variables in S. For vS we take the minimum bound provided by Lemmas 1, 2 and 3 where applicable, and in situations where some (not all) of the variables in S are mutex, we use model-counting to derive a bound based on the cardinality of that abstract state space.
3. Topologically sort the SCCs and go through them so that the calculations related to an SCC S (summarized as values vS and below tS) is carried out after the calculations for all its ancestors have been completed.
4. We associate with each SCC S a positive integer value tS . Intuitively, tS is an upper bound on the length of an (abstract) action sequence that affects variables in S and its ancestors, with the purpose of achieving a given valuation (which may be determined by the top-level goal G, or by preconditions in the top-level plan with occurrences of variables in S).

An upper bound is obtained from vS by assuming that a maximal number of actions are needed between any two actions in π ↓ S. That is, before and after every action in π ↓ S, we may need tS′ actions from every predecessor SCC S′ of S. Hence,

Above, we multiply the sum by vS (not 1 + vS) if no ancestor of S includes a goal variable. Note that actions affecting both S and its ancestor S′ are counted multiple times.

1. The final step sums the tS terms for all SCCs S that have no successors. Let S1, .., Sm be all such SCCs, then a plan length upper bound is tS1 + .. + tSm .

5 Experimental Evaluation

We have implemented our algorithm as a program that takes a planning problem as input, constructs the dependency graph, and then derives an upper bound on the length of a plan. All experiments were performed using a compute cluster of 2 GHz Intel Xeon E6540 nodes. In cases where good bounds according to our decomposition are only available by modelcounting, we have used CACHET [Sang et al., 2005] to bound the length of plans for the abstract problems induced by SCCs. Deriving the upper bounds is computationally cheap, whether we use Lemmas 1, 2 or 3, or in situations where we resort to model-counting. In the case of all reported results, the only costly calculation associated with our approach is the detection of 2-literal invariants (taking some dozens of seconds for the largest instances), which is required by Lemma 3. Because that computation is standard in all competitive planners, it is not an additional overhead.

As test material, we used the benchmark sets from the planning competitions. Plan lengths typically vary from some tens to some hundreds of steps. Humans can typically derive relatively tight upper bounds on plan lengths in these domains. The results we obtained with automated bounding are reported in Table 1. We have presented data for the 8 domains where an upper bound can be ≤ 2.5k, a horizon at which the state-of-the-art SAT-based planner MP [Rintanen, 2012] can routinely solve problems in under 30 minutes. That ≤ 2.5k condition is met for 69 instances, 18 of which are from logistics, and another 30 from the trivial domain movie. In Figure 5 we explore the relationship between the upper bounds we are able to derive and the number of problem variables. The figure highlights our key claim: Our decomposition can yield sub-exponential growth in upper bounds as the number of variables increases, into the hundreds, and even into the thousands. This is particularly evident in domains satellite and logistics, where no model-counting is necessary, 5 and in zeno.

It is worth understanding why our approach works so effectively in logistics. There are no capacity constraints on the transports. The location of a package does not alter the possibility of moving transports, and there is no dependence between any two transport's actions either. Also, package movements are mutually independent. A consequence of all this independence is that the number of SCCs in the dependency graph is equal to the number of transports and packages. The number of variables in the SCC associated with a package is equal to the number of places the package can be. Moreover, Lemma 3 applies to every SCC. Each package and each transport can only be in one place at a time.

The benefit of omitting some of the inter-effect arcs in the dependency graph in Definition 1, though broadly important, can be more concretely understood by examining rovers. The graph associated with the second problem in that benchmark has 7 SCC if all inter-effect arcs are included. A graph excluding those arcs has 10 SCC, with additional components of size 1 for each of the propositions have rock analysis, have soil analysis and have image, that is, all facts that can only become true once, and then remain true. Bounding with all inter-effect arcs yields 235 steps, and 122 steps according to Definition 1. The difference occurs because using the former we are bounding abstract plans that achieve facts, such as have image, multiple times. These facts cannot be made false and hence need only be achieved once, a constraint that cannot be expressed using invariants.

5 i.e. our approach is tractable in both those domains.

We can leverage upper bounds in SAT-based planning to prove that a problem admits no solution. We experimented using a version of rovers with qualitative preferences (QP) from the IPC in 2006. Haslum (2007) proposed an optimal QP solution procedure that operates by solving open sets, which are sets of classical goal-oriented STRIPS problems. Whether or not these problems admit solutions allows us to infer plan-cost bounds about the underlying QP problem. We obtained "open sets"-each of which is a set of STRIPS problems-for each of the unsolved QP rovers problems from the competition. Specifically, QP rovers problems 06 to 19. Each of the sets contains at least one STRIPS problem for which it was not known whether it admits solutions. In total, we have a corpus of 1440 STRIPS problems.Of those, Mp cannot easily find a plan in 86 problems.

Problem 06 in the QP series has remained open since 2006, i.e. it was not known whether a candidate plan was optimal. In this case, the most challenging STRIPS problem which does not admit a solution has a bound of 3486 steps. In conjunction with our upper bounds, given a 1 GB memory limit and 2 hour time limit MP is able to close rovers 06. Our approach is to remove all easily solvable instances from the open sets, and for the remaining instances (none admitting solutions), in each case we prove that no plan exists for a subset of the goals. Adding 1 goal literal at a time, in each iteration choosing to add the literal that minimises the upper bound of the resulting instance, MP quickly proves there is no solution. Our approach mitigates upper bound bloat. For example, rather than producing a proof for 3486 steps, which takes days, we produce a proof in hours for 730 steps and 4 (of a possible 11) goal facts. It is worth noting that breadthfirst search is ineffective in solving problems from these open sets, and that recent admissible landmark-based heuristics offer no guidance here.

Considering planning by forward search of the state space more generally, admissible pattern database (PDB) heuristics can be leveraged to prove that no plan exists. First, it is worth noting that given a 4 GB memory limit the state-of-the-art PDB approach by Haslum et al. (2007) cannot solve the challenging instances that admit no solutions, including those associated with rovers QP problem 06. 6 The allocated memory is quickly exhausted during search. We find that PDB approach can benefit from the iterative goal inclusion procedure outlined above. We prove that 34 of the 86 problems have no solution. Of those 34 problems, 4 are very hard, and cannot be solved using the PDB approach alone due to memory (4 GB) being exhausted. Addressing computation time in this setting, we can report a very significant savings also. Using iterative goal selection, in the 30 STRIPS problems with no plans which can be solved by both our approach and a generic PDB search, we save a total of 646 CPU-seconds. Putting that in perspective, refutation guided by our upper bounds in those problems takes less than 5% of the time taken by a vanilla PDB search.

6 We used the PDB implementation by Sievers et al. (2012).

6 Conclusions and RelatedWork

Treating a classical (deterministic perfect information) planning setting, we developed an approach to computing upper bounds on the lengths of solutions in transition system problems. This is achieved by first constructing a dependency graph, which expresses dependencies between state variables, and then decomposing that graph into SCCs. A number of earlier works have leveraged dependency graph structures with the motivation of delimiting the boundary between tractable and intractable planning with single-effect actions [Williams and Nayak, 1997; Brafman and Domshlak, 2003; Jonsson and B¨ackstr¨om, 1998]; a motivation that is orthogonal to ours, of computing upper bounds. In our work, variable independence exhibited by the graphical decomposition is used to obtain an additive expression for an upper bound on the solution length. Factors in that expression are upper bounds on the lengths of solutions to abstract subproblems, obtained in this work according to state space cardinality arguments. We considered two techniques for bounding in subproblems. The first is a polynomial time procedure that appeals to problem invariants and a small fixed set of bounding expressions. The second poses some cardinality questions as 2SAT model-counting problems. Model-counting here, although not tractable, is very efficient. In our experience so far, we have not found that 2SAT model-counting is a bottle neck. In a number of domains where problem variables can be partitioned into components representing physical or virtual objects, the decomposition to SCCs yields several small SCCs, often with a size that is independent of the number of objects and size of the underlying problem. For these types of problems our decomposition method can yield polynomial upper bounds of practical importance. For example, we were able to close an open plan existence problem.

It is also worth noting a previous study related to our own, which developed a different upper bound concept for cost-optimal planning using constraint satisfaction techniques [Cooper et al., 2011]. Those authors addressed the situation where a (suboptimal) plan is already known, and describe how one can then tractably answer the question: Assuming a better (lower cost) plan exists, what is an upper bound on the length of such a plan? Unlike our approach, Cooper et al. assume the question of plan existence is a priori answered positively. An interesting direction for future work is to use dependency graph decompositions to obtain tighter bounding expressions in that setting.

Wrapping up, there are a few considerations for future research worth highlighting. Numerous planning benchmarks admit well-known tight upper bounds, and yet our procedure is unable to derive them. For example, IPC benchmarks blocksworld and gripper admit well known linear bounds. An interesting avenue of research is to explore in what situations dependency graph derived bounds can offer tight approximations of the lengths of optimal plans. Also, an important direction for future research is to derive additional problem constraints with the properties: (a) a solution exists iff a solution to the over-constrained problem exists, and (b) the over-constrained problem yields tight bounds (e.g. via 2SAT model counting with strong invariant conditions in the over-constrained problem). Constraints on the order in which objects/resources can be used (e.g. lex-leader) will likely be fruitful here. Future extensions of our framework should also study upper bounds for parallel plans.