# planlength_bounds_beyond_1way_dependency__9d915ace.pdf

The Thirty-Third AAAI Conference on Artiﬁcial Intelligence (AAAI-19)

Plan-Length Bounds: Beyond 1-Way Dependency

Mohammad Abdulaziz Technical University of Munich, Munich, Germany

We consider the problem of compositionally computing upper bounds on lengths of plans. Following existing work, our approach is based on a decomposition of state-variable dependency graphs (a.k.a. causal graphs). Tight bounds have been demonstrated previously for problems where key dependencies ﬂow in a single direction i.e. manipulating variable v1 can disturb the ability to manipulate v2 and not vice versa. We develop a more general bounding approach which allows us to compute useful bounds where dependency ﬂows in both directions. Our approach is practically most useful when combined with earlier approaches, where the computed bounds are substantially improved in a relatively broad variety of problems. When combined with an existing planning procedure, the improved bounds yield coverage improvements for both solvable and unsolvable planning problems.

Introduction Many techniques for solving reachability problems in transition systems, like SAT-based planning (Kautz and Selman 1992) and bounded model checking (Biere et al. 1999), beneﬁt from knowledge of upper bounds on the lengths of transition sequences, aka completeness thresholds. If N is such a bound, and if a transition sequence achieving the goal exists, then that sequence need not comprise more than N actions. Biere et al. (1999) identify the diameter and the recurrence diameter, which are topological properties of the state space, as conceptually appealing upper bounds. The diameter is the longest shortest path between any two states. The recurrence diameter is the longest simple path in the state space, i.e. the longest path that does not traverse any state more than once. Approximate and exact algorithms have been developed to calculate both properties given an explicit (e.g. tabular) representation of the transition system. Exact algorithms to compute the diameter have worse than quadratic runtimes in the number of states (Fredman 1976; Alon, Galil, and Margalit 1997; Chan 2010; Yuster 2010), and approximation approaches have super-linear runtimes (Aingworth et al. 1999; Roditty and Vassilevska Williams 2013; Chechik et al. 2014; Abboud, Williams, and Wang 2016). The situation is even worse for the recurrence diameter, whose computation is

Copyright c 2019, Association for the Advancement of Artiﬁcial Intelligence (www.aaai.org). All rights reserved.

NP-Hard (Pardalos and Migdalas 2004). The impracticality of those explicit algorithms is exacerbated in settings where systems are described using factored representations, like planning and model-checking, since a system s explicit representation can be exponential in the size of the corresponding factored problem description. However, compositional approaches to calculate bounds for problems described using factored representations are feasible. The concrete system s (recurrence) diameter is bounded by composing together bounds for abstract subsystems. The subsystems are projections of the concrete system. The motivation for compositional approaches is that they provide useful approximations of plan bounds using smaller computational effort, since only explicit representations of abstract subsystems have to be constructed. Baumgartner, Kuehlmann, and Abraham (2002) and Rintanen and Gretton (2013) followed this projection-based approach to develop procedures to compositionally bound the diameter. This was later improved by Abdulaziz, Gretton, and Norrish (2015) and Abdulaziz, Gretton, and Norrish (2017) (we refer to those two papers as AGN1 and AGN2 hereafter). A common drawback with previous approaches, however, is that they are only usefully applicable if the projections are induced by acyclicity in the causal/dependency graph (Williams and Nayak 1997; Knoblock 1994). Thus it is an open question as to whether there are practically useful ways to upper-bound plan lengths using projections not resulting from dependency graphs with acyclicity. We address this question by developing a compositional bounding procedure which is applicable to arbitrary projections. We do so by deﬁning a new topological property for the state space to which we refer as the traversal diameter. The distinctive feature of the traversal diameter is that, for any given factored transition system, the traversal diameter of that system is upper bounded by the product of the traversal diameters of projections of that system. Those projections can be obtained using any partition of the system s state variables, i.e. the restriction of having acyclic dependencies is not required for this compositional bound. Using the traversal diameter based compositional method to bound concrete problems is not very practically useful since it uses the product of all the projections traversal diameters as the bound. However, the utility of this new procedure is most pronounced when combined with previous

state-of-the-art algorithms from AGN1 and AGN2. We use the traversal diameter based method to further decompose atomic sub-problems , which are abstractions that cannot be further abstracted by the algorithms from AGN1 and AGN2. We experimentally show that this additional decomposition improves the bounds computed by the algorithms from AGN1 and AGN2. For instance, bounds computed using the method from AGN2 improved in 68% of the planning problems on which we experimented, with an improvement of at least 50% in 71% of the cases. We also use the bounds computed by the new algorithm as horizons for the SAT-based planner Madagascar MP (Rintanen 2012). This improves the coverage of MP in both solvable and unsolvable planning instances compared to the default query strategies or to upper bounds computed by all previous algorithms as horizons.

Background and Notations Compositional bounds are deﬁned on factored transition systems which are purely characterised in terms of a set of actions. From actions we can deﬁne a set of valid states, and then approach bounds by considering properties of executions of actions on valid states. Whereas conventional expositions in the planning and model-checking literature would also deﬁne initial conditions and goal/safety criteria, here we omit those features from discussion since the notion of diameter and other bounds are independent of those features.

Deﬁnition 1 (States and Actions). A maplet, v 7 b, maps a variable v i.e. a state-characterising proposition to a Boolean b. A state, x, is a ﬁnite set of maplets. We write D(x) to denote {v | (v 7 b) x}, the domain of x. For states x1 and x2, the union, x1 x2, is deﬁned as {v 7 b | v D(x1) D(x2) if v D(x1) then b = x1(v) else b = x2(v)}. Note that the state x1 takes precedence. An action is a pair of states, (p, e), where p represents the preconditions and e represents the effects. For action π = (p, e), the domain of that action is D(π) D(p) D(e).

