# schematic_invariants_by_reduction_to_ground_invariants__371a6ac6.pdf

Schematic Invariants by Reduction to Ground Invariants

Jussi Rintanen

Department of Computer Science Aalto University, Helsinki, Finland

Computation of invariants, which are approximate reachability information for state-space search problems such as AI planning, has been considered to be more scalable when using a schematic representation of actions/events rather than an instantiated/ground representation. A disadvantage of schematic algorithms, however, is their complexity, which also leads to high runtimes when the number of schematic events/actions is high. We propose algorithms that reduce the problem of ﬁnding schematic invariants to solving a smaller ground problem.

Introduction Invariants are a form of approximate reachability information for state-space search problems (Blum and Furst 1997; Gerevini and Schubert 1998), which can be used as a pruning method for search algorithms for planning (Rintanen 2012), and also have a close connection to admissible heuristics used with informed search (Rintanen 2006; 2008). Many of the early algorithms used a ground representation of actions (Blum and Furst 1997; Rintanen 1998). The number of ground instances of schematic actions can be impractically high. Also, invariants for action sets induced by a small set of schematic actions can often be compactly represented as a small number of schematic invariants. This motivates the introduction of invariant algorithms that directly work with the schematic action/event representation and produce invariants in a schematic form (Gerevini and Schubert 1998; Rintanen 2000). In their most general forms, however, such algorithms are quite complex to implement and to prove correct, and there is also a signiﬁcant performance penalty for handling a schematic representation. This performance penalty makes schematic algorithms uncompetitive when the number of schematic actions is high but the number of ground instances is low. In such cases algorithms working with the grounded representation can dramatically outperform schematic algorithms.

Also afﬁliated with Grifﬁth University, Brisbane, Australia, and the Helsinki Institute for Information Technology, Finland. This work was funded by the Academy of Finland (Finnish Centre of Excellence in Computational Inference Research COIN, 251170). Copyright c 2017, Association for the Advancement of Artiﬁcial Intelligence (www.aaai.org). All rights reserved.

In this work we devise algorithms that share the beneﬁts of both approaches: the algorithms are simple and efﬁcient to implement (similar to invariant algorithms based on grounding), and scale well even when the number of ground instances is high (similarly to schematic algorithms.) Careful implementation can ensure that runtimes are never (substantially) higher than corresponding ground algorithms. Our novel idea is to devise hybrid algorithms, which perform the basic invariance tests with a ground method, but ground the actions and formulas only with respect to a small number of objects, roughly matching what takes place in schematic algorithms which partially instantiate schematic actions and formulas through uniﬁcation and substitution operations. The challenge here is to keep the number of objects as small as possible to guarantee efﬁciency and scalability but not too small, to guarantee correctness and to identify as many and as strong invariants as possible. This idea is, in effect, exploiting the structural symmetry of the state space generated by schematic actions. The set of schematic candidate invariants obtained from the initial state (as opposed to the (ground) facts holding in the initial state), is symmetric, and the schematic formulas (approximately) representing the sets of states reachable by a given number of steps are similarly symmetric in the sense that if φ is a ground instance of a schematic formula, then any permutation of its objects that respects typing also is. The main outcome from the work is a substantial improvement in the scalability of the invariant algorithm for temporal planning by Rintanen (2014). That algorithm ﬁnds broad classes of invariants and can be easily adapted to a wide range of temporal modeling languages, but its scalability needs to be improved because of the time complexity of its satisﬁability tests. In earlier work, Smith & Weld (1999) extended Blum & Furst s (1997) planning graph method to temporal planning, but similarly to Rintanen (2014) the method works with ground actions and has reduced scalability, and additionally, it is deﬁned for a limited temporal language only. Bernardini & Smith (2011) proposed a schematic algorithm with a very good scalability, but, it ﬁnds at-most-one invariants only, and is deﬁned for a syntactically limited modeling language with no easy avenues to generalization. At-most-one invariants have limited utility with expressive modeling languages that support multi-valued (not only Boolean) discrete state variables.

Proceedings of the Thirty-First AAAI Conference on Artificial Intelligence (AAAI-17)

Background In the presentation we only consider a simple typed schematic language for expressing actions and invariants.1

Deﬁnition 1 (Types) Let O be a set of objects. Let there be a ﬁnite set T of types, and to each type t T a non-empty set D(t) O of objects is associated by the domain function D : T O.

The objects of different types do not need to be disjoint, but in this work we assume that if D(t) D(t ) = , then either D(t) D(t ) or D(t ) D(t).

Deﬁnition 2 (Terms) Let V be a set of schema variables and O a set of objects. Terms (over O and V ) are objects o O and variables v V . Each variable has a type τvar(v) T.

Deﬁnition 3 (Predicates) Let P be a set of predicate symbols. Each predicate p P has arity ar(p) N and an associated type τpre(p) T ar(p), the latter given by the typing function τpre.

Deﬁnition 4 (State Variables) Let p P be a predicate symbol of arity n = ar(p) and of type τpre(p) = (t1, . . . , tn). Then schematic state variables are of the form p(s1, . . . , sn) where each si is either an object o D(ti) or a variable v with τvar(v) = ti. The set gnf(P, τpre, D) of (ground) state variables consists of all p(o1, . . . , on) such that p P, ar(p) = n, and oi D(ti) where τpre(p) = (t1, . . . , tn).

In this work we only consider Boolean state variables, like is common in classical planning, but clearly we could consider any numeric and multi-valued types just as well.

Deﬁnition 5 (States) Let P be a set of predicates and D a domain function. A state is a mapping from gnf(P, τpre, D) to {0, 1}, indicating the truth-value of every state variable.

Deﬁnition 6 (Schematic Formulas) Let O be a set of objects, V a set of variables, and P a set of predicates with arities ar(p) for every p P. The following are schematic formulas over O and V .

1. schematic state variables p(s1, . . . , sn) over V and O 2. φ1 φ2, if φ1 and φ2 are schematic formulas 3. φ1 φ2, if φ1 and φ2 are schematic formulas 4. φ, if φ is a schematic formula

Deﬁnition 7 (Schematic Effects) Let p(s1, . . . , sn) be a schematic state variable. Then p(s1, . . . , sn) and p(s1, . . . , sn) are schematic effects.

Deﬁnition 8 (Schematic Actions) A schematic action over O and V is a pair c, e where

c is a schematic formula over O and V , and e is a set of schematic effects over O and V .

We deﬁne prec( c, e ) = c.

1Extensions to more expressive languages are possible. In our implementations, e.g. numeric variables are currently handled by eliminating them before invariant synthesis.

Deﬁnition 9 A problem instance in planning Π = O, T, D, P, τpre, A, I consists of a ﬁnite set O of objects, a ﬁnite set T of types, a domain function D, a ﬁnite set P of predicates, a typing function τpre, a ﬁnite set A of schematic actions over O and V , and an initial state I.

We do not need goals, as our interest is in reachable states, not ﬁnding particular action sequences.

Deﬁnition 10 Candidate invariants are schematic formulas (with free variables) of the forms

χ (l1 l2) χ l1

where χ is a (possibly empty) conjunction of inequalities x = x where x and x are schema variables referring to objects, and the li are (Boolean) schematic state variables or negated schematic state variables (literals).

Example 1 The formula in(p, b) outdoors(p) says that an object cannot be simultaneously inside a building and outdoors, and b1 = b2 ( in(p, b1) in(p, b2)) that it cannot be simultaneously inside two different buildings.

Deﬁnition 11 (Substitutions) For sets V of schema variables and sets O of objects, a function σ : V V O is a substitution.

Deﬁnition 12 (Application of Substitutions) For formulas φ, (schematic) actions a, and other syntactic objects, we deﬁne φσ and aσ as the syntactic objects respectively obtained from φ and a by replacing every occurrence of v V by σ(v).

Deﬁnition 13 (Substitution Composition) Let V and Q be sets of schema variables and O a set of constant symbols (object names). Let σ : V V O and σ : V Q O be substitutions. Then σσ : V Q O is the substitution deﬁned by σσ (v) = σ (σ(v)) (also denoted by σ σ.)

Invariants from Limited Grounding Earlier works can be divided to those that ground all schematic actions (Blum and Furst 1997; Rintanen 1998; 2008), and to those that work with ungrounded actions (Gerevini and Schubert 1998; 2000; Edelkamp and Helmert 2000; Rintanen 2000; Lin 2004). The most general algorithms from both categories are at least in some cases slow. The ground algorithms are slow when there are thousands of ground actions or more. Schematic algorithms are slow when the number of schematic actions is high (sometimes even just some dozens or hundreds) or the actions are complex, even when the number of ground instances is low. Ground algorithms are easier to implement efﬁciently, whereas handling schematic actions can be quite complicated due to the necessity of using concepts such as substitution and uniﬁcation, and the far bigger effort in implementing these very efﬁciently.

This suggests combining the strengths of the two approaches: algorithms that generate schematic invariants only, by means of ground instances of actions, but without generating all of the ground instances. We show that when the goal is to produce schematic invariants (which might not cover all invariants, or not even all invariants that could be identiﬁed with an algorithm working on the ground action set), instead of producing all ground instances of schematic actions, it is sufﬁcient to produce a substantially smaller set of ground instances. We need to make sure that this approach is correct and ﬁnds enough invariants to be useful. First note that there can never be too many objects to instantiate the schematic actions and too many ground instances.2

Lemma 1 Assume a formula φ is an invariant of a problem instance Π. Let Π be a problem instance such that 1. Π has the same schematic actions, 2. O O , and 3. I(x) = I (x) for all state variables x of Π. Then any schematic formula φ for which some ground instances are not invariants of Π, also has ground instances w.r.t. Π that are not invariants of Π .

Proof: Consider a reachable state of Π that falsiﬁes a ground instance of φ. Let π be an action sequence that reaches that state. Since all these actions are also ground actions of Π , and the initial state of Π is included in the initial state of Π , also this action sequence reaches a state that falsiﬁes a ground instance of φ in the state-space of Π .

Increasing the number of objects, therefore, never leads to identifying too many invariants, which are not invariants of the original problem instance. Decreasing the number of objects, conversely, does lead to more invariants, which might not hold for the original problem instance.

Example 2 Consider the blocks world. If there is only one block, then on(x,y) is an invariant.

Hence, in this work our main goal is to ﬁnd lower bounds on the number of objects so that, even with the reduced object sets, the schematic invariants found also hold for the original (unreduced) problem instance. Consider an invariant P(x, y) Q(y, z), with x, y and z all having the same type. We consider ﬁve cases: the ﬁrst is x = y = z, the second is that all are different, and the remaining three are when one of x = y, y = z and x = z holds. These cases can be obtained by instantiating x, y, z with a, b and c in ﬁve different ways. This makes it seem that it might be sufﬁcient to instantiate a candidate invariant in all possible ways with as many objects as there are variables in the candidate invariant. If the variables were of different and disjoint types, then the number of objects of each type would be analogously the number of variables of that type, as equality between variables of different types cannot hold.

2The result doesn t hold for some other forms of schematic actions, for example ones that include existential quantiﬁcation in preconditions. Such a precondition could explicitly require that there are at most n different objects.

Next we formalize these ideas, and then apply them to a class of invariants algorithms based on ﬁxpoint iteration and satisﬁability tests. Schematic actions can directly refer to named objects, which we call ﬁxed, as they occur in all ground instances of the schematic action, and might not be interchangeable with non-ﬁxed objects. The invariant algorithm we apply our results ﬁrst to for classical planning, based on a syntactic regression operation and satisﬁability tests (Rintanen 2008). The regression operation regra(φ) produces for an action a and formula φ a weakest precondition that has to be satisﬁed for φ to hold after a. For grounded actions a = (c, e) from Deﬁnition 8 where c is a ground formula and e is a set of state variables, regra(φ) is deﬁned as the formula c φ where φ is obtained from φ by replacing x by the constant (for true) if x e and by constant (for false) if x e. An action a is relevant for φ if the effects of a and φ share a state variable. Let prmst(a) be the number of schema variables of type t in action a. Let prmst(p) be the number of terms of type t in schematic atomic formulas with predicate p. Next we give a lower bound on the number of objects of each type that are needed in computations of invariants by partial grounding, when the invariants are disjunctions of at most N literals. This is stated in Lemma 2, for the number of objects of a given type in the formula to test if a candidate invariant holds. Intuitively, the formula indicates the maximum possible number of instantiated objects of type t in the candidate invariant minus the occurrences eliminated from it by the action plus the occurrences in that action.

Deﬁnition 14 (Limited Instantiation) For a given action set A, predicate set P, domain function D, type t, and integer N 1, deﬁne

LN t (A, P) = max(maxa A prmst(a), maxp P prmst(p)) +(N 1) (maxp P prmst(p))

Lemma 2 Let a be a ground instance of a schematic action in A and φ a ground instance of a schematic disjunction of N literals, both formed from state variables with predicates from P. Assume a is relevant for φ. Then there are at most LN t (A, P) different non-ﬁxed objects of type t in regra(φ).

The following theorem shows that we can always limit to domains of small size, limited by LN t (A, P) and the number of ﬁxed objects, without sacriﬁcing correctness: if a (schematic) candidate invariant gets falsiﬁed with a ground action set that contains all ground actions (as on line 5 in Figure 1), then it will be falsiﬁed also with the (possibly much smaller) set.

Theorem 3 Let A be a set of schematic actions, D a domain function for the types T, D a domain function such that for every t T, either D (t) = D(t) or

1. D (t) D(t), 2. |D (t)| LN t (A, P), 3. D (t) includes all ﬁxed objects of type t, and 4. D (t0) D (t1) iff D(t0) D(t1), for all {t0, t1} T.

Let C be a set of schematic formulas (without occurrences of objects), CD the ground instances of C w.r.t. D, and CD the ground instances of C w.r.t. D . Let φ be a schematic disjunction of at most N literals. Assume CD {regraσ(φσ)} is satisﬁable for some ground instance aσ of a A and a ground instance φσ of φ w.r.t. D, for some σ : V O, and aσ is relevant for φσ. Then CD {regraσ (φσ )} is satisﬁable for some σ with range of σ included in D .

Proof: Let v be a valuation such that v |= CD {regraσ(φσ)}. We will construct a substitution σ and then a valuation v such that v |= CD {regraσ (φσ )}. Let R(t), for all t T, be any subset of D(t) of same cardinality as D (t) that includes all objects of type t in regraσ(φσ). Such sets R(t) exist because of the assumption that |D (t)| LN t (A, P) and because of Lemma 2. Let R =

t T R(t). Let π a bijective mapping π : R t T D (t) such that for all o R and t T, π(o) D (t) iff o D(t). Such a mapping exists because the cardinalities of R(t) and D (t) are the same. Deﬁne σ = σπ. Deﬁne a valuation v by v (π(x)) = v(x) for every state variable x occurring in aσ and φσ. Clearly, for every such x, v |= x iff v |= π(x), and hence v |= regrσ (φσ ). It remains to show that v |= CD . Take any ψ CD . Now ψ = π(ψ) for some ψ CD because CD contains all ground instances of C w.r.t D, and π(ψ) CD CD. By assumption, v |= ψ. Since ψ = π(ψ), also v |= ψ .

Notice that the theorem does not apply to very small domains where the number of objects of a given type is lower than the number of parameters of that type in the actions or invariants, meaning that two or parameters have to be instantiated with the same object. Of course, in these cases the number of ground instances of actions and formulas is small anyway, even without reducing the number of objects. What is remarkable in Theorem 3 is that LN t (A, P) is independent of the number of objects in the problem instance. It only depends on the number and size of the actions, and the length N of invariant formulas sought (which is in practice constant N = 2). This is why the approach is scalable to large instances obtained by increasing the number of objects while the number of schematic actions stays small. Theorem 3 can be used in an algorithm that represents (candidate) invariants as schematic formulas, a modiﬁcation of the algorithm given by Rintanen (2008), see Figure 1. The set A of actions consists of, instead of all possible ground actions, only of a subset induced by the small domains D (t), t T as indicated in Theorem 3. On line 1, those schematic formulas of some limited syntactic form3 that are true in the initial state are identiﬁed. On line 6 a schematic formula c that cannot be guaranteed to hold in all reachable states because some ground instance cσ could possibly become false is replaced with a set weaken(c) of logically weaker formulas c l. Or if c was already of the

3For example, disjunction of two literals, possibly with some equality constraints, as in Example 1.

1 C := schematic formulas true in the initial state; 2 repeat 3 C0 := C; 4 foreach a A and c C do 5 if C0 {regra( cσ)} SAT for some cσ 6 then C := (C\{c}) weaken(c); 7 end 8 until C = C0; 9 return C;

Figure 1: Algorithm for invariants for classical planning

weakest possible form, weaken(c) = . After running the algorithm, the schematic invariants C can be grounded according to the original domain function, or used as is with the original problem instance.

Using Ground Algorithm (Almost) As Is Next we consider another way of using limited grounding, which relies even more on the original algorithm which uses both ground actions and ground formulas. The cost of simplicity in this case is a (moderate amount) of additional computation. The idea is to compute ground invariants with a limited set of ground state variables, and only in the end extract the schematic invariants from the set of ground invariants. The computation is more expensive than that of Figure 1, but as the ground action and ground invariant sets are still small, it is still cheap enough to be practically useful. The only modiﬁcation to the ground algorithm is that the set of literals describing the initial state is replaced by ground instances (with limited grounding) of all schematic formulas (of a given form) that are true in the initial state of the original problem. After the ground algorithm terminates, schematic invariants for the original problem are extracted from the ground invariants obtained. This idea is based on the following property.

Lemma 4 (Invariance Modulo Renaming) For all rounds of the proposed algorithm, if φσ C for some substitution σ , then φσ C for any other substitution such that

1. for all x and ﬁxed objects h, σ(x) = h iff σ (x) = h, and 2. for all x and y, σ(x) = σ(y) iff σ (x) = σ (y).

At all steps of the algorithm, permuting the non-ﬁxed objects in any formula in the current candidate invariant set yields another member in the set.

Example 3 Assume h is the only ﬁxed object, and there is only one type to which a, b, c and h all belong. If p(a, a, a) is a ground invariant, then p(x, x, x) is a schematic invariant. If p(a, b, c) is a ground invariant, then (x = y) (x = z) (y = z) p(x, y, z) is a schematic invariant. If p(a, b, h) is a ground invariant, then p(x, y, h) is a schematic invariant.

Temporal Planning This section generalizes the previous ideas to temporal planning, which is our main application: the cost of computing temporal invariants is much higher than that of classical invariants, and therefore the scalability to large instances is a

1 C := {x X|I |= x} { x|x X, I |= x}; 2 repeat 3 C0 := C; 4 foreach a A and c C such that 5 (z, l) is an effect of a and l occurs in c do 6 if Sa,c D,C TSAT 7 then C := (C\{c}) weaken(c); 8 end 9 until C = C0; 10 return C;

Figure 2: Algorithm for invariants for temporal planning

much more acute problem. The main reason for the poorer scalability is that the preservation of a candidate invariant is tested against the set of all actions rather than a single action, lifting the asymptotic complexity by O(n) for n (ground) actions, typically from O(n) to O(n2). To present our results, we use a simple but general model which covers an important fragment of temporal planning. However, everything in this section can be generalized to more expressive temporal modeling languages.

Deﬁnition 15 (Schematic Temporal Effects) A schematic temporal effect is a pair (z, l) where z > 0 indicates how much after the time point of the action the effect takes place and l is a schematic effect (as in Deﬁnition 7).

Deﬁnition 16 (Schematic Temporal Actions) A schematic action is a pair c, e where

c is a schematic formula, and e is a set of schematic temporal effects.

An important feature of temporal modeling languages is concurrency. In this work we only use constraints on concurrency that are binary constraints between two actions. This is in line with most of earlier work temporal planning, including all standard benchmark problems. Nevertheless, our deﬁnitions can be trivially generalized to non-binary constraints, needed for example for N-ary resources familiar from scheduling. Our focus in this section is the iterative algorithm by Rintanen (2014), given in Figure 2, which, besides being a generalization of the algorithm for classical planning in the previous section, also covers a wide range of different types of temporal invariants. This algorithm similarly uses a satisﬁability test, for a temporal logic. The greatest difference to the classical case is that the required satisﬁability tests have to address the possibility of multiple actions taking place concurrently. This somewhat complicates the formal result, but, as we will see, leads to a similar upper bound on the number of objects needed in limited grounding. For formalizing the satisﬁability tests we use temporal logic operators [z]φ which says that φ is true at time point z relative to the current time point, the interval operator [z, z ]φ for the truth of φ over the (closed) interval [z, z ] relative to the current time point, and the until operator φUψ which says that φ remains true until ψ is true (if ever). The always operator 2 is deﬁned as the open interval operator

] , [. The truth of a temporal formula φ in a given time point z is given by a temporal valuation v through the relation v |=z φ. This relation generalizes to arbitrary formulas φ given v |=t x for atomic propositions x. The satisﬁability test includes (ground) formulas that describe the behavior of all actions, including their preconditions and effects, as well as constraints on their concurrency. They (explained in (Rintanen 2014)) are as follows. formula explanation (1) a prec(a) action a has precondition prec(a) (2) a [z]l action a has temporal effect (z, l) (3) l l U n i=1[ zi]ai frame axiom for literal l (4) a [z0, z1]a exclusion of actions Here the frame axiom says that l remains true until made false by action ai taken at a relative (earlier) time point zi, where a1, . . . , an are all actions respectively with (zi, l) as their temporal effect, for some zi 0. The exclusion formulas indicate that two actions cannot be taken at the same or nearby time points. These formulas describe the dynamics of the temporal actions exactly, but not all of them are needed for the soundness of the invariant computation. Indeed, the satisﬁability tests typically used are incomplete for reasons of efﬁciency (polynomial time, rather than solving the NP-hard satisﬁability problem exactly.) Interestingly, for the temporal satisﬁability tests needed in computing invariants, the formulas (1) and (2) can be left out: this does not sacriﬁce correctness of the computation, may reduce the number of invariants identiﬁed (because the consistency checks could become too weak to prove that an invariant must remain true), but in practice (conﬁrmed experimentally) does not change the set of invariants found. The proof of Theorem 5 assumes this.

Deﬁnition 17 (Formulation of A Problem Instance) We deﬁne the set MD as formulas (3) and (4) for all ground instances of actions in a given instance of temporal planning with domain function D.

Deﬁnition 18 (Instances of Candidate Formulas) Schematic formulas of the forms l and l [0, z[l , where l and l are atomic propositions x (state variables) or their negations x, are candidate invariants. For a set C of such formulas, CD denotes the set of all ground instances of C with with respect to domain function D.

Deﬁnition 19 (Invariance Test (Rintanen 2014)) The invariance test for a given action a A and formula c such that a has effect (z, l) and one of the literals in c is l, is the following set of formulas.4

Sa,c D,C = {2φ|φ MD} {] , 0]φ | φ CD} {]0, [a | a A} {[0]a, [0]prec(a), [z] c}

The counterpart of Deﬁnition 14 for the temporal case is the following, where we limit to invariants with 2 literals

4We added [0]prec(a) to compensate for the removal of formulas (1) a prec(a). This is critical to obtain the same invariants.

only, and have to acknowledge the involvement of two actions in falsifying a candidate invariant, rather than one.

Deﬁnition 20 (Limited Instantiation for Temporal Planning) For a given action set A, predicate set P, domain function D and type t, deﬁne

L t (A, P) = 2(max(max a A prmst(a)), max p P prmst(p))

Next is the counterpart of Theorem 3.

Theorem 5 Let A be a set of schematic temporal actions, D a domain function for the types T, D a domain function such that for every t T, either D (t) = D(t) or

1. D (t) D(t), 2. |D (t)| L t (A, P), 3. D (t) includes all ﬁxed objects of type t, and 4. D (t0) D (t1) iff D(t0) D(t1), for all {t0, t1} T.

Let c be a schematic candidate invariant. Assume Saσ,cσ D,C is satisﬁable for some schematic action a and a schematic candidate invariant c for some σ with range D, and aσ is relevant for cσ. Then Saσ ,cσ

D ,C is satisﬁable for some σ with range in D .

Proof: Given a satisfying valuation v for Saσ,cσ D,C , we will

construct a satisfying valuation v for Saσ ,cσ

D ,C . The starting point is aσ and cσ, analogously to the proof of Theorem 3. An additional component is a possible second action a σ which may be involved in falsifying the second literal in cσ. For the simplicity of presentation the proof is given for cσ = x [0, d]x , with other syntactic forms of cσ proved analogously. We assume that aσ has effect (z, x) (assumption that aσ is relevant for cσ). If v |=0 x and aσ does not make x true, then taking aσ alone falsiﬁes cσ. Otherwise v |=0 x and some action a (possibly a = a) makes x false between time points 0 and z + d, with a taken at some time point z 0. This is the case we address in the rest of the proof sketch. The ﬁrst case is similar and simpler. Let L consist of all state variables in aσ, a σ and cσ. Let R(t), for all t T be any subset of D(t) of same cardinality as D (t) that includes all objects of type t in L. Such sets R(t) exist because of the assumption that |D (t)| L t (A, P) and because with assumption that aσ is relevant for cσ a, a and c together have at most L t (A, P) parameters. Let R = t T R(t). Let π a bijective mapping π : R t T D (t) such that for all o R and t T, π(o) D (t) iff o D(t). Such a mapping exists because the cardinalities of R(t) and D (t) are the same. Deﬁne σ = σπ. We deﬁne a temporal valuation v that corresponds to aσ and a σ (possibly) changing the values of x and x to false and all other state variables unchanged.

1. v |=z π(x ) iff v |=0 x , for every z and x L\{x, x }

2. v |=z a σ for all z and a σ A\{aσ, a σ}

3. v |=0 a and v |=z a for all z = 0

year problem |Alim| max |A| 2014 driverlog 160 105300 2014 ﬂoortile 396 600 2014 matchcellar 6 1326 2014 parking 600 6468 2014 satellite 64 33034 2014 storage 320 6468 2014 tms 34 1104 2014 turnandopen 640 17450

Table 1: Number of ground actions

4. v |=z a and v |=z a for all z = z

5. v |=0 π(x) iff v |=0 x 6. v |=0 π(x ) iff v |=0 x

7. Values of x and x change in v only at the time points determined by aσ and a σ . The proof that v satisﬁes CD over the interval ]0, ] is as in Theorem 3. The rest of Sa,c D ,C is straightforward because of the action variables only aσ and a σ are true, and only x and x change.

Evaluation In most of standard temporal planning benchmark problems the majority of schematic state variables and actions have at most one parameter of each type, sometimes 2, which by Theorem 5 leads to a low number of ground instances, well within the capabilities of the target algorithm (Rintanen 2014). Table 1 shows the numbers of ground instances for some of the problems from the 2014 planning competition. For each problem class we give the reduced number |Alim| of ground actions as justiﬁed by Theorem 5 and the highest number max |A| of ground actions of all instances in the class (after simpliﬁcations by the planner front-end). We have plotted the runtimes of the algorithm by Rintanen (2014) for the problems from the 2008, 2011 and 2014 competitions in Figure 3. Obviously, the number of actions (and state variables) is a decisive factor in the performance of the algorithm, with runtimes of each iteration approximately O(n3) in the size of the ground instance. A decrease in the number of ground actions and state variables decimates runtimes: at 250 ground actions they are never over 10 seconds. With 50 actions it is at most 3 seconds. Figure 4 demonstrates with applicable problem instances from the competitions 2008, 2011 and 2014 the runtime reduction obtained by grounding a temporal planning problem only partially according to Theorem 5, obtaining schematic invariants from the fully grounded instance, instantiating them with the limited domains, and running Rintanen s (2014) algorithm to obtain ground invariants, which are ﬁnally lifted to the original problem instance. Except for some of the smallest instances the reductions are rather consistent, and in many cases dramatic. Runtimes for some of the instances reported in (Rintanen 2014) were over 4 hours, and now all runtimes are some seconds.

10 100 1000 10000 100000

runtime in seconds

Number of actions vs. runtime

Figure 3: Runtime vs. number of ground actions

0.1 1 10 100 1000

schematic algorithmic

ground algorithm

Runtime comparison

Figure 4: Reduction in runtime

For most of the benchmarks, the obtained invariants are the same for both algorithms. Exceptions are Crewplanning, Elevator and some variants of Openstacks, which all contain critical information in the initial state that cannot be effectively utilized without grounding: for Crewplanning this is data on the succession of days, and for Elevator and Openstacks it is action durations which vary between ground instances of some of the schematic actions.

We have shown how limited grounding of schematic actions leads to simple schematic algorithms for ﬁnding invariants in classical and temporal planning. Schematic algorithms are efﬁcient when the number of action schemas is low. However, such algorithms are complicated and rather difﬁcult to implement, especially when good scalability is desired, and start to fail when the number of action schemas is high, even when the number of instances is low. Our hybrid approach which only produces a (potentially very small) subset of all ground instances of a schematic action set, scales up well and is as easy to implement as algorithms that only use ground actions and invariants.

References Bernardini, S., and Smith, D. E. 2011. Automatic synthesis of temporal invariants. In Proceedings of the 9th Symposium on Abstraction, Reformulation, and Approximation, SARA 2011. AAAI Press. Blum, A. L., and Furst, M. L. 1997. Fast planning through planning graph analysis. Artiﬁcial Intelligence 90(1-2):281 300. Edelkamp, S., and Helmert, M. 2000. Exhibiting knowledge in planning problems to minimize state encoding length. In Recent Advances in AI Planning. 5th European Conference on Planning, ECP 99, number 1809 in Lecture Notes in Artiﬁcial Intelligence, 135 147. Springer-Verlag. Gerevini, A., and Schubert, L. 1998. Inferring state constraints for domain-independent planning. In Proceedings of the 15th National Conference on Artiﬁcial Intelligence (AAAI-98), 905 912. AAAI Press. Gerevini, A., and Schubert, L. K. 2000. Discovering state constraints in DISCOPLAN: some new results. In Proceedings of the 17th National Conference on Artiﬁcial Intelligence (AAAI-2000), 761 767. AAAI Press. Lin, F. 2004. Discovering state invariants. In Principles of Knowledge Representation and Reasoning: Proceedings of the 9th International Conference (KR 2004), 536 544. AAAI Press. Rintanen, J. 1998. A planning algorithm not based on directional search. In Principles of Knowledge Representation and Reasoning: Proceedings of the Sixth International Conference (KR 98), 617 624. Morgan Kaufmann Publishers. Rintanen, J. 2000. An iterative algorithm for synthesizing invariants. In Proceedings of the 17th National Conference on Artiﬁcial Intelligence (AAAI-2000), 806 811. AAAI Press. Rintanen, J. 2006. Uniﬁed deﬁnition of heuristics for classical planning. In ECAI 2006. Proceedings of the 17th European Conference on Artiﬁcial Intelligence, 600 604. IOS Press. Rintanen, J. 2008. Regression for classical and nondeterministic planning. In ECAI 2008. Proceedings of the 18th European Conference on Artiﬁcial Intelligence, 568 571. IOS Press. Rintanen, J. 2012. Engineering efﬁcient planners with SAT. In ECAI 2012. Proceedings of the 20th European Conference on Artiﬁcial Intelligence, 684 689. IOS Press. Rintanen, J. 2014. Constraint-based algorithm for computing temporal invariants. In Logics in Artiﬁcial Intelligence, 14th European Conference, JELIA 2014, volume 8761 of Lecture Notes in Computer Science, 665 673. Springer Verlag. Smith, D. E., and Weld, D. S. 1999. Temporal planning with mutual exclusion reasoning. In Proceedings of the 16th International Joint Conference on Artiﬁcial Intelligence, 326 337. Morgan Kaufmann Publishers.