2 Related work

The pioneering work of LPSAT (Wolfman & Weld, Reference Wolfman and Weld1999) on planning with resources can indeed be considered one of the precursors of SMT, as the basic ideas of SMT (Boolean abstraction, interaction of a SAT solver with a theory solver, etc.) were already present in it.

A comparison between SAT- and SMT-based encodings for planning in numeric domains can be found in Hoffmann et al. (Reference Hoffmann, Gomes, Selman and Kautz2007). In the SAT approach, the possible values of numeric state variables is approximated, by generating a set of values D _t (v) for every numeric variable v, so that every value that v can have after t time steps is contained in D _t (v). These finite domains then serve as the basis for a fully Boolean encoding, where atoms represent numeric variables taking on particular values. With respect to SMT, where numeric variables and expressions are first class citizens, the authors argue that the expressivity of the SMT language comes at the price of requiring much more complex solvers than for SAT and, for this reason, their SAT-based method is very efficient in domains with tightly constrained resources, where the number of distinct values that a numeric variable can take is small.

Other approaches, related to SMT to some amount as well, have been developed more recently. In Belouaer and Maris (Reference Belouaer and Maris2012), a set of encoding rules is defined for spatio-temporal planning, taking SMT as the target formalism. On the other hand, in Gregory et al. (Reference Gregory, Long, Fox and Beck2012) a modular framework, inspired in the architecture of lazy SMT, is developed for planning with resources.

3 Preliminaries

A numeric planning problem is defined as a tuple 〈V, P, A, I, G〉, where V is a set of numeric variables, P a set of propositions (or Boolean variables), A is a set of actions, I the initial state and G a formula over V∪P that any goal state must satisfy.

A state is a total assignment to the variables. Actions are formalized as pairs 〈p, e〉, where p are the preconditions and e the effects. More formally, p is a set of Boolean expressions over V∪P, while e a set of (conditional) effects of the form f⇒d, where f is a Boolean expression over V∪P and d a set of assignments. An assignment is a pair 〈v, exp〉, where v is a variable and exp an expression of the corresponding type. For example, increasing a variable v by 1 is represented by the pair 〈v, v+1〉, indicating that v+1 is the value that v will hold in the next state. Unconditional effects are represented by setting f=true.

The active effects of an action a=〈p, e〉 in a state s are ${\cup}_{{f \Rightarrow d \,\in \,e}} \left\{ {d\!\mid\!s\!\models f} \right\}$ . An action a=〈p, e〉 is executable in a given state s if s⊨p and the active effects of a in state s are consistent. For numeric variables, we restrict to the case where there is only one assignment per variable in the active effects.

The state resulting from executing action a in state s is denoted by apply(a, s)=s′. The new state s′ is defined by assigning new values to the variables according to the active effects, and retaining the values of the variables that are not assigned values by any of the active effects.

A sequential plan of length n for a given planning problem 〈V, P, A, I, G〉 is a sequence of actions a ₁; a ₂; …; a _n such that apply(a _n … apply (a ₂, apply (a ₁, I))…)⊨G.

A parallel plan of length n can be defined similarly to a sequential plan. Instead of having a sequence of actions, we have a sequence of sets of actions σ ₁; σ ₂; …; σ _n such that order (σ ₁)⊕ order (σ ₂) ⊕ … ⊕ order (σ _n ) is a sequential plan, where order (σ _i ) is an ordering function which transforms the set σ _i into a sequence of actions, and ⊕ denotes the concatenation of sequences. Actions in the same set σ _i are said to occur in parallel.

The notion of parallelism of a ∀-step plan is defined as the possibility of ordering the actions of each set to any total ordering, that is, no two actions a, a′ in each σ _i are interfering (e.g. executing a neither falsifies the precondition of a′ nor changes any of its active effects, and vice versa).

The ∃-step semantics weakens the ∀-step requirements, by only requiring the existence of some correct ordering of the actions that results in a valid sequential plan.

In the planning as SAT approach, a planning problem is solved by considering a sequence of formulas ϕ ₀, ϕ ₁, ϕ ₂, …, where ϕ _i encodes the feasibility of a plan that allows to reach a goal state from the initial state in i steps. The solving procedure proceeds by testing the satisfiability of ϕ ₀, ϕ ₁, ϕ ₂ and so on, until a satisfiable formula ϕ _n is found. It is a matter of the encoding whether one or various (non interfering) actions are executed at each step.

4 Framework and system architecture

RANTANPLAN supports a fragment of PDDL which is close to general numeric PDDL 2.1, excluding the temporal extensions and metric optimizations. With respect to numeric effects, we consider assign (x, exp), increase (x, exp) and decrease (x, exp), where exp is any constant expression over linear integer (or real) arithmetic. With respect to preconditions and conditions of numeric effects, we assume that the restrictions imposed on numeric fluents take the form of any closed formula over linear integer (or real) arithmetic.

The structure of the RANTANPLAN system is represented in Figure 1. To encode the formulas ϕ ₀, ϕ ₁, ϕ ₂, …, one of the two encodings described in the following sections (QF_LIA or QF_UFLIA) is carried out, transforming the PDDL problem to a pure SMT problem. Then the problem is iteratively solved, using the chosen SMT solver as a black box.

Figure 1

Basic architecture and solving process of the RANTANPLAN solver. SMT=satisfiability modulo theories.

A key aspect of the planner is the detection of interferences between parallel actions at compile time, by means of calls to a SMT solver. In case the user demands a parallel plan, a disabling graph is computed. By disabling graph we refer to a directed graph, where nodes are the grounded actions from the planning problem and an edge exists from action a to action a′ if the execution of a can affect a′ (forbid its execution or change its active effects) (Rintanen et al., Reference Rintanen, Heljanko and Niemelä2006). This graph is used, depending on the notion of parallelism chosen, to encode the necessary constraints restricting which actions can be carried out at the same time step. In particular, the solver supports:

• ∙ A sequential encoding, achieved by using an at least one and an at most one constraint.

• ∙ The ∀-step semantics, using the quadratic encoding in Rintanen et al. (Reference Rintanen, Heljanko and Niemelä2006).

• ∙ The ∃-step semantics, with two encodings. Using the quadratic encoding in Rintanen et al. (Reference Rintanen, Heljanko and Niemelä2006), and a linear-size encoding based on a fixed ordering of operators, also in Rintanen et al. (Reference Rintanen, Heljanko and Niemelä2006).

The system supports solving via application programming interface or plain text file using the Yices SMT solver and the Z3 SMT solver. Once a solution has been found, then it is finally retrieved and serialized. In the following subsections, the relevant aspects of the RANTANPLAN solver are explained in more detail.

4.1 QF_LIA encoding

Numeric planning problems with linear integer arithmetic expressions naturally fall into the QF_LIA logic. In the SMT-library standard, QF_LIA stands for the logic of Quantifier-Free Boolean formulas, with Linear Integer Arithmetic constraints. This logic has a good compromise between expressivity and performance, and is the natural choice for this problem. We generalized Rintanen’s (Reference Rintanen2012) encoding of planning as SAT to include numeric variables as follows.

For each time step, every ground instance of a PDDL predicate and action is mapped to a Boolean variable, and every ground instance of a PDDL function is mapped to an integer variable. For instance, a predicate stating the position of an aircraft such as at(?a - aircraft, ?c - city), with three cities c ₁, c ₂ and c ₃, and two planes p ₁ and p ₂, will result into six ground instances at(p ₁, c ₁), …, at (p ₂, c ₃), that will be mapped to six Boolean variables $$at_{{p_{1} ,\,c_{1} }}^{t} $$ , …, $$at_{{p_{2} ,\,c_{3} }}^{t} $$ for each time step t. Following the same example, being at(?o - aircraft) - city an object fluent, the mapping would result into two integer variables $$at_{{p_{2} }} $$ , $$at_{{p_{2} }} $$ with the domains being the possible cities c ₁, c ₂ and c ₃ (these are internally mapped into three distinct integers). Note that thanks to the SMT language, we can get a more compact encoding of states in the presence of object fluents than using a plain SAT approach. The Boolean variables resulting from actions will be used to denote what action is executed at each time step, and with which parameters. The Boolean and integer variables resulting from grounding the predicates and functions, respectively, will constitute the state variables. A superscript t is used to differentiate the variables at each time step.

Given a formula ϕ, by ϕ ^t we denote the same formula ϕ, where all integer variables x have been replaced by x ^t . For the case of assignments, we define:

$$\eqalignno{ & \left\langle {x,\,{\rm true}} \right\rangle ^{t} \mathop{\, {\equals}\, }\limits^{{{\, \rm def}}} x^{t} \cr & \left\langle {x,\,{\rm false}} \right\rangle ^{t} \mathop{\, {\equals}\, }\limits^{\,{{\rm def}}} \neg \,x^{t} \cr & \left\langle {x,k} \right\rangle ^{t} \mathop{\, {\equals}\, }\limits^{{{\rm \, def}}} \left( {x^{t} \, {\equals}\, k} \right) \cr & \left\langle {x,x{\plus}k} \right\rangle ^{t} \mathop{\, {\equals}\, }\limits^{{{\rm \, def}}} \left( {x^{t} \, {\equals}\, x^{{t{\minus}1}} \,{\plus}\,k} \right) \cr & \left\langle {x,x\,{\minus}\,k} \right\rangle ^{t} \mathop{\, {\equals}\, }\limits^{{{\rm \,def}}} \left( {x^{t} \, {\equals}\, x^{{t{\minus}1}} {\minus}k} \right) $$

For each groundFootnote ¹ action a=〈p, e〉, we have the following constraints. First, its execution during time step t implies that its precondition is met:

(1) $$a^{t} \to p^{t} \quad \quad \quad \quad \quad \forall a\, {\equals}\, \left\langle {p,e} \right\rangle \in A$$

Also, each of its conditional effects will hold at the next time step if the corresponding condition holds:

(2) $$\left( {a^{t} \wedge f^{t} } \right)\to d^{{t{\plus}1}} \quad \quad \quad \quad \quad \forall a\, {\equals}\, \left\langle {p,e} \right\rangle \in A,\forall f \Rightarrow d \in e$$

Here, we view sets d of literals as conjunctions of literals. Recall also that unconditional effects will have true as condition f. Second, we need explanatory axioms to express the reason of a change in state variables. For each variable x in V∪P:

(3) $$\matrix{ {x^{t} \,\ne\,x^{{t{\plus}1}} \to\mathop \vee\limits_{a\, {\equals}\, \left\langle {p,e} \right\rangle \, \in \,A} \left( {a^{t} \wedge\left( {EPC_{x} \left( a \right)} \right)^{t} } \right)} \cr } $$

where, given an action a=〈p, e〉 and a variable x

$$\matrix{ {EPC_{x} \left( a \right)\, {\equals}\, \mathop \vee\limits_{f \, \Rightarrow \,d \, \in \, e} \left\{ {f\!\mid\!d\,{\rm contains}\,{\rm an}\,{\rm assignment}\,{\rm for}\,x} \right\}} \cr } $$

that is, the effect precondition for the modification of x in action a, where the empty disjunction is defined as false. For Boolean variables, the expression x ^t ≠x ^t+1 can be written as (x ^t ∧¬x ^t+1)∨(¬x ^t ∧x ^t+1). These constraints have to be complemented depending on the parallelism we wish.

4.2 Interference between actions

As said in the introduction, a key concept in parallel plans is the notion of interference between actions. This issue has been carefully considered by Rintanen et al. (Reference Rintanen, Heljanko and Niemelä2006) in the setting of planning as SAT. Given a disabling graph, where an edge exists from action a to action a′ if the execution of a can affect a′, we know, for example, that the simultaneous execution of all actions pertaining to a strongly connected component is not possible, as given all possible orderings of actions, all of them contain a cycle (and thus they cannot be serialized). Note that acyclicity is a sufficient but not necessary condition for a set of actions to be executable in some order, since disabling graphs are computed independently of any state.

In Rintanen et al. (Reference Rintanen, Heljanko and Niemelä2006), an action a ₁ is defined to affect another action a ₂ if a ₁ may prevent the execution of a ₂ or change its active effects, and two actions a ₁ and a ₂ are considered to interfere if a ₁ affects a ₂ or a ₂ affects a ₁. In ∀-step plans, where all possible serializations must be valid, no two interfering actions can occur in parallel. In the more relaxed notion of parallelism of ∃-step plans, where it is only required that no action affects a later one in some total ordering, often much more parallelism is allowed in practice. For efficiency reasons, typically syntactic (rather than semantic) restrictions are imposed on parallel actions. For example, in Rintanen et al. (Reference Rintanen, Heljanko and Niemelä2006), where only Boolean variables are considered, a ₁=〈p ₁, e ₁〉 is determined to affect a ₂=〈p ₂, e ₂〉 if, for some variable a,

1. 1. a is set to true in d ₁ for some f ₁⇒d ₁∈e ₁, and a occurs negatively in p ₂ or occurs in f ₂ for some f ₂⇒d ₂∈e ₂, or

2. 2. a is set to false in d ₁ for some f ₁⇒d ₁∈e ₁, and a occurs positively in p ₂ or occurs in f ₂ for some f ₂⇒d ₂∈e ₂.

That is, a ₁ affects a ₂ if a ₁ can impede the execution of a ₂, or change its effects. Note that this is not a symmetric relation.

This is a fully syntactic check which can be used to establish sufficient although not necessary conditions for finding serializable parallel plans. We can observe that interference between effects is not considered. This is because, in the case two actions have contradictory effects, any formula encoding a plan with those two actions running in parallel will become unsatisfiable.

The previous approach could be naively generalized to the case of numeric variables as follows: an action a ₁=〈p ₁, e ₁〉 affects an action a ₂=〈p ₂, e ₂〉 if, for some variable x, x is modified in d ₁ for some f ₁⇒d ₁∈e ₁, and x occurs in p ₂ or occurs in f ₂ for some f ₂⇒d ₂∈e ₂.

Performing only syntactic checks like the previous seems too much restrictive for numeric variables, even in the case that we determine interference at compile time, that is, independently of any concrete state. For this reason, we propose a new ideaFootnote ² , which is to use SMT technology to perform semantic checks of interference at compile time, in order to increase the amount of parallelization of numeric plans.

Our method is independent of any test suite and does not require any special purpose algorithm, as it relies on encoding the possible interference situations between pairs of actions as SMT formulas and checking their satisfiability, by calling an SMT solver, at compile time. For example, an important difference with the purely syntactic definition of interference of Rintanen et al. (Reference Rintanen, Heljanko and Niemelä2006) is that we include the preconditions of the actions in the semantic checks. More precisely, two actions can occur in parallel only if their preconditions can be satisfied simultaneously, regardless of the variables they contain. This way, we are able to avoid many ‘false positive’ interference relationships.

All in all, we obtain a much more fine-grained notion of interference, that we will see how it helps us to increase the parallelization of actions. Note that the interference relationships determined semantically will always be a subset of the interference relationships determined syntactically. Interestingly, we will be using an SMT solver both at compile time, as an oracle to predict interference relationships, and at solving time. For efficiency reasons, to perform the interference checks we do not consider grounded actions, but the original actions in the PDDL model. Since now actions are not instantiated, we need to unify the parameters of the same type in the actions for which we check interference.

Imagine we have two actions, say move(?d - ship ?a ?b - location) and dock(?e - ship ?c - location). We will be interested to know, for example, if the actions interfere in the case that ?d and ?e are the same ship. Or in the case that locations ?a and ?c are the same, etc. We will have to check all the possible combinations of equalities and disequalities between the parameters. These combinations are all the possible partitions of the sets formed by all the parameters of the two considered actions grouped by its most general declared type. Once the set partitions have been generated for each set of parameters, each parameter is substituted by an integer. When we intent for two parameters to be equal (i.e. they are in the same partition), we substitute them for the same integer, and by different integers when we want them to be different. Finally, the formulas encoding the incompatibility between the actions are checked for satisfiability.

These consistency checks can be done in a reasonable time with an SMT solver, and the amount of parallelism achieved is significantly higher than with syntactic approaches. To illustrate the situations where our new notion of interference (thoroughly explained in Bofill et al., Reference Bofill, Espasa and Villaret2016) is especially accurate, consider the following example. The Planes domain in Figure 2 consists in transporting people between cities using planes. Each plane has a limited number of seats and a given fuel capacity. We focus on the fly and board actions. A plane can only fly if it is transporting somebody and it has enough fuel to reach its destination, and boarding is limited by seat availability.

Figure 2

PDDL model of the Planes domain

The syntactic notion of interference would determine interference between fly and board, since board modifies the onboard function (number of passengers) and fly checks the value of this function in its precondition. On the contrary, with the semantic technique, we would find out that there is no interference at all, since it is impossible that the preconditions of board and fly were true at the same time, and after executing board the precondition of fly became false. Note that the precondition of fly requires (> (onboard ?a) 0) and the effect (increase (onboard ?a) 1) of board can never falsify (> (onboard ?a) 0).

4.3 Sequential and parallel plans

The sequential encoding allows exactly one action per time step. This is achieved by imposing an exactly one constraint on the action variables at each time step. We tested some well-known encodings, and we settled with the binary encoding (Frisch & Giannaros, Reference Frisch and Giannaros2010) as it gave us the best performance.

A ∀-step plan is defined as the possibility of ordering the actions of each time step to any total order. Therefore, at each time step t we simply add a mutex between any pair of interfering actions a _i and a _j :

(4) $$\neg \left( {a_{i}^{t} \wedge a_{j}^{t} } \right)\,{\rm if}\,a_{i} \,{\rm affects}\,a_{j} \,{\rm or}\,a_{j} \,{\rm affects}\,a_{i} $$

In ∃-step plans, there must exist at least a total ordering of parallel actions resulting in a valid sequential plan. RANTANPLAN implements a quadratic encoding for this purpose. It takes as ingredient an arbitrary total ordering < on the actions, and the parallel execution of two actions a _i and a _j such that a _i affects a _j is forbidden only if i<j:

(5) $$\neg \left( {a_{i}^{t} \wedge a_{j}^{t} } \right)\,{\rm if}\,a_{i} \,{\rm affects}\,a_{j} \,{\rm and}\,i\,\lt\,j$$

The linear-size encoding for ∃-step plans described in Rintanen et al. (Reference Rintanen, Heljanko and Niemelä2006), is also supported. Since ∃-step plans are less restrictive than ∀-step plans, as they do not require that all orderings of parallel actions result in valid sequential plan, they normally allow more parallelism.

4.3.1 Plan serialization

To obtain a sequential plan from the solution, for each time step with more than one action, a subgraph of the disabling graph is extracted, containing only the actions at that time step. A valid order between actions can then be computed. Since in all implemented parallel encodings acyclicity is guaranteed between the executed actions, a reversed topological order of the subgraph is always as a valid order.

5 Extension: QF_UFLIA encoding

As the previously introduced QF_LIA encodings grows considerably with the time horizon, to the point of getting unmanageable instances, we started to develop a more compact encoding, using the theory of uninterpreted functions to express predicates, functions and actions. This encoding is reminiscent of the lifted causal encodings in Kautz et al. (Reference Kautz, McAllester and Selman1996).

In the SMT-library standard, QF_UFLIA stands for the logic of Quantifier-Free Boolean formulas, with Linear Integer Arithmetic constraints and Uninterpreted Functions. Uninterpreted functions have no other property than its name and arity, and are only subject to the following axiom: $$x_{1} \, {\equals}\, {x{\prime}\!\!\vskip 4pt_1} \wedge\,\ldots\,\wedge x_{n} \, {\equals}\, {x{\prime}\!\!\vskip 4pt_n} \to f\left( {x_{1} ,\,\,\ldots\,,\,x_{n} } \right)\, {\equals}\, f\left( {x{\prime}\!\!\vskip 4pt_1} ,\,\,\ldots\,,\,{x{\prime}\!\!\vskip 4pt_n} } \right)$$ .

The encoding goes as follows. Every defined object in the problem is mapped to an integer. For each function, predicate and action, an uninterpreted function is declared, with each parameter being declared as an integer. Also, a new integer parameter is added to each of them, representing a time step. Uninterpreted functions corresponding to predicates and actions return a Boolean value, while the ones for functions return an integer value. Moreover, for each action, parameter and time step, a new integer variable is defined, representing the value of that parameter in the action if executed at the corresponding time step.

For example, the Boolean function $$\varphi _{a} \left( {x_{{a,1}}^{t} ,\,\,\ldots\,,\,x_{{a,n}}^{t} ,\,t} \right)$$ determines whether action a with parameters $$x_{{a,1}}^{t} ,\,\,\ldots\,,\,x_{{a,n}}^{t} $$ is executed at time step t. The parameter t is a constant, which is shared between all uninterpreted functions for the actions, predicates and functions in the same time step. Contrarily, $$x_{{a,1}}^{t} ,\,\,\ldots\,,\,x_{{a,n}}^{t} $$ are variables with finite domains, and constraints are added to restrict their possible values. Regarding predicates and functions, no new variables are defined, since their arguments will be either constants or variables occurring in some action.

We remark that, in this new setting, a state is defined by the value of the uninterpreted functions corresponding to predicates and functions, for a given value of their arguments. Equations (1) and (2) of the QF_LIA encoding are generalized here as

(6) $$\varphi _{a} \left( {x_{{a,1}}^{t} ,\,\,\ldots\,,\,x_{{a,n}}^{t} ,t} \right)\to p^{t} \quad \quad \quad \quad \quad \forall a\, {\equals}\, \left\langle {p,\,e} \right\rangle \in A$$

(7) $$\varphi _{a} \left( {x_{{a,1}}^{t} ,\,\,\ldots\,,\,x_{{a,n}}^{t} ,t} \right)\wedge f^{t} \to d^{{t{\plus}1}} \quad \quad \quad \forall a\, {\equals}\, \left\langle {p,\,e} \right\rangle \in A,\forall \left\langle {f,\,d} \right\rangle \in e$$

Note that this results in a much more compact encoding than if we restrict to QF_LIA, since here we are using variables as arguments of functions, and it is the SMT solver who is in charge of guessing the concrete values of the parameters of the executed actions. The considered set of actions A is now parametrized, and hence similar to that of PDDL, with actions like fly(x, y, z), instead of grounded actions like $${\rm fly}_{{p_{1} ,c_{1} ,c_{1} }} ,\,{\rm fly}_{{p_{1} ,c_{1} ,c_{2} }} $$ , etc. Equation (3) is generalized as

(8) $$\eqalignno{ &#x0026; \varphi _{h} \left( {c_{{h,1}} ,\,\,\ldots\,,\,c_{{h,n}} ,t} \right)\,\ne\,\varphi _{g} \left( {c_{{h,1}} ,\! \ldots \! ,c_{{h,n}} ,t{\plus}1} \right)\to \cr &#x0026; \quad \quad \quad \quad \quad \mathop \vee\limits_{a \, \in \, {\rm touch}(g)} \left( {\varphi _{a} \left( {x_{{a,1}}^{t} ,\! \ldots \!, \,x_{{a,m}}^{t} ,t} \right)\mathop \wedge\limits_{\matrix{ {i\in1..n,j\in1..m} \cr {{\rm name}\left( {h,\,i} \right)\, {\equals}\, {\rm name}\left( {a,\,j} \right)} \cr } } \left( {x_{{a,j}}^{t} \, {\equals}\, c_{{h,i}} } \right)} \right) \cr &#x0026; \quad \quad \quad \quad \quad \quad \quad \quad \quad \quad \quad \quad \quad \quad \quad \quad \forall h \in H,\;\forall c_{{h,1}} ,\!\,\ldots\!,\,c_{{h,n}} \in S_{1} {\times}\,\ldots\,{\times}S_{n} $$

where H is the set of predicates and functions, touch(h) is the set of actions that may modify h, S _i the domain of the ith argument of φ _h , and name(h, k) is the name in the PDDL model of the kth argument of the functor h. To help the reader understand the formula, we provide an example. Suppose we have the following simple PDDL problem:

• ∙ objects: A,B - truck, L1,L2,L3 - loc

• ∙ predicate: at(?t - truck, ?l - loc)

• ∙ actions: travel(?t - truck, ?from ?to - loc) and refuel(?x - truck, ?where - loc)

• ∙ function: fuel(?t - truck) - number

where travel has (decrease (fuel ?t) 10) among its effects, and refuel has (increase (fuel ?x) 20) as its only effect. Constraint (8) for the fuel function would be encoded into SMT at time step 0 as follows:

That is, we are saying that if the fuel of truck A (or B) has changed this should be because it has been the protagonist of some action implying a modification in its fuel, namely traveling or refueling. Again, this is much more compact than its QF_LIA counterpart. With respect to the parallelism, for now this encoding only supports the sequential plan semantics, as encoding parallelism using this encoding is not straightforward. This approach is currently under development, as we obtained encouraging preliminary experimental results (Bofill et al., Reference Bofill, Espasa and Villaret2014).

6 Experimental evaluation

The goal of the experiments is to evaluate if RANTANPLAN is competitive with state of the art exact numeric planners, as well as showing the benefits of having a good notion of interference. We report on experiments with RANTANPLAN using Yices (Dutertre & De Moura, Reference Dutertre and De Moura2006) v1.0.38 as back-end solver. All experiments have been run on 8GB Intel^® Xeon^® E3-1220v2 machines at 3.10 GHz.

For the sake of simplicity, only QF_LIA ∃-step plans are considered, using a quadratic encoding for expressing incompatibility of actions. We experimentally observed that the solver behavior was more stable when using a quadratic encoding than when using a linear encoding.

We consider four distinct domains: the numeric versions of ZenoTravel and Depots, the real-life challenging Petrobras domain, and the crafted Planes domain, shown in Figure 2. All instances have been translated to make use of object fluents, in order to obtain a compact representation in the translation to SMT. The Planes domain was crafted due to the limited interest of the other domains with respect to numeric interactions between actions. This new domain was derived from ZenoTravel, by adding some plausible numeric constraints that will help us demonstrate the goodness of the semantic approach when determining potential interference between actions.

We compare the performance of RANTANPLAN with the exact numeric planner NumReach/SAT (Hoffmann et al., Reference Hoffmann, Gomes, Selman and Kautz2007) using MiniSAT 2.2.0, and NumReach/SMT using Yices v1.0.38. For NumReach/SMT, we had to adapt its output so it could be used with modern SMT solvers. Moreover, since NumReach supports neither object fluents nor conditional effects, the models have been properly adapted.

Table 1 shows the results for the domains considered using the RANTANPLAN system. The syntactic column shows the results using the generalization of the interference notion of Rintanen et al. (Reference Rintanen, Heljanko and Niemelä2006), described at the beginning of the Section 4.2, additionally forbidding any two actions to occur in parallel if they modify the same numeric variable. The semantic column shows the results with the introduced new semantic notion of interference. In these two columns the number of parallel steps of the valid plan is found between parentheses. In case of a time out the number between parentheses is the last plan length considered.

Table 1

Time in seconds followed by the number of parallel steps of the plan found between parentheses, for each instance

TO=time out; MO=memory out.

Cut-off set to 3600 seconds. The Time and Edges columns show the reduction in time and edges of the disabling graph, respectively, when using the semantic approach. Instances where all approaches timed out are omitted.

The Time column shows how much faster each instance is solved with the semantic notion of interference, and the Edges column shows which percentage of edges of the disabling graph can be avoided thanks to this new interference notion. Note that even in instances that need the same amount of time steps, the reduction of edges in the disabling graph affects positively on the solving time. This is probably because we are reducing the number of clauses that do not contribute at all to the problem.

Table 2 shows the results for the domains considered, comparing NumReach with the semantic version of RANTANPLAN. NumReach does a good job with the Depots and ZenoTravel domains, but its performance decreases in more complex numeric domains like Petrobras and Planes, where the range of possible values for numeric fluents tends to grow. It can be seen that on the Planes domain, containing only a few non-trivial numeric constraints, classical approaches (syntactic and NumReach) tend to be overly restrictive with respect to incompatibility between actions. In most instances it can be observed an important gap between the number of time steps needed to find a valid plan by NumReach and our semantic approach. This is also generally reflected in terms of solving time.

Table 2

Time in seconds followed by the number of parallel steps of the plan found between parentheses, for each instance

SMT=satisfiability modulo theories; TO=time out; MO=memory out.

Cut-off set to 3600 seconds. Instances where all systems timed out are omitted.

Table 3 lists the total number of instances of each family, the number of instances solved by NumReach/SAT, NumReach/SMT, and the presented semantic approach. It also gives the number of accumulated parallel time steps used to reach a valid plan on the commonly solved instances by NumReach/SMT and the two methods implemented in RANTANPLAN. Finally, the other columns show the averaged solving time reduction and disabling graph edge reduction on the solved instances. Even in domains that maintain the same number of time steps, the reduced disabling graphs make solving times notably smaller.

Table 3

Summarized results for the domains considered using NumReach/SAT (N/SAT), NumReach/SMT (N/SMT) and RANTANPLAN with the syntactic and the semantic notions of interference

For each domain we report the number of solved instances and their accumulated time steps of the commonly solved ones. We also show their averaged reductions in solving time and number of edges of the disabling graph.

Note that the amount of parallelism in RANTANPLAN is notable. With respect to the number of steps, RANTANPLAN is strictly more parallel than NumReach/SAT and NumReach/SMT in nearly all instances.

The only domain where the RANTANPLAN planner is not competitive is the Depots domain. It is obvious that the reachability approach of NumReach is more adequate for this domain. Moreover, NumReach/SAT dominates NumReach/SMT in this domain. This happens because the numeric reasoning present in the domain is nearly null: the only functions present are for controlling load limits of trucks, and thus this domain is perfectly adequate for the approach used by NumReach/SAT. The use of a Linear Integer Arithmetic solver in the RANTANPLAN planner is overkill and a leaner and more efficient approach should be taken for problems of this kind.