Lifted Sequential Planning with Lazy Constraint Generation Solvers

One of the most significant advances in classical planning was the realisation of Green’s [18] vision for theorem proving as a framework for general problem solving, via the ground-breaking seminal work of H. Kautz and B. Selman [29, 28]. Putting together the insights of Blum and Furst [3], where planning becomes the problem of analysing whether goal states are reachable in a suitably defined graph, with space efficient solutions to the frame problem formulated in the Situation Calculus [32, 19], Kautz & Selman showed that formulating planning problems in terms of satisfiability of Conjunctive Normal Form (CNF) formulas was feasible and, at the time, highly scalable. Attention to planning as satisfiability has been somewhat eclipsed since then with the development of planning algorithms based on direct, but lazy, incremental heuristic search over transition systems [4, 23, 21, 38, 51]. Yet deep theoretical connections exist between planning as satisfiability and as heuristic search [15, 40] questioning [41, 50] perceptions of either approach as being parallel or mutually exclusive.

Like R. Frost’s traveller in the woods this paper finds its way back to a crossroads in the development and study of approaches to planning as satisfiability. One way is that of the so-called GraphPlan encodings (linear and parallel), the other being that of so-called causal encodings (ground and lifted) invented by Kautz, McAllester and Selman (KMS) [28]. Unlike Frost’s poem though, lifted causal encodings are clearly an approach seldom followed in the literature in automated planning. Inspired by the formulation of nonlinear or partially-ordered planning of McAllester and Rosenblitt [31], these encodings have polynomial size over the lower bound on the number of plan steps in feasible plans. Importantly too, they do away entirely with the need for explanatory frame axioms. Yet these very desirable properties follow from the premise of not having to ground actions and predicates first, as otherwise the unavoidable exponential blow outs obliterate any practical differences with GraphPlan encodings.

In this paper we realize this potential by tapping into the power of Lazy Clause Generation (LCG) [35], a ground-breaking technology that unifies propositional satisfiability (SAT) and Constraint Programming (CP), and allows representing implicitly large tracts of complex systems of constraints by suitably defined inference procedures, or propagators. These lazily generate new constraints to record violations by assignments to decision variables, and propagate information following from the consistency of assignments and constraints in order to tighten the domains of variables. This, in addition to very sophisticated and performant modeling tools and solvers [37], provide us the foundations to develop scalable planners that follow the path laid by KMS lifted causal encodings. We have found these planners to clearly outperform state-of-the-art optimal planning algorithms on benchmarks designed to be hard to ground [7], while standing their ground on the IPC benchmarks.

Paper Overview. We start the paper with a precise formulation of the kind of planning problems of interest to us and their solutions. We then introduce a formalism to describe the structure of states and actions that is based on Functional STRIPS [13]. We assume that all atoms in precondition and effects are equality atoms over suitably defined function symbols and constant terms. These ground domain theories are then lifted [31]. With these preliminaries in place, we introduce our encoding, for which we prove validity and provide a characterisation of its complexity. After that, we explain how we leverage state-of-the-art CP solvers to implement efficiently our encoding. We then present a method to do a concise transformation of planning instances represented in PDDL to FSTRIPS. We end with an evaluation of several planners built on top of our encoding and propagators, along with a brief analysis of related work and a discussion of the significance and potential of this research.

A problem planning instance (PPI) is given by a tuple $P=(S,A,\to,s_{0},S_{G})$ where $S$ and $A$ are finite sets of states and actions, $\to$ $\subset$ $S\times A\times S$ is the transition relation, where $s\to_{a}s^{\prime}$ indicates that $s^{\prime}$ is reachable from $s$ via $a$, $s_{0}\in S$ is the initial state and $S_{G}\subset S$ is the set of designated goal states. We say that a PPI admits a trajectory $\sigma=s_{0},a_{1},s_{1},\ldots,s_{i-1},a_{i},s_{i}$ iff $s_{i-1}$ $\to_{a_{i}}$ $s_{i}$ for every $i>0$. In this paper the notion of planning problems is that of optimization problems where we seek sequences $\sigma$ $=$ $s_{0},a_{1},s_{1},\ldots,s_{k-1},a_{k},s_{k}$, that minimize $\mathrm{length}(\sigma):=k$, and satisfies $s_{k}\in S_{G}$. The set of $\sigma$ sequences that satisfy $s_{k}\in S_{G}$ is referred to as the set of valid plans $\Pi_{P}$. The optimal cost of $P$ is thus $c^{*}:=\min_{\sigma\in\Pi_{P}}\mathrm{length}(\sigma)$. When $\Pi_{P}=\emptyset$, we say that $P$ is infeasible and optimal cost is $c^{*}=\infty$. We observe that $|S|-1$ is a trivial upper bound on $c^{*}$ when $\Pi_{P}\neq\emptyset$. Non-trivial, feasibly computable upper bounds are known [1] but only for PPIs with special structure.

The approach known as planning as satisfiability [29] proceeds by considering a sequence of instances for a related decision problem, that of plan existence. We state the latter simply as follows: given some PPI $P$ and parameter $N_{\pi}$, with actions and states defined in terms of some domain theory, the task is to prove that a feasible trajectory $\sigma$ exists such that $\mathrm{length}(\sigma)=N_{\pi}$, or alternatively, certify that no such $\sigma$ exists. The classic algorithm for optimal planning in this framework thus considers the sequence of CSPs $T_{P,n_{0}}$, $T_{P,n_{1}}$, $\ldots$, $T_{P,n_{k}}$, $\ldots$ each of these a reduction of the plan existence problem for $P$ and $N_{\pi}=n_{k}$ into that of the satisfiability of a CSP $T_{P,n_{k}}$ with suitably defined decision variables and constraints. The sequence of natural numbers $n_{0},n_{1},\ldots,n_{k},\ldots$ is typically, but not necessarily [48], defined as $n_{0}$ $=$ $0$, $n_{1}$ $=$ $1$, and so on. When defined in this manner, as soon as $T_{P,n_{k}}$ is satisfiable, we have proven that $c^{*}=n_{k}$. Scalable certification of infeasibility in this framework has been an open problem until recently [8], yet still remains challenging.

We start by giving a high-level account of our proposed encoding of CSPs $T_{P,N_{\pi}}$ and explain the roles played by the decision variables in Table 1. Central to our encoding is the notion of plan step or slot, of which we have one for each action in a plan. In contrast with the causal encoding of KMS, slots are totally ordered thus greatly simplifying the definition of persistence that we use to deal with the frame axioms. To each slot exactly one action schema $\alpha\in Act$ needs to be assigned (variables $act_{i}$), which in turn restricts choices on the possible values for the arguments (variables $arg_{ij}$) of the schema $\alpha$ as per $\tau(\alpha)$. The assignments to the variables $act_{i}$ and $arg_{ij}$ determine the choices of input and output pins for a slot. A pin is a vector of decision variables which we use to represent equality atoms $f(\bar{y})=z$. These variables choose the function symbol $f$, terms (constants in $U$) $\bar{y}$ (a vector) and $z$. Input pins of slot $i$ thus encode the equality atoms in ${\rm Phys.\leavevmode\nobreak\ Rev.\leavevmode\nobreak\ E}{\alpha}(\bar{x})/\bar{v}$ required to be true in state $s_{i-1}$, and output pins the atoms in $\mathrm{Eff}_{\alpha}(\bar{x})/\bar{v}$ required to be true in $s_{i}$, where $\alpha(\bar{v})$ is the ground action selected by the assigned schema and (possibly partially) assigned values to arguments. These dependencies between the variables of a slot are depicted in Figure 1(a), and Figure 1(b) illustrates the active constraints between variables when the move action schema is chosen at slot $i$ in the visitall problem domain. The move schema has two arguments representing the current position and the target position of an agent in an $n\times n$ grid. Thus, when $act_{i}=\emph{move}$, we require that $arg_{i1}\in C$ and $arg_{i2}\in C$, the input pin $in_{i1}$ is assigned the function symbol $at$ and the variable $y_{i1}$ holds an equality relation with $arg_{i1}$.

We note that we create up front variables for arguments and pins following from $K_{\alpha}$, $K_{f}$, $K_{\mathrm{pre}}$ and $K_{\mathrm{eff}}$, all constants given by the data in an instance $P$. For a given slot $i$, argument variables $arg_{ij}$ that are not used by the schema assigned are set to a special $\mathrm{null}$ constant. To disable pins not needed to represent atoms in preconditions or effect formulas we have a Boolean variable $active_{ik}$ that indicates if they are being used. Finally, variables $spt_{jk}$ allow choosing what output pin is supporting a given input pin. These variables allow encoding causal links [31] without referring explicitly to atoms.

In our implementation, the action assigned to slot $i$, $act_{i}$ is an index variable, which depends on the data assigned to input and output pins as per constraints  (7) and (8). Both of these constraints can be encoded compactly using (15a)

where $f_{j}$ is a function symbol, $\nu_{j}$ and $\mu_{j}$ are the argument variables of slot $i$ or constants that are consistent with the definition of action schema when $act_{i}=j$. $f_{j}$ is assigned a special function when the input pin is inactive in the action schema, thus accounting for literals $\neg\textit{active}_{ik}$.

The support variables $spt_{jk}$ are index variables with two elements, $(i,l)$, the first being the index of a slot and the second the index of an output pin. As discussed in the previous section, variables $spt_{jk}$ depend on the data of input pin $in_{jk}$. Output pins $out_{jl}$ and constraints (9a) and (9b) can be accounted for using $\mathrm{element}(\cdot)$ in its matrix form (15b)

where $H$ is the data of all output pins in a $2$-dimensional grid. Constraint (17) thus requires that the data of the output pin at the row $i$ (slot $i$) and column $l$ ($l$-th pin) of $H$ is equal to that in $in_{jk}$. The matrix $H$ includes a specially defined element, containing the data used to represent inactive pins, whose index is assigned to $spt_{jk}$ when the $k$-th input pin at slot $j$ is inactive, thereby encoding constraint (9a).

We exploit other modeling features offered by CpSat to implement the $\mathrm{persist}(\cdot)$ predicate given in Equation (10)

where $u,v_{o}$ and $w$ are auxiliary Boolean variables created for each $(out_{j^{\prime}l},in_{jk})$ pair, and $1$ $\leq$ $o$ $\leq$ $K_{f}$. CpSat does not represent explicitly constraints (18b), (18c) and (18d). Instead, it collects them into a precedences propagator as inequalities between integer variables. The precedences propagator uses the Bellman-Ford algorithm to detect negative cycles in the constraint graph of inequalities, and propagates bounds on the integer variables [34]. Still, $O(N_{\pi}^{2}K_{\mathrm{pre}}K_{\mathrm{eff}}K_{f})$ variables are generated in the worst-case, e.g. $O(n^{5})$ if all these quantities belong to the same order of magnitude. In most of the benchmarks we use to test planners using these encodings, the number of preconditions, effects and arity of functions are much smaller than $N_{\pi}$, thus generating $O(n^{2})$ variables.

Encoding static relations with table constraints. Some PPIs contain domain specific relations that are not affected by the action schemas. For example, in visitall the relation connected is static and its interpretation is fixed by the specification of the initial state. We encode the dependency of the input pin variables on these static relations using table constraints which allow us to specify a set of allowed (or forbidden) assignments to a tuple of variables, i.e. for a static relation $R$, we encode the constraint as $table(in_{ik},R)$, where the pin $in_{ik}$ is specially designed to represent a tuple in $R$. This is more efficient than using the element constraints (17) since CpSat translates them into a concise CNF formulation.

Propagator for Required Persistence. We recall constraint (9c) that enforces the requirement that whenever an output pin $out_{il}$ is to provide causal explanation for an input pin $in_{jk}$, the atom described by the former is not interfered with by any other output pins in intermediate slots. Clearly, the number of variables and clauses (18a) is proportional to $j-i$, bringing the potential number of variables generated to be $O(n^{6})$. While such a rate of growth seems unsustainable for non-trivial instances, the empirical results we obtain clearly show that this worst-case does not always follow for many domains widely used to evaluate planning algorithms.

To avoid this blow up, yet keep the strong inference offered by the system of constraints (18), we introduce specific propagator that interfaces with CpSat precedences propagator and checks whether constraint (9c) is satisfied. The propagator activates whenever an assignment in the CDCL search fully decides the variables in input pin $in_{jk}$. We then check, for every slot $j^{\prime}$, $0$ $<$ $j^{\prime}$ $<$ $j$, whether the current assignment has fully decided some output pin $out_{j^{\prime}l}$, and proceed to evaluate the $\mathrm{persistence}$ predicate in Equation (9) on the assignment. If the former evaluates to false, we have a conflict between the assignment and constraint (9c). We then generate the following blocking clause or reason to explain it

where $\varphi$ formulae are the conjunction of equality atoms that bind variables in pins to the values in the current assignment. $spt_{jk_{1}}$ is the first element (variable) in $spt_{jk}$ and $LB$ is a function provided by CpSat that allows to access the lower bound of the domain of a variable in constant time.

Searching for plans. Our algorithm for planning as satisfiability uses a strategy to find plans that is analogous to the notion of lookaheads in Approximate Dynamic Programming. Like in the classic algorithm described earlier in the paper, we generate a sequence of CSPs $T_{P,k_{1}}$, $T_{P,k_{2}}$, $\ldots$, $T_{P,k_{i}}$, $\ldots$ with $k_{0}=0$ and $k_{i}-k_{i-1}\geq 1$ for $i>0$.

To each $T_{P,k_{i}}$ we impose the Pseudo-Boolean objective

where $enabled_{j}$ are auxiliary Boolean variables which we use to “switch off” slots via constraints $\neg enabled_{j}$ $\rightarrow$ $act_{j}>|Act|$. If CpSat proves that the resulting optimization problem has finite optimal value $z$ then we know that $c^{*}=z$ and the search terminates as we have found an optimal plan. If CpSat finds an upper bound $z$, that is, a sequence of feasible solutions are found but it is not possible to prove optimality of the last one within the time limit set, then we know that $c^{*}\leq z$. If CpSat proves the tightest upper bound to be $\infty$ (e.g. the problem is unsatisfiable) then we have proved a deductive lower bound [15], as we know that $c^{*}>k_{i}$. In this last case, we repeat the process above with $TP_{k_{i+1}}$ until a solution is found, or the allowed time to search for plans is exhausted.

Benchmarks in planning are not expressed in FSTRIPS directly but in PDDL [20], a defacto abstract representation of a PPI used by the research community. PDDL is defined by the tuple $P=\left<{U,T,{\cal P},Act,s_{0},\gamma}\right>$, where $U$ is a set of objects, $T\in 2^{U}$ is a collection of types, ${\cal P}$ is a set of predicates, $Act$ is a set of action schemas, $s_{0}$ is the initial state, and $\gamma$ is goal formula. For a given predicate $\mathsf{P}\in{\cal P}$ of arity $d_{\mathsf{P}}$, there are two associated literals, the positive atom $\mathsf{P}(\bar{x})$ and negative atom $\neg\mathsf{P}(\bar{x})$, where $\bar{x}$ is tuple of variables $(x_{1},x_{2},\ldots,x_{d_{\mathsf{P}}})$, the domain of $x_{i}$ corresponds to a type $t_{i}\in T$. We denote $\max_{\mathsf{P}\in{\cal P}}d_{\mathsf{P}}$ as $K_{\mathsf{P}}$. A simple reformulation of PDDL planning task into FSTRIPS representation is to treat each predicate $\mathsf{P}\in{\cal P}$ as a Boolean function or a mapping, $f_{\mathsf{P}}:\mathrm{Dom}_{f_{\mathsf{P}}}\mapsto\mathrm{Co}_{f_{\mathsf{P}}}$, $\mathrm{Dom}_{f_{\mathsf{P}}}\subseteq t_{1}\times t_{2}\times,\ldots,\times t_{d_{\mathsf{P}}}$, $\mathrm{Co}_{f_{\mathsf{P}}}=\{\top,\bot\}$. Thus, $(f_{\mathsf{P}}(\bar{x})=\top)$ denotes $\mathsf{P}(\bar{x})$ and $(f_{\mathsf{P}}(\bar{x})=\bot)$ denotes $\neg\mathsf{P}(\bar{x})$. Mappings that go beyond Boolean functions can yield a more compact FSTRIPS representation for CP. Hence, we present in this section a novel method to derive a more concise functional transformation of predicates ${\cal P}$.

Any function $f:\mathrm{Dom}_{f}\mapsto\mathrm{Co}_{f}$ has an associated binary relation, a mapping, ${\cal R}_{f}:=\{(x,y)\mid f(x)=y,\ x\in\mathrm{Dom}_{x},y\in\mathrm{Dom}_{y}\}$. A predicate $\mathsf{P}\in{\cal P}$ of arity $2$ also has an associated binary relation, ${\cal R}_{\mathsf{P}}:=\{(x,y)\mid\mathsf{P}(x,y),\ x\in\mathrm{Dom}_{x},y\in\mathrm{Dom}_{y}\}$. If the relation ${\cal R}_{\mathsf{P}}$ is a mapping, then we can create a more concise transformation, i.e. $f_{\mathsf{P}}:\mathrm{Dom}_{x}\mapsto\mathrm{Dom}_{y}$, instead of $f_{\mathsf{P}}:\mathrm{Dom}_{x}\times\mathrm{Dom}_{y}\mapsto\{\top,\bot\}$. Moreover, $0$-ary, $1$-ary and $n$-ary predicates can all be mapped into the binary case without loss of generality, i.e. $\mathsf{P}()$ can be substituted by $\mathsf{P}(c_{1},c_{2})$, $c_{1},c_{2}\in\mathrm{Dom}_{c},\mathrm{Dom}_{c}\cap U=\emptyset$, $\mathsf{P}(y)$ by $\mathsf{P}(c,y)$, and for $n\geq 2$, $\mathsf{P}(x,y)$ replaces the predicate $\mathsf{P}(u_{1},\ldots,u_{n})$, where $x$ is a tuple in the set of combinations of parameters of length $n-1$ and $y$ is the parameter which is excluded from $x$. For example, in the PDDL specification of visitall, $at$ is a $1$-ary predicate which represents the current position of the agent. We can map $at$ into the binary case by introducing a constant $A$, and then, transform it into a function as $at:\{A\}\mapsto C$ since the agent can take at most one position on the grid. Thus, for each predicate $\mathsf{P}\in{\cal P}$, there is an associated binary relation ${\cal R}_{\mathsf{P}}:=\{(x,y)\mid\mathsf{P}(x,y),x\in\mathrm{Dom}_{x},y\in\mathrm{Dom}_{y}\}$. There are two necessary and sufficient conditions for a binary relation to be a mapping, $(1)$ it is right-unique, and $(2)$ it is left-total. A binary relation ${\cal R}_{\mathsf{P}}$ is right unique iff $\forall\ x_{1},x_{2}\in\mathrm{Dom}_{x},y_{1},y_{2}\in\mathrm{Dom}_{y},\ \mathsf{P}(x_{1},y_{1})\land\mathsf{P}(x_{2},y_{2})\land(x_{1}=x_{2})\rightarrow(y_{1}=y_{2})$. It is left-total iff $\forall\ x\in\mathrm{Dom}_{x},\ \exists\ y\in\mathrm{Dom}_{y},\ \mathsf{P}(x,y)$. Since, the states $s\in S$ set the interpretation of predicate $\mathsf{P}$, we have to at-least prove that the right-unique and left-total conditions hold in $S^{R}_{P}$, the set of states reachable from $s_{0}$, to make a case for the more concise functional transformation.

A sufficient condition for the right-unique property to hold in all interpretations $s\in S_{P}^{R}$ is that the negation of right-unique condition is false in $S^{R}_{P_{r}}\supseteq S_{P}^{R}$, where $P_{r}$ is a relaxation of $P$. Thus, we can do a relaxed reachability analysis of the formula $\psi_{\mathsf{P}}:=\exists x_{1},x_{2},y_{1},y_{2},\ \mathsf{P}(x_{1},y_{1})\land\mathsf{P}(x_{2},y_{2})\land(x_{1}=x_{2})\land(y_{1}\neq y_{2})$ to test whether the right-unique condition holds for all $s\in S_{P_{r}}^{R}$, i.e. the right-unique property holds if $\psi_{\mathsf{P}}$ is unreachable in $P_{r}$. The relaxation is important since checking the reachability of the condition in $P$ is as hard as solving the problem itself. To this end, we extend the $h^{m}$ heuristic [17], which is an admissible approximation of the optimal heuristic function $h^{*}$, to the first order logic existential formula of the form $\psi:=\exists\bar{x},\psi^{L}\land\psi^{EQ}$, where $\bar{x}:=(x_{1},x_{2},\ldots,x_{n})$ is a vector of parameters, $\psi^{L}$ is a conjunction of literals whose interpretation is set by the states $s\in S^{R}_{\Pi}$, and $\psi^{EQ}$ is an equality-logic formula²²2See the definition of $h^{m}$ over first-order logic formulae in the Appendix A.. We then use the extension of $h^{m}$ to test the reachability of the formula $\psi_{\mathsf{P}}$, i.e. if $h^{m}(\psi_{\mathsf{P}})=\infty$, then $\psi_{\mathsf{P}}$ is unreachable, and hence, the right unique condition holds in all interpretations $s\in S_{P}^{R}$ of $\mathsf{P}$. Also, we note that, if ${\cal R}_{\mathsf{P}}$ is right-unique, the left-total property is trivial to satisfy. For each $x\in\mathrm{Dom}_{x}$, if $\not\exists y\in\mathrm{Dom}_{y},\ \mathsf{P}(x,y)$, then we map $x$ to $\Box$, a dummy constant symbol.