Deﬁnition 2 (Execution). When an action π (= (p, e)) is executed at state x, it produces a successor state π(x), formally deﬁned as π(x) = if p x then x else e x. We lift execution to lists of actions π, so π(x) denotes the state resulting from successively applying each action from π in turn, starting at x.

We give examples of states and actions using sets of literals. For example, {a, b} is a state where state variables a is (maps to) true, b is false, and its domain is {a, b}. ({a, b}, {c}) is an action that if executed in a state that has a and b, it sets c to true. D(({a, b}, {c})) = {a, b, c}.

Deﬁnition 3 (Factored Transition System). A set of actions δ constitutes a factored transition system. D(δ) denotes the domain of δ, which is the union of the domains of all the actions it contains. Let set( π) be the set of elements from π. The set of valid action sequences, δ , is { π | set( π) δ}. The set of valid states, U(δ), is {x | D(x) = D(δ)}. G(δ) denotes the state space of δ, i.e. the digraph whose vertices are U(δ) and edges are {(x, π(x)) | x U(δ), π δ}.

Figure 1: a) is the largest connected component of the state space of δ in Example 1. b) and c) are the state spaces of the projections of δ on {v1, v2} and {v3, v4}. d) is the dependency graph GD(δ) of δ and e) is a lifted dependency graph GVS for δ. f) is a quotient of the state space of δ vs1.

Example 1. Consider the factored representation, δ = {π1 = ({v1, v2}, {v2}), π2 = ({v1, v2}, {v2}), π3 = ({v1, v2}, {v1, v2}), π4 = ({v1, v2}, {v1}), π5 = ({v1, v2, v3, v4}, {v4}), π6 = ({v1, v2, v3, v4}, {v3}), π7 = ({v1, v2, v3, v4}, {v3, v4})}. The digraph in Figure 1a represents the largest connected component in the state space of δ, where different states deﬁned on the variables D(δ) = {v1, v2 v3, v4} are shown. Interpreting δ as a transition system, it has two modes of operation. The ﬁrst mode changes the assignments of {v1, v2} and is represented by actions {π1 π4}. The second mode, represented by actions {π5, π6, π7}, changes the assignments of {v3, v4} and is only enabled if {v1, v2} are both set to true.

Compositional Bounding

For a system δ, a bound on the length of action sequences is EXP(δ) = 2|D(δ)| 1 (i.e. one less than the size of the state space), where | | denotes the cardinality of a set or the length of a list. Other bounds employed by previous approaches are topological properties of the state space like the diameter, suggested by Biere et al. 1999.

Deﬁnition 4 (Diameter). The diameter, written d(δ), is the length of the longest shortest action sequence, formally

d(δ) = max x U(δ), π δ min π (x)= π (x), π δ | π |

Note that if there is a valid action sequence between any two states, then there is a valid action sequence between them which is no longer than the diameter. Another topological property suggested by Biere et al. 1999 as a suitable upper bound is the recurrence diameter.

Deﬁnition 5 (Recurrence Diameter). Let distinct(x, π) denote that all states traversed by executing π at x are distinct states. The recurrence diameter is the length of the longest simple path in the state space, formally

rd(δ) = max x U(δ), π δ ,distinct(x, π ) | π|

Choosing a topological property as an upper bound depends on many factors. Size: for a system δ, d(δ) can be exponentially smaller than rd(δ), which in turn can be exponentially smaller than EXP(δ) (Biere et al. 1999). Complexity: computing EXP(δ) is the easiest since it can be done in a time linear in |D(δ)|, while the diameter can be computed in time at least quadratic in the size of the state space (Abboud, Williams, and Wang 2016), and the recurrence diameter is the hardest as it is NP-Hard in the size of the state space (Pardalos and Migdalas 2004). Usability: the diameter is a completeness threshold for SAT-based AI planning and bounded model checking of safety formulae, while the recurrence diameter is a completeness threshold for bounded model checking of fairness formulae (Biere et al. 1999). In this work, the most relevant trait of a topological property is the ability to compositionally bound it. By that we mean computing an upper bound on the topological property of a given system by composing topological properties of abstractions of that system. A key abstraction concept for compositional reasoning about transition systems is projection, which is deﬁned as follows. Deﬁnition 6 (Projection). Projecting an object (a state x, an action π, a sequence of actions π or a factored representation δ) on a set of variables vs restricts the domain of the object or the components of composite objects to vs. Projection is denoted as x vs, π vs, π vs and δ vs for a state, action, action sequence and factored representation, respectively. However, for action sequences or transition systems, an action with no effects after projection is dropped entirely. Example 2. Let vs1 = {v1, v2} and vs2 = {v3, v4}. A partition of the domain of δ from Example 1 is {vs1, vs2}. The projection δ vs2 = {π5 vs2 = ({v3, v4}, {v4}), π6 vs2 = ({v3, v4}, {v3}), π7 vs2 = ({v3, v4}, {v3, v4})}. The variables {v1, v2} were removed from action preconditions and effects, and actions with empty effects were removed. Figures 1b and 1c show the state spaces of the projections δ vs1 and δ vs2. Compositional techniques that use projection bound a topological property of a system δ by topological properties of a set of projections of δ. Those projections are done on a partition vs1..n of the set of state variables D(δ). For instance, for any vs1..n, EXP(δ) is equal to (and accordingly bounded by) Πvs vs1..n(EXP(δ vs) + 1) 1, i.e. the product of the state space sizes of such a set of projections. In contrast to EXP, the (recurrence) diameter cannot generally be bounded by the (recurrence) diameters of projections (Abdulaziz 2017, Chapter 3, Theorems 1 and 2). However, if there are acyclicities in variable dependencies, there are methods that compose the recurrence diameters of projections to bound on the concrete system s diameter (Baumgartner, Kuehlmann, and Abraham 2002; Rintanen and Gretton 2013). We now review variable dependency and the most recent of those methods from AGN1. Acyclicity in variable dependency has been exploited in previous research by reasoning about the dependency/causal graph (Williams and Nayak 1997; Knoblock 1994). We formally describe that graph, reviewing precisely what is meant by dependency.

Deﬁnition 7 (Dependency). A variable v2 is dependent on v1 in δ (written v1 v2) iff one of the following statements holds: (i) v1 = v2, (ii) there is (p, e) δ such that v1 D(p) and v2 D(e), or (iii) there is a (p, e) δ such that both v1 and v2 are in D(e). A set of variables vs2 is dependent on vs1 in δ (written vs1 vs2) iff: (i) vs1 vs2 = , and (ii) there are v1 vs1 and v2 vs2, where v1 v2.

Deﬁnition 8 (Digraph Quotient). For a digraph G, and a partition P of its vertices V (G), the quotient G/P of G is the digraph with a vertex for each u P. G/P has an edge between any us1, us2 P iff G has an edge between any u1 us1 and u2 us2.

Deﬁnition 9 (Dependency Graph). GD(δ) is a dependency graph of δ, if D(δ) are its vertices and {(u1, u2) | u1 u2 u1, u2 D(δ)} are its edges. A quotient, GVS, of GD(δ) on a partition vs1..n of D(δ) is a lifted dependency graph.

Example 3. Figure 1d shows the dependency graph GD(δ) of δ from Example 1, where self-loops are omitted. Figure 1e has a lifted dependency graph GVS of δ which is the quotient GD(δ)/{vs1, vs2} .

AGN1used the compositional bounding function Nsum, deﬁned via the recurrence below. δ is the system of interest, GVS is a lifted dependency graph of δ used to identify abstract subproblems, and child GVS(vs) denotes the set of children of a set of varaibles vs in GVS, {vs2 | vs2 V (GVS) vs vs2}. The functional parameter b bounds projections and we refer to it as the base case function.

Deﬁnition 10 (Acyclic Dependency Compositional Bound).

N b (vs, δ, GVS) = b(δ vs)(1+ X

c child GVS(vs) N b (c, δ, GVS))

Then, let Nsum b (δ, GVS) = P

vs GVS N b (vs, δ, GVS).

Theorem 1. For any δ with an acyclic lifted dependency graph GVS, d(δ) Nsum rd (δ, GVS).

Example 4. Consider GVS from Figure 1e, and the base case function b. Let Ni denote N b (vsi, δ, GVS) and bi denote b(δ vsi). We have (i) N2 = b2, (ii) N1 = b1 + b1b2, and (iii) Nsum b (δ, GVS) = b1 + b2 + b1b2.

Since previous methods only apply to dependencies with acyclicity, it is an open question as to whether there is a compositional bound on plan lengths better than EXP(δ) for projections not induced by acyclic lifted dependency graphs. In this work we provide a positive answer to that question.

The Traversal Diameter

The traversal diameter is one less than the largest number of states that could be traversed by any path.

Deﬁnition 11 (Traversal Diameter). Let ss(x, π) be the set of states traversed by executing π at x. The traversal diameter is

td(δ) = max x U(δ), π δ |ss(x, π)| 1.

Intuitively, the traversal diameter is a version of the diameter that instead of selecting shortest action sequences that reach the same ﬁnal destination, it selects shortest action sequences that traverse the same states en route to the destination. It should also be clear that the traversal diameter is upper bounded by the state space size.

Example 5. For δ vs1 from Example 2 whose state space is shown in Figure 1b, the traversal diameter is 2.

The most appealing feature of the traversal diameter is that it is an upper bound on the recurrence diameter (and accordingly the diameter) that can be compositionally bounded with projections from arbitrary partitions of the state variables. In other words, unlike other topological properties, it avoids any conditions on the dependencies between the projections used for bounding, as shown in the theorem below.

Theorem 2. For a factored representation δ and a partition vs1..n of D(δ), td(δ) Πvs vs1..n(td(δ vs) + 1) 1.

To prove Theorem 2 we begin by stating the following propositions.

Proposition 1. For a number k, if for every x U(δ) and π δ , |ss(x, π)| k + 1, then td(δ) k.

Proposition 2. For a set of states S, let S vs denote {x vs | x S}. Let sat-pre(x, π) denote that preconditions of every action in π are satisﬁed, if π is executed from x. If sat-pre(x, π), then ss(x, π) vs = ss(s vs, π vs).

Proposition 3. For any partition vs1..n of D(δ), |ss(x, π)| Πvs vs1..n|ss(x, π) vs|.

Perhaps Proposition 3 is the least obvious. Its intuitive meaning is that a set of states is a subset of the cartesian product of its own projections, given that the projection is on a partition of the state variables.

Proof of Theorem 2. Consider x U(δ) and without loss of generality, an action sequence π δ such that sat-pre(x, π). From Deﬁnition 11, for any vs, x vs U(δ vs) and π vs δ vs , we have |ss(x vs, π vs)| 1 td(δ vs). Theorem 2 then follows from Proposition 2, Proposition 3 and Proposition 1.

Optimality of the Compositional Bound The bound in Theorem 2 is optimal in the following sense: any sound compositional bounding function that takes as input (i) projections traversal diameters and (ii) the dependencies between the projections, will produce a bound that is no less than the bound speciﬁed in Theorem 2. In other words this bound cannot be improved except by exploiting more structure than that of the variable dependencies. Since the optimality theorem quantiﬁes over compositional bounding functions , we ﬁrst need to discuss how we formulate such functions. One notion we need to introduce is that of labelled digraphs, which are digraphs whose vertices have labels. For example, a lifted dependency graph is a graph whose vertices are labelled by sets of state variables. For a labelled digraph Gα and a vertex u, the label of

u is denoted by Gα(u). Also, we deﬁne and image operation for labelled digraphs that effectively changes the vertex labels. In particular, the image h LGαM of the function h on the labelled digraph Gα is a graph that has the same vertices and edges as Gα, but with the label of every vertex u changed from Gα(u) to h(Gα(u)). In this setting, one can see the lifted dependency graph as a labelled digraph whose vertices are labelled each with a set of state variables. A compositional bounding function f is a function that takes the projections traversal diameters and the dependencies between the projections and returns an upper bound on the traversal diameter of the entire system. As arguments to f, projections traversal diameters and their dependencies are encoded as a labelled digraph, GN, in which every vertex is labelled by a natural number. This digraph has one vertex per projection and every edge represents a dependency between two projections. Every vertex is labelled by a natural number that is the traversal diameter of the corresponding projection. Theorem 3. For any digraph, GN, with natural number labels, there is a factored system δ such that: (i) Πu V (GN)(GN(u) + 1) 1 td(δ), and (ii) there is a lifted dependency graph GVS for δ, such that GN = TLGVSM, where T(vs) = td(δ vs). The proof is made of three main steps. Firstly, for each given projection traversal diameter m (i.e. m is a label of a vertex u V (GN)) we construct a factored system 4u with traversal diameter m. Those systems are constructed such that: i) their union is a system with a traversal diameter more than f(GN), and ii) they are projections of the ﬁnal construction δ. Secondly, for every dependency from projection 4u1

to 4u2 (i.e. an edge in GN), we construct an action that has preconditions from 4u1 and effects from 4u2. Those actions are supposed to not change the state space of the ﬁnal construction, they only add dependencies corresponding to the edges in GN. Thirdly, we show that the union of the constructed projections and the dependency inducing actions is the required witness δ, i.e. its diameter exceeds f(GN). Before we start the proof, for system δ and states x, y U(δ), let x y denote that there is a π δ such that π(x) = y.

Proof. For u V (GN), let 4u denote the factored system (i.e. set of actions) {(xu 0, xu i ) | 1 i GN(u)} {(xu 0, xu i ) | 1 i GN(u)}. For instance, if for a vertex u, GN(u) = 3, the state space of 4u will look like the one depicted in Figure 2c. Also construct those systems s.t. for u1 = u2 we have D(4u1) D(4u2) = . Fix some u V (GN). Let S(4u) denote the largest connected component in the state space of 4u, which is unique. xu i xu j holds for any xu i , xu j S(4u), thus td(4u) = |S(4u)| 1 = GN(u). Let δ = {(xu1 0 xu2 0 , xu2 1 ) | (u1, u2) E(GN)} S u V (GN) 4u. We now show that δ satisﬁes requirement (i). Again, let S(δ) denote the largest connected component in the state space of δ, which is unique. Since xu i xu j holds for any xu i , xu j S(4u), then x y holds for any x, y S(δ), and therefore there is a path that traverses every member of S(δ). Since for u1 = u2 we have D(4u1)

D(4u2) = , we have |S(δ)| = Πu V (GN)|S(4u)|. Since from we haveΠu V (GN)|S(4u)| = Πu V (GN)(GN(u)+1), then Πu V (GN)(GN(u) + 1) 1 td(δ). To show that δ satisﬁes requirement (ii), consider a relabelling, GVS, of GN, where every vertex u is relabelled by the domain of the system 4u. Recall that δ had the set of actions {(xu1 0 xu2 0 , xu2 1 ) | (u1, u2) E(GN)} as a subset. These actions are constructed such that they add dependency from D(4u1) to D(4u2) in δ iff (u1, u2) E(GN). Accordingly edges of GVS represent the dependencies of δ and accordingly it is a lifted dependency graph of δ. Also since, for u V (GN), δ D(4

u) = 4u, and by construction GN is a relabelling of GVS, and from we have GN = TLGVSM.

Figure 2: Referring to Example 6, (a) is a natural number labelled graph. (b) a lifted dependency graph of the factored system δ from Example 6. (c), (d), (e) are the largest connected components in the state spaces of the systems 4u2,

4u3 and 4u1, respectively. (f) is the largest connected component in the state space of δ.

Example 6. This is an example of the construction from Theorem 3, for the natural number labelled digraph GN in

Figure 2a. In GN there are three vertices u1 (the root), u2, and u3, labelled by the numbers 2, 3, and 2, respectively. We construct three systems, one per vertex, shown in Figures 2c2e. For u2 the constructed system is 4u2 = {(xu2 0 , xu2 1 ), (xu2 0 , xu2 2 ), (xu2 0 , xu2 3 ), (xu2 1 , xu2 0 ), (xu2 2 , xu2 0 ), (xu2 3 , xu2 0 )}. The states are deﬁned as xu2 0 = {v3, v4}, xu2 1 = {v3, v4}, xu2 2 = {v3, v4}, xu2 3 = {v3, v4}. For u3 the constructed system is 4u3 = {(xu3 0 , xu3 1 ), (xu3 0 , xu3 2 ), (xu3 1 , xu3 0 ), (xu3 2 , xu3 0 )}. The states are deﬁned as xu3 0 = {v5, v4}, xu3 1 = {v5, v4} and xu3 2 = {v5, v4}. For u1 the constructed system is

4u1 = {(xu1 0 , xu1 1 ), (xu1 0 , xu1 2 ), (xu1 1 , xu1 0 ), (xu1 2 , xu1 0 )}. The states are deﬁned as xu1 0 = {v1, v2}, xu1 1 = {v1, v2}, and xu1 2 = {v1, v2}. For any xu1 i , xu1 j S(4u1), xu1 i xu1 j holds and accordingly td(4u1) = 2. Similarly, td(4u2) = 3 and td(4u3) = 2. The required witness is δ = {(xu1 0 xu2 0 , xu2 1 ), (xu1 0 xu3 0 , xu3 1 )} 4u1 4u2 4u3, where the actions {(xu1 0 xu2 0 , xu2 1 ), (xu1 0 xu3 0 , xu3 1 )} add to δ dependencies equivalent to the edges of GN, i.e. the dependencies shown in Figure 2b. Also, in the constructed witness, for all states x0, x1 S(δ) (shown in Figure 2f) x0 x1 holds, and accordingly td(δ) = 35.

Computing the Traversal Diameter An important aspect of td is that, unlike the diameter or the recurrence diameter, it can be computed in linear time using Algorithm 1. A principal component of computing the traversal diameter is an algorithm to compute the weight of the weightiest path in acyclic digraphs, where vertices are assigned numerical weights. The weight of a path is the sum of weights of all the vertices that it traverses added to the number of edges comprising it. The weightiest path is computed using the recurrence Smax. Deﬁnition 12 (Weighted Longest Path). For a digraph G, let the function b : V (G) N be a function that assigns a natural number for every vertex in V (G). S is

S b (u, G) = b(u) + max u child G(u)(S b (u , G) + 1)

Then, let Smax b (G) = max u V (G)S b (u, G).

Smax is only well-deﬁned if G is acyclic. The runtime of Smax is linear in the size of V (G), if the values of S for different vertices are memoised and assuming that b is at most of linear complexity. Accordingly if we use Tarjan s (Tarjan 1972) algorithm to compute the strongly connected components, the runtime of Algorithm 1 would be linear in the size of the state space of the given system.

Algorithm 1: TRAVD(δ)

SCC := set of strongly connected components of G(δ) return Smax C (G(δ)/SCC), where C(s) = |s| 1

Theorem 4. TRAVD(δ) = td(δ).

Proof. For notational brevity, let G = G(δ)/SCC, and for a strongly connected component scc, S(scc) = S C (scc, G)

and child(scc) = child G(scc). Since G is a DAG, its vertices can be topologically ordered in a list l SCC. Firstly, we prove TRAVD(δ) td(δ). We show that for any strongly connected component scc G there is an action sequence π scc δ and a state xscc scc, such that S(scc) |ss(xscc, π scc)| 1, which from Deﬁnitions 11 and 12, implies TRAVD(δ) td(δ). We prove this by induction on l SCC. The base case, l SCC = [], is straightforward. For the step case l SCC = scc :: l SCC,1 and for any scc l SCC, there is a state x scc and an action se-

quence π δ where S(scc ) |ss(x , π )| 1. Since scc is a strongly connected component of states in G(δ), then there is π scc δ and a state xscc scc, where π scc traverses exactly all the states in scc, if executed at xscc scc, i.e. ss(xscc, π scc) = scc. We have two cases:

Case 1 (child(scc) = ). From Deﬁnition 12, S(scc) = |scc| 1 = |ss(xscc, π scc)| 1 holds for this case. Accordingly the required witness π scc is the same as π scc.

Case 2 (child(scc) = ). Let sccmax be a strongly connected component where scc child(scc). S(scc ) S(sccmax). Because sccmax child(scc) we have sccmax l SCC, and accordingly from the inductive hypothesis there are xmax sccmax and π max δ such that S(sccmax) |ss(xmax, π max)| 1.( ) Also, because sccmax child(scc) and since both scc and sccmax are strongly connected components, there must be π δ , where π scc π (xscc) = xmax. 2 We now show that π scc = π scc π π max is the required witness. First, it is easy to see that ss(xscc, π scc) ss(xmax, π max) ss(xscc, π scc). Since sccmax child(scc), then ss(xmax, π max) is disjoint with scc. Accordingly |ss(xscc, π scc)| + |ss(xmax, π max)| |ss(xscc, π scc)|. From this, ( ), and Deﬁnition 12 we have S(scc) |ss(xscc, π scc)| 1.

Secondly, we prove td(δ) TRAVD(δ) by showing that for any scc G, xscc scc, and π scc δ , we have |ss(xscc, π scc)| 1 S(scc). Our proof is again by induction on the list l SCC. The base case, l SCC = [], is straightforward. The step case l SCC = scc :: l SCC, and

we have that for any scc l SCC, x scc , and π δ ,

|ss(x , π )| 1 S(scc ) holds. We have two cases:

Case 1 (ss(xscc, π scc) scc). Since ss(xscc, π scc) scc then |ss(xscc, π)| |scc|. From Deﬁnition 12, we know that |scc| 1 S(scc), and accordingly |ss(xscc, π scc)| 1 S(scc).

Case 2 ( ss(xscc, π scc) scc). Since ss(xscc, π scc) scc, then there are π scc, π, and π child such that:

1For a list l, h :: l is l with the element h appended to its front. 2For two lists l1 and l2, l1 l2 denotes their concatenation.

(i) π scc = π scc π :: π child, (ii) ss(xscc, π scc) scc, and (iii) letting xchild = π( π scc(xscc)), xchild sccchild holds, for some sccchild child(scc). Using the same argument as the last case, we have |ss(xscc, π scc)| |scc|.(*) Since xchild sccchild, and from the inductive hypothesis, we have that |ss(xchild, π child)| 1 S(sccchild). Then using (*) and since ss(xchild, π child) and scc are disjoint, we have |ss(xscc, π scc)| 1 |scc| + S(sccchild). From Deﬁnition 12, we have |scc| + S(sccchild) S(scc) and accordingly |ss(xscc, π scc)| 1 S(scc).

Example 7. Consider the projection δ vs1 of δ from Example 2 as input to Algorithm 1. The ﬁrst step in Algorithm 1 is to compute the SCCs of the state space G(δ). G(δ) is shown in Figure 1b, and it has three strongly connected components, thus SCC := {{v1v2, v1v2}, {v1v2}, {v1v2}}. Those connected components induce the quotient of the state space shown in Figure 1f. Next, the algorithm computes Smax C (G(δ)/SCC). We have S C ({v1v2}) = C({v1v2}) = 0, and S C ({v1v2}) = C({v1v2}) = 0. S C ({v1v2, v1v2}) = C{v1v2, v1v2}+max{S C ({v1v2}), S C ({v1v2})}+1 = 1+0+1 = 2. Thus, Smax C (G(δ)/SCC) = 2, which is the traversal diameter of the state space of δ vs1 and the value returned by Algorithm 1.

Tightness of the Traversal Diameter Having a product of the traversal diameters of all projections as a compositional bound may not seem like a practically helpful bound. However, it is a substantial improvement over what can currently be done in the case when there is not a non-trivial acyclic lifted dependency graph. When given a set of projections without acyclicity in the dependencies between them, existing compositional bounding approaches use the product of the projected state space sizes EXP(δ) as a bound (Rintanen and Gretton 2013, AGN1, and AGN2). Using the product bound of Theorem 2 is a substantial improvement over that because, as shown in the next theorem, the traversal diameter can be exponentially smaller than the size of state space.

Theorem 5. There are inﬁnitely many factored systems whose traversal diameters are exponentially smaller (in the number of state variables) than the size of their state spaces.

Proof. For an arbitrary number n N, we construct a system whose state space size is a factor of n more than its traversal diameter. Let xi, for 0 i n, be n + 1 states. Consider the system {(x0, xi) | 1 i n}. The traversal diameter of this system is 1 since, the only possible transitions are from state x0 to a state xi, for 1 i n. However the system s state space has at least n + 1 states.

Example 8. δ vs2 from Example 2 whose state space is shown in Figure 1c is an example of the above construction with n = 3. We can take x0, x1, x2, and x3 to be v3v4, v3v4, v3v4, and v3v4, respectively.

Practical Bounding Using the Traversal Diameter

In the last section, we laid down a theoretical foundation suggesting that the traversal diameter could be successfully used for compositional upper bounding. A schema for algorithms utilising that theoretical framework to compositionally bound the traversal diameter of a system δ is

ARB(δ) = ch vs1..n VS1..nΠvs vs1..n(TRAVD(δ vs) + 1) 1

Above, VS1..n denotes the set of all partitions of the set of state variables D(δ), and ch denotes a function that chooses one partition vs1..n to use for compositional bounding. To fully specify the bounding algorithm ARB we need to determine the choice of the partition of D(δ) using which we obtain the projections. Optimally, the function ch would be instantiated with the function min that would choose the partition which results in the smallest bound. However, since the size of VS1..n is intractable, min would be an impractical solution. We adopt a practically feasible approach used by AGN2: we take the situation where D(δ) models all assignments in the SAS+ model generated using Fast Downward s preprocessing step (Helmert 2006), and choose ch to return a partition vs1..n s.t. each equivalence class in vs1..n has elements that model all the assignments of exactly one SAS+ state variable. Now that we have fully speciﬁed ARB we compare it to other bounding algorithms. We experimentally evaluate different bounding algorithms on problems from previous International Planning Competitions (IPC), and the unsolvablity IPC, open Qualitative Preference Rovers benchmarks from IPC2006 (to which we refer as NEWOPEN) and the hotel-key protocol veriﬁcation problem from AGN2. Our experiments were conducted on a uniform cluster with time and memory limits of 30minutes and 8GB, respectively. The ﬁrst two columns in Table 1 show that compared to Nsum EXP , ARB fails to compute bounds tighter than 109 in most domains. That is because when there is branching in the dependency graph, Nsum computes a bound that has additive terms like the ones in Example 4, while on the other hand, ARB always returns a bound that is the product of the projections traversal diameters. Now, recall that Theorem 5 predicts the possibility for exponential improvement in the computed bound if, instead of EXP, we use ARB to bound a system. This suggests another utilisation of ARB: to use it as a base case function for Nsum instead of EXP. This way ARB will be only used to bound projections which cannot be further decomposed by Nsum, i.e. projections whose variable dependencies are strongly connected. Indeed, using ARB as a base case function improves the computed bounds in 71% of the problems, and the improvement is at least 50% in 66% of the cases. The second row in Table 1 gives an overview of the improvement in the bounds computed by Nsum ARB compared to Nsum EXP for different domains. A more detailed comparison is in the top plot of Figure 3.

The Traversal Diameter and State Space Acyclicity The construction used in the proof of Theorem 3 suggests that the bounds computed by ARB are better than those computed by EXP only if the projections of the system have acyclicity and branching in their state space. In fact the following proposition holds. Proposition 4. If G(δ) is strongly connected, then td(δ) = EXP(δ). This begs the question of whether ARB can somehow be combined with the algorithm proposed by AGN2, which also exploits acyclicity in the state space, to compute tighter bounds and better system decompositions. We ﬁrst review the approach of AGN2. A critical element of their approach is a system abstraction to which they refer as a snapshot. It models the system when we ﬁx the assignment of a subset of the state variables, removing actions whose preconditions or effects contradict that assignment. Deﬁnition 13 (Snapshot). For states x and x , let agree(x, x ) denote |D(x) D(x )| = |x x |, i.e. every variable that is in the domains of both x and x has the same assignment in x and x . The snapshot of δ at a state x is

δ| x= {(p, e) | (p, e) δ agree(p, x) agree(e, x)} D(x)

where D(x) denotes D(δ) \ D(x). Based on snapshots, and given a system δ, a set of variables vs, and a base case function b, AGN2 deﬁned a method Smax b (vs, δ).3 That method computes the weightiest path in the state space G(δ vs), where the weight of a state x is b(δ| x). It is only deﬁned if G(δ vs) is acyclic. Combining Smax and Nsum, AGN2 suggested Algorithm 2 as a hybrid approach to exploit acyclicities in state spaces and dependencies. In HYB, vs1..n is a partition of D(δ), and ac(vs1..n) is a member of vs1..n s.t. the projection δ ac(vs1..n) has a non-trivial acyclic state space. HYB interleaves the functions Nsum and Smax. It only calls Smax if the given system s dependencies are strongly connected and δ has acyclic projections on members of vs1..n. If both Nsum and Smax cannot be called, HYB uses EXP as a base case function.

Algorithm 2: HYB(δ, vs1..n)

SCC := set of strongly connected components of GD(δ) GVS := GD(δ)/SCC if 2 |V (GVS)| return Nsum HYB( , vs1..n) (δ, GVS) if vsi = ac(vs1..n) vsi := ac(vs1..n) return Smax HYB( , vs1..n \ {vsi}) (vsi, δ) return EXP(δ)

Example 9. From Examples 1 and 2, consider the system δ and the partition vs1..n = {vs1, vs2} of its state variables. The SCCs of the dependency graph of δ are vs1

3We overload the same symbol used in Deﬁnition 12

and vs2, and thus the lifted dependency graph GVS computed by HYB is the one in Example 3. Accordingly, HYB will return Nsum HYB( , vs1..n) (δ, GVS). Then we have that Nsum HYB( , vs1..n) (δ, GVS) = HYB1 + HYB2 + HYB1HYB2, where HYBi = HYB(δ vsi, vs1..n) for i {1, 2}. Since δ vs2 has the acyclic state space shown in Figure 1c we have HYB2 = Smax HYB( , vs1) (vs2, δ vs2) = 1. Since the state space of δ vs1 is not acyclic, HYB1 = EXP(δ vs1) = 3. Thus, HYB(δ, vs1..n) = 1+3+1 3 = 7. Since HYB already exploits state space acyclicity using Smax, the main question now is whether using ARB as a base case function for HYB instead of EXP can improve the computed bounds. The short answer to that question is: yes, bounds computed by HYB using ARB as a base case function are better in 68% of the problems compared to those computed with EXP as a base case, and the improvement is at least 50% in 71% of the cases. The third column of Table 1 and the bottom plot of Figure 3 show a ﬁne-grained comparison between the bounds. To understand the improvement in the computed bounds, recall that if the dependency graph has one SCC, HYB will pick one vsi from vs1..n, s.t. the state space of δ vsi is acyclic. Then HYB uses Smax to decompose δ into multiple abstractions: the projection δ vsi and the snapshots of δ on the different states in U(δ). Then Smax calls HYB recursively on each of the snapshots of δ, with vsi removed from vs1..n. This is repeated until the state space of the projection on each remaining member of vs1..n is not acyclic. Then the base case function is called to bound the projection on

Figure 3: Top (resp. bot.): bounds computed by Nsum (resp. HYB) when EXP (vert.) is base case function vs ARB (hor.).

Table 1: Col. 1: the domain name and the number of problems in it. Col. 2: the number of problems for which ARB computed a bound less than 109. Col. 3 (resp. 4) has four numbers: (i) problems for which Nsum EXP (resp. HYB EXP ) computed a bound less than 109 (ii) problems for which Nsum ARB (resp. HYB ARB ) computed a bound less than 109 (iii) problems for which the bound by Nsum ARB (resp. HYB ARB ) is less than the bound by Nsum EXP (resp. HYB EXP ) (iv) problems for which the bound by Nsum ARB (resp. HYB ARB ) is less than half the bound by Nsum EXP (resp. HYB EXP ).

the remaining members of vs1..n. However, as shown in the next example, if a projection s state space is not acyclic, its traversal diameter can still be much tighter than the size of its state space. This will lead to much tighter bounds computed by HYB if it uses ARB as a base case function instead of EXP.

Example 10. Consider the computation in Example 9. If ARB is used as a base case function, HYB1 = ARB(δ vs1, vs1..n) = TRAVD(δ vs1) = 2 (for the evaluation of TRAVD(δ vs1) see Example 7). Thus HYB(δ, vs1..n) = 1 + 2 + 1 2 = 5.

Using the Bounds To Compute Plans AGN2 showed that when the bounds computed by HYB, with EXP as a base case function, are used as a horizon for the SAT-based planner Madagascar MP (Rintanen 2012), the coverage of MP substantially increased. Indeed, it solved satisﬁable and un-

satisﬁable planning problems that other state-of-the-art planners could not solve. We now study the improvement in the coverage of MP if we use as horizons the bounds computed by HYB when ARB is the base case. Compared to using EXP as a base case, ARB increases the coverage by 234 for solvable problems. Those problems come from the domains: NEWOPEN (221 problems), ROVER (7 problems), SATELLITE (5 problems), and TPP (1 problem). Also, using ARB as a base case for HYB allows MP to prove the unsolvability of an additional 4 problems from the domain NEWOPEN and 52 problems from the domain HOTELKEY, that it could not solve when EXP is used as a base case function.

Conclusions and Future Work

We contributed a novel compositional upper bounding approach in planning. Our technique exposes problems with a relatively wide variety of dependency structures to upper bounding. Previous approaches only apply to a limited class of problems that have a branching 1-way state variable dependency structure. Our analysis treats a much broader class of problems, with 2-way dependencies. Our new approach, however, is most useful when combined with other existing compositional bounding techniques, where it leads to substantial improvement in the computed bounds. We use it to decompose problem abstractions produced using the other compositional bounding techniques when those abstractions have bidirectional dependencies. An open problem is to devise a method to practically decompose large concrete problems with strongly connected dependencies instead of only small abstractions produced by other compositional algorithms. Also, investigating the effect of the partition of the state variables used to decompose problems on the value of computed bounds is an interesting avenue for future research.

Acknowledgements We thank Dr. Charles Gretton, Dr. Michael Norrish, Lars Hupel and Simon Wimmer for proofreading parts of this paper, and Lars Hupel for helping me set up the experiments. We also thank Prof. Tobias Nipkow and the German Research Foundation for funding that facilitated this work through the DFG Koselleck Grant NI 491/16-1.

Abboud, A.; Williams, V. V.; and Wang, J. 2016. Approximation and ﬁxed parameter subquadratic algorithms for radius and diameter in sparse graphs. In Proceedings of the twenty-seventh annual ACM-SIAM symposium on Discrete Algorithms, 377 391. SIAM. Abdulaziz, M.; Gretton, C.; and Norrish, M. 2015. Veriﬁed Over-Approximation of the Diameter of Propositionally Factored Transition Systems. In Interactive Theorem Proving. Springer. 1 16. Abdulaziz, M.; Gretton, C.; and Norrish, M. 2017. A State Space Acyclicity Property for Exponentially Tighter Plan Length Bounds. In International Conference on Automated Planning and Scheduling (ICAPS). AAAI.

Abdulaziz, M. 2017. Formally Veriﬁed Compositional Algorithms for Factored Transition Systems. The Australian National University. Aingworth, D.; Chekuri, C.; Indyk, P.; and Motwani, R. 1999. Fast estimation of diameter and shortest paths (without matrix multiplication). SIAM Journal on Computing 28(4):1167 1181. Alon, N.; Galil, Z.; and Margalit, O. 1997. On the exponent of the all pairs shortest path problem. Journal of Computer and System Sciences 54(2):255 262. Baumgartner, J.; Kuehlmann, A.; and Abraham, J. 2002. Property checking via structural analysis. In Computer Aided Veriﬁcation, 151 165. Springer. Biere, A.; Cimatti, A.; Clarke, E. M.; and Zhu, Y. 1999. Symbolic model checking without BDDs. In TACAS, 193 207. Chan, T. M. 2010. More algorithms for all-pairs shortest paths in weighted graphs. SIAM Journal on Computing 39(5):2075 2089. Chechik, S.; Larkin, D. H.; Roditty, L.; Schoenebeck, G.; Tarjan, R. E.; and Williams, V. V. 2014. Better approximation algorithms for the graph diameter. In Proceedings of the Twenty-Fifth Annual ACM-SIAM Symposium on Discrete Algorithms, 1041 1052. Society for Industrial and Applied Mathematics. Fredman, M. L. 1976. New bounds on the complexity of the shortest path problem. SIAM Journal on Computing 5(1):83 89. Helmert, M. 2006. The Fast Downward planning system. Journal of Artiﬁcial Intelligence Research 26:191 246. Kautz, H. A., and Selman, B. 1992. Planning as satisﬁability. In ECAI, 359 363. Knoblock, C. A. 1994. Automatically generating abstractions for planning. Artiﬁcial Intelligence 68(2):243 302. Pardalos, P. M., and Migdalas, A. 2004. A note on the complexity of longest path problems related to graph coloring. Applied Mathematics Letters 17(1):13 15. Rintanen, J., and Gretton, C. O. 2013. Computing upper bounds on lengths of transition sequences. In International Joint Conference on Artiﬁcial Intelligence. Rintanen, J. 2012. Planning as satisﬁability: Heuristics. Artiﬁcial Intelligence 193:45 86. Roditty, L., and Vassilevska Williams, V. 2013. Fast approximation algorithms for the diameter and radius of sparse graphs. In Proceedings of the Forty-Fifth Annual ACM Symposium on Theory of Computing, 515 524. ACM. Tarjan, R. 1972. Depth-ﬁrst search and linear graph algorithms. SIAM Journal on Computing 1(2):146 160. Williams, B. C., and Nayak, P. P. 1997. A reactive planner for a model-based executive. In International Joint Conference on Artiﬁcial Intelligence, 1178 1185. Morgan Kaufmann Publishers. Yuster, R. 2010. Computing the diameter polynomially faster than APSP. ar Xiv preprint ar Xiv:1011.6181.