Analysis of Planning Instances Without Search

Abstract

In order to prove classical planning instances unsolvable, state-of-the-art planners resort to a state space search. However, we show here that an incomplete, yet computationally efficient criterion is sometimes sufficient to immediately identify as unsolvable a wide range of planning instances. Based on linear and integer programming, we show in this paper how it can be leveraged, should it fail at first. This criterion is the keystone of various techniques we propose to rewrite and enhance the STRIPS model, so as to gather new information about it. If the newly found bits of information is not sufficient to identify the instance as unsolvable, they still constitute human-readable bits of information that can provide additional insight on the planning instance.

1. Introduction

Current classical planners go through a search phase, with the aim of finding a sequence of actions that satisfies a given goal. They often start with the assumption that such a plan exists, and for the past few decades, significant work has been done on designing more and more efficient techniques to find solution plans. However, various reasons may lead to an instance not admitting any solution. Search-based planners will then explore the state space in its entirety, potentially cutting branches of the search tree, until they realize no plan can be found. The detection of states that cannot lead to any solution is often a byproduct of the heuristics used during search: an infinite heuristic value for an admissible heuristic is a synonym of a dead-end state.

This is why in recent years, there has been a renewed interest in detecting unsolvable planning instances, as illustrated by the 2016 Unsolvability International Planning Competition (Unsolvability IPC). Various techniques have been developed in the last couple of decades, such as dead-end formulas (Cserna et al., 2018) and traps (Lipovetzky et al., 2016; Steinmetz et al., 2022). However, all of these methods are based on the exploration of the state space.

In this article, we propose to leverage a linear programming (LP)- and integer programming (IP)-based criterion to iteratively refine a planning model, to show its unsolvability. The criterion we use is fast to compute and allows us to quickly recognize a wide range of unsolvable planning instances. However, it is not complete, in the sense that it may not recognize some unsolvable instances as such. Nevertheless, we show how to use it to iteratively refine the planning model, and keep gathering additional information about the instance with the aim that our procedure can detect that it is unsolvable.

Most of our techniques to gather information are based on a simple schema: after testing the solvability of planning instances ${\mathrm{\Pi }}^{\prime }$ that is derived from the initial planning problem $\mathrm{\Pi }$ given as input, we deduce additional information about the problem $\mathrm{\Pi }$ if ${\mathrm{\Pi }}^{\prime }$ is unsolvable. For instance, if the instance ${\mathrm{\Pi }}^{\prime }$ , which is $\mathrm{\Pi }$ where operator $a$ was removed, is proven to be unsolvable, then it means that $a$ appears in all solution plans of $\mathrm{\Pi }$ . In the case where one can efficiently detect some unsolvable planning instances (but not all), then lots of such derived instances ${\mathrm{\Pi }}^{\prime }$ can be tested successfully. As the criterion we use is incomplete but fast, even though it often fails to detect unsolvable instances, it still manages to help gather new information, as lots of tests can be made in a reasonable time. As more and more information is known about the planning instance, the mathematical program on which the criterion is based can also be enriched with the new knowledge, so that it can detect additional unsolvable instances.

More generally, being able to detect planning instances that have no solution can have various applications in itself. For instance, consider the case where an instance models the attacks that a malicious user may perform on a system, with the goal of accessing restricted data. Finding that no sequence of actions may achieve this shows that the system is secure.

The paper is organized as follows. In Section 2, we introduce our formalism and notations for classical planning. In Section 3, we present the mathematical-programming-based criterion we use throughout this paper. In Section 4, we show how to design tests to gather new information about a planning model. In Section 5, we report our experimental trials on standard sets of benchmarks. Section 6 reviews related work, while Section 7 is devoted to a discussion and perspectives on our findings.

2. Background

2.1. STRIPS Planning Instance

A STRIPS planning instance is a tuple $\mathrm{\Pi }=⟨F,I,O,G⟩$ such that $F$ is a set of propositional variables called fluents, and $I$ is a set of fluents of $F$ , called the initial state. $G$ is a set of literals of $F$ , such that no literal appears at the same time as its negation, and is called the goal. We will denote $G^{+}$ the set of positive literals of $G$ , and $G^{-}$ the set of fluents that appear negated in $G$ . Finally, $O$ is a set of operators: operators $a\in O$ are of the form $a=⟨\mathsf{\text{pre}}(a),\mathsf{\text{eff}}(a)⟩$ . $\mathsf{\text{pre}}(a)\subseteq F$ is the precondition of $a$ , which is a set of fluents. $\mathsf{\text{eff}}(a)$ is the effect of $a$ , and is a set of literals of $F$ . We will denote ${\mathsf{\text{eff}}}^{+}(a)=\{f\in F\mid f\in \mathsf{\text{eff}}(a)\}$ the set of positive effects of $a$ , and ${\mathsf{\text{eff}}}^{-}(a)=\{f\in F\mid \mathrm{\neg }f\in \mathsf{\text{eff}}(a)\}$ its negative effects.

Note that we define a version of STRIPS with negative goals. The original STRIPS formulation only specified positive goals, and is not any less expressive: any instance with negative goals can be translated, in polynomial time, into an equivalent instance without negative goals. We nonetheless allow negative goals in our formulation of STRIPS, since later in this paper we investigate the possibility of adding negative goals in order to strengthen a STRIPS instance. But one should keep in mind that most planning instances (and in particular, the ones used in our set of benchmarks) come with positive goals only: this is why we assume $G^{-}$ is empty, except in the section where we consider adding negative goals.

Something similar could be said for the preconditions of operators: standard STRIPS only defines positive preconditions, since any STRIPS instance with negative preconditions can be translated into an equivalent instance without negative preconditions in linear time (Geffner & Bonet, 2013). Some versions of STRIPS allow negative preconditions; however, in this case, disallowing negative preconditions makes the formulation of some of our criteria simpler, hence our choice to use this version of STRIPS.

Without loss of generality, we assume that for all operators $a$ , ${\mathsf{\text{eff}}}^{+}(a)\cap {\mathsf{\text{eff}}}^{-}(a)=\varnothing$ . In addition, we will also suppose that ${\mathsf{\text{eff}}}^{+}(a)\cap \mathsf{\text{pre}}(a)=\varnothing$ , otherwise the redundant fluents from the effects can be removed. Any planning instance that does not satisfy these criteria can be transformed, in polynomial time, into an equivalent instance that complies with them.

2.2. States and Plans

A state $s$ is an assignment of truth values to all fluents in $F$ . For notational convenience, we associate $s$ with the set of fluents of $F$ which are true in $s$ . An operator $a$ can be applied to states of $\mathrm{\Pi }$ that verify its preconditions. More formally, for any state $s$ , if $\mathsf{\text{pre}}(a)\subseteq s$ then we define the result of the application of $a$ to $s$ as $s[a]=(s\setminus {\mathsf{\text{eff}}}^{-}(a))\cup {\mathsf{\text{eff}}}^{+}(a)$ .

Given an instance $\mathrm{\Pi }=⟨F,I,O,G⟩$ , a plan is a sequence of operators $\pi =a_1,\dots ,a_k$ from $O$ such that there exists a sequence of states $s_0,\dots ,s_k$ , such that, for all $i\in 1,\dots ,k$ , the operator $a_i$ is applicable in $s_{i-1}$ , and that $s_i=s_{i-1}[a_i]$ . A plan is a solution plan if we have, in addition, $s_0=I$ , $G^{+}\subseteq s_k$ and $G^{-}\cap s_k=\varnothing$ . We say that a fluent $f$ is established (respectively, deleted) by some occurrence of an operator $a\in O$ in $\pi$ if $f$ is false (respectively, true) in some state $s_i$ , but true (respectively, false) after the application of $a$ , in state $s_{i+1}=s_i[a]$ . In the rest of this paper, we will refer to solution plans as simply plans.

3. Detecting Unsolvable Instances by LP

This section introduces two equivalent criteria that we use, and extend, to detect a planning instance’s unsolvability. These criteria are incomplete, in the sense that they cannot detect all unsolvable planning instances by themselves. However, they require very limited computational resources, and are fast to run, as they are based on LP or IP. We will show later how to leverage those properties in order to make the most of these criteria when they are not able to detect an instance’s unsolvability by themselves.

3.1. Potential-Based Argument

The first LP formulation that we worked with is based on the following argument. Suppose that we have a numerical function $\mathrm{\Phi }:F\to {\mathbb{R}}^{+}$ , that associates a potential to each fluent. We can then naturally define the potential of a state $s\subseteq 2^F$ as $\mathrm{\Phi }(s)=\sum _{f\in s}\mathrm{\Phi }(f)$ . If one can prove that all goal states have a higher potential than the initial state, but the application of any operator $a$ to any state $s$ leads to a state $s^{\prime }$ of lesser (or equal) potential, then the planning instance has no solution plan.

Such a function $\mathrm{\Phi }$ can be found thanks to the following observation. In any plan, the potential of a state $s^{\prime }$ solely depends on the previous state $s$ , and on the operator $a$ that was applied such that $s[a]=s^{\prime }$ . In this case, we will say that $a$ induced an increase in potential of $\mathrm{\Delta }{\mathrm{\Phi }}_a(s)=\mathrm{\Phi }(s^{\prime })-\mathrm{\Phi }(s)$ . One can remark that there exists an upper bound for $\mathrm{\Delta }{\mathrm{\Phi }}_a(s)$ , which does not depend on $s$ but only on $a$ . Indeed, in the limit case, all fluents $f\in {\mathsf{\text{eff}}}^{+}(a)$ are effectively established by $a$ , but no fluent $f^{\prime }\in {\mathsf{\text{eff}}}^{-}(a)$ is destroyed, except when $f^{\prime }\in {\mathsf{\text{eff}}}^{-}(a)\cap \mathsf{\text{pre}}(a)$ . Recall that we assume, without loss of generality, that ${\mathsf{\text{eff}}}^{+}(a)\cap \mathsf{\text{pre}}(a)=\varnothing$ .

More formally, let us consider two sets of operators, with regard to some fluent $f$ : on the one hand, the operators that will surely delete $f$ when applied, that we denote ${\mathit{S}\mathit{D}}_f$ ; on the other hand, the operators that could possibly add $f$ when applied, denoted ${\mathit{P}\mathit{A}}_f$ . The latter are operators that may establish $f$ in the resulting state $s^{\prime }$ depending on whether $f$ is false in the previous state $s$ or not. More formally, the sets are defined as follows:

$\bullet$

${\mathit{S}\mathit{D}}_f=\{a\mid f\in {\mathsf{\text{eff}}}^{-}(a)\cap \mathsf{\text{pre}}(a)\}$ .

$\bullet$

${\mathit{P}\mathit{A}}_f=\{a\mid f\in {\mathsf{\text{eff}}}^{+}(a)\}$ .

This leads to the following inequality, which models the limit case previously presented. This effectively gives us an upper bound on the change of potential induced by $a$ from any state $s$ , which we denote $\mathrm{\Delta }{\mathrm{\Phi }}_a(s)$ . Observe that the right-hand side is independent of $s$ .

$$\mathrm{\Delta }{\mathrm{\Phi }}_a(s)\le \sum _{f\in {\mathsf{\text{eff}}}^{+}(a)}\mathrm{\Phi }(f)-\sum _{f\in {\mathsf{\text{eff}}}^{-}(a)\cap \mathsf{\text{pre}}(a)}\mathrm{\Phi }(f).$$

Now suppose that, for all operators $a$ , the right-hand side of the previous inequality is negative. It means that applying any operator makes the potential of the state decrease. As a consequence, states that have a higher potential than the initial state cannot be reached. Note that, as the potential of a state is only determined by the potential of the fluents that are true in this state, and all potentials are positive, $\mathrm{\Phi }(G^{+})$ is a lower bound for the potential of any goal state. Thus, if we also have that $\mathrm{\Phi }(G^{+})>\mathrm{\Phi }(I)$ , then the planning instance has no solution.

The only remaining issue is to check whether such a potential function $\mathrm{\Phi }$ exists. As $\mathrm{\Phi }$ is only determined by its values on the various fluents, this can be done with the following set of equations, with the set of variables $V=\{x_f\mid f\in F\}$ . Intuitively, $x_f$ corresponds to the potential $\mathrm{\Phi }(f)$ of $f$ .

Linear Program 1

Let $\mathrm{\Pi }=⟨F,I,O,G⟩$ be a planning instance. Define ${\mathcal{L}}_{\mathrm{\Pi }}^{pot}$ to have the following variables and constraints:

Variables: $\{x_f\mid f\in F\}$ .

Constraints:

$$\begin{array}{rl}\sum _{f\in G^{+}}{x}_f-\sum _{f\in I}{x}_f& >0,\end{array}$$

(1)

$$\begin{array}{rl}\sum _{f\in {\mathit{e}\mathit{f}\mathit{f}}^{+}(a)}{x}_f-\sum _{f\in {\mathit{e}\mathit{f}\mathit{f}}^{-}(a)\cap pre(a)}{x}_f& \le 0(a\in O)\end{array}$$

(2)

$$\begin{array}{rl}{x}_f& \ge 0(f\in F).\end{array}$$

(3)

Note that the set of constraints above is not a linear program per se, since it contains the strict inequality (1). However, it can be easily reduced to an actual linear program (for instance by replacing $>0$ by $\ge 1$ in (1)), and we present it as such for the sake of simplicity.

The following proposition follows from the discussion further above.

Proposition 1

Let $\mathrm{\Pi }$ be a STRIPS instance. Suppose that there exists a solution for the Linear Program 1. Then $\mathrm{\Pi }$ has no solution.

Proof.

Suppose that the hypothesis is true, and let $x_f$ ( $f\in F$ ) be a solution to Linear Program 1. As outlined in the discussion above, for each state $s$ , we associate the potential:

$$\mathrm{\Phi }(s)=\sum _{f\in s}{x}_f.$$

A solution plan must be valid for any initial state satisfying the initial condition and, in particular, for the initial state $s_0=I$ in which all fluents not in $I$ are false. Equation (1) tells us that $\mathrm{\Phi }(s_0)<\mathrm{\Phi }(s_k)$ at (any) goal state $s_k$ . If an operator $a\in O$ transforms state $s_{i-1}$ into state $s_i$ , then the maximum of $\mathrm{\Delta }{\mathrm{\Phi }}_a(s_{i-1})=\mathrm{\Phi }(s_i)-\mathrm{\Phi }(s_{i-1})$ , that is the net gain in the score, is attained when each positive effect $f\in {\mathit{e}\mathit{f}\mathit{f}}^{+}(a)$ is established (i.e., $f$ was not already true in $s_{i-1}$ ) and only those negative effects $f\in {\mathit{e}\mathit{f}\mathit{f}}^{-}(a)\cap pre(a)$ actually occur (i.e., negative effects $f\in {\mathit{e}\mathit{f}\mathit{f}}^{-}(a)\setminus pre(a)$ were already false in $s_{i-1}$ ). Equations (2) and (3) tell us that $\mathrm{\Phi }(s_{i-1})\ge \mathrm{\Phi }(s_i)$ for any consecutive states in a solution plan $s_0,\dots ,s_k$ . Clearly a goal state $s_k$ can never be reached since potentials of all states reachable from $s_0$ remain less than or equal to $\mathrm{\Phi }(s_0)$ .

Note that the converse of Proposition 1 is not true: not all unsolvable planning instances are detected by the criterion we propose.

Our definition of potential is reminiscent of potential heuristics, as introduced by Pommerening et al. (2015): facts are assigned numerical values, also called potentials, which uniquely and compactly define the potentials of all states of the planning instance. In their paper, the authors do so in order to synthesize a heuristic $h^{\text{pot}}$ , which is a linear combination of these potentials. They show that the consistency, the goal awareness, and thus the admissibility of the heuristic can all be expressed in terms of linear constraints, and potential heuristics are thus easy to synthesize through a linear program.

The main differences with our work lie in two points. First, potential heuristics are defined for planning tasks in Finite Domain Representation (FDR), where variables describing states are not binary, but can have domains of arbitrary size. They are then, in theory, slightly more general than our formulation. Second, while potentials in Pommerening et al. (2015) range over $\mathbb{R}$ , we only allow positive potentials for fluents. These two points, combined, allow us to have a simple formulation for our linear program, without requiring the operators to be in transition normal form (TNF). TNF requires every fluent found in the effects of an action $a$ to also appear in its precondition. In FDR, TNF can be achieved through a transformation of any noncompliant action into a set of equivalent actions. When the planning instance cannot be transformed into an equivalent instance in TNF of reasonable size, the synthesis of potential heuristics, as well as their use, becomes slightly more tedious. In our work, we propose a criterion based on potentials that does not require a planning instance to be in TNF, and we rely on STRIPS and the positivity of the fluents’ potentials for this.

3.2. Dual Linear Program

The linear program presented in the previous section is hard to interpret, as the concept of potential we introduced has no reality outside of the criterion. However, we show in this section how to transform it into another program that can equivalently allow us to detect some unsolvable instances, but whose result is easier to interpret.

To this effect, we resort to Farkas’s lemma. Farkas’s lemma is related to the well-known fact that in LP, the primal problem is feasible iff the dual problem is feasible. One version of this lemma states that exactly one of the following sets of equations has a solution: either (1) $\mathbf{\text{Ay}}\ge \mathbf{\text{d}}$ where $\mathbf{\text{y}}\ge 0$ , or (2) ${\mathbf{\text{A}}}^t\mathbf{\text{x}}\le 0$ and ${\mathbf{\text{d}}}^t\mathbf{\text{x}}>0$ where $\mathbf{\text{x}}\ge 0$ , where $\mathbf{\text{A}}$ is a matrix and $\mathbf{\text{x}},\mathbf{\text{y}}$ , and $\mathbf{\text{d}}$ vectors of the appropriate sizes. Let us consider the set of equations previously mentioned. Applying Farkas’s lemma, it has a solution iff the following system has no solution:

Linear Program 2 ( ${\displaystyle {\mathcal{L}}_{\mathrm{\Pi }}^{\mathit{\text{op}}}}$ )

Let $\mathrm{\Pi }=⟨F,I,O,G⟩$ be a planning instance. We define ${\displaystyle {\mathcal{L}}_{\mathrm{\Pi }}^{\mathit{\text{op}}}}$ as follows:

Variables: $V=$ $\{y_a\mid a\in O\}.$

Constraints $C$ :

$$\begin{array}{rl}\sum _{a\in {\mathit{P}\mathit{A}}_f}{y}_a-\sum _{a\in {\mathit{S}\mathit{D}}_f}{y}_a& \ge {\delta }_f^{-}(f\in F),\end{array}$$

(4)

$$\begin{array}{rl}{y}_a& \ge 0(a\in O),\end{array}$$

(5)

where ${\delta }_f^{-}={\mathbb{1}}_{G^{+}}(f)-{\mathbb{1}}_I(f)$ ( ${\mathbb{1}}_S(x)$ being the indicator function of set $S$ : ${\mathbb{1}}_S(x)=1$ if $x\in S$ , and 0 otherwise). In this context, the variable $y_a$ corresponds to the number of times operator $a$ is executed in some sequence of actions. Note that $y_a$ is positive, but not necessarily integral: this allows us to obtain a polynomial time relaxation of the STRIPS instance. Inequality (4) states that the number of possible establishments of $f$ minus the number of sure destructions of $f$ must be greater than or equal to ${\delta }_f^{-}$ . For instance, any fluent that appears positively in the goal but not in the initial state must be established as least once more than it is surely deleted in any plan. This dual version of our original linear program provides an alternative insight into the meaning of Proposition 1.

Lemma 1

Let $\mathrm{\Pi }=⟨F,I,O,G⟩$ be a planning instance, ${\displaystyle {\mathcal{L}}_{\mathrm{\Pi }}^{\mathit{\text{op}}}}$ as defined in Linear Program 2, and $\pi$ a solution plan for $\mathrm{\Pi }$ . Let us define $c_{\pi }:O\to \mathbb{N}$ to be the number of occurrences of operators of $O$ in $\pi$ . Then the assignment where, for all $a\in O$ , $y_a=c_{\pi }(a)$ , is a solution for ${\displaystyle {\mathcal{L}}_{\mathrm{\Pi }}^{\mathit{\text{op}}}}$ .

Proof.

Let $y_a$ ( $a\in O$ ) be as defined above. We will show that this is a solution for ${\displaystyle {\mathcal{L}}_{\mathrm{\Pi }}^{\mathit{\text{op}}}}$ . For each fluent $f$ , let us denote $e_f$ the number of times a fluent is established during the execution of $\pi$ , and $d_f$ the number of times it is destroyed. Recall that a fluent $f$ is established (respectively, deleted) by some occurrence of an operator $a\in O$ in $\pi$ if $f$ is false (respectively, true) before the application of the operator, but true (respectively, false) after. As $\pi$ is a solution plan, we have that:

$${\mathbb{1}}_{G^{+}}(f)-{\mathbb{1}}_I(f)\le e_f-d_f,$$

which can be shown by case disjunction on whether $f$ is in $I$ , $G^{+}$ , both or neither. We denote the inequalities above in a more concise way:

$${\delta }_f^{-}\le e_f-d_f.$$

In addition, in the extreme case, $f$ is established in $\pi$ at most as many times as there are occurrences of operators $a$ with $f\in {\mathsf{\text{eff}}}^{+}(a)$ . Hence,

$$e_f\le \sum _{a\in {\mathit{P}\mathit{A}}_f}{y}_a.$$

Similarly, the only operators $a\in O$ whose applications are guaranteed to destroy $f$ are such that $f\in {\mathsf{\text{pre}}}^{+}(a)\cap {\mathsf{\text{eff}}}^{-}(a)$ . Thus,

$$d_f\ge \sum _{a\in {\mathit{S}\mathit{D}}_f}{y}_a.$$

By combining both inequalities above, we have

$$\begin{array}{rl}{\delta }_f^{-}& \le e_f-d_f\\ & \le \sum _{a\in {\mathit{P}\mathit{A}}_f}{y}_a-\sum _{a\in {\mathit{S}\mathit{D}}_f}{y}_a,\end{array}$$

(6)

which means that $y_a$ ( $a\in O$ ) satisfies the constraints of the form of inequality (4) of ${\displaystyle {\mathcal{L}}_{\mathrm{\Pi }}^{\mathit{\text{op}}}}$ . As a consequence, as each $y_a$ is also positive, this is a solution to ${\displaystyle {\mathcal{L}}_{\mathrm{\Pi }}^{\mathit{\text{op}}}}$ .

The contrapositive of Lemma 1 is an alternative proof that, if ${\displaystyle {\mathcal{L}}_{\mathrm{\Pi }}^{\mathit{\text{op}}}}$ has no solution, then neither has $\mathrm{\Pi }$ . But it allows us to show more than that, as we have the following corollaries, that we use later on:

Corollary 1

If ${\displaystyle {\mathcal{L}}_{\mathrm{\Pi }}^{\mathit{\text{op}}}}$ has no integral solution, then the associated planning instance $\mathrm{\Pi }$ has no solution.

Proof.

The proof is immediate, as each operator appears an integral number of times in any solution plan $\pi$ .

Linear Program 2 is, in fact, an LP formulation of the state equation heuristic (Bonet, 2013), as previously shown in Pommerening et al. (2014). Its efficiency for detecting unsolvable planning instances has been shown before, as it is part of the Aidos planner, which won the Unsat IPC in 2016 (Seipp et al., 2016). The planner uses the LP formulation of the operator-counting heuristic to detect dead ends during search, working on a FDR of the instance. As a consequence, Aidos can detect every instance on which our criterion succeeds: when Linear Program 2 detects some instance $\mathrm{\Pi }$ as unsolvable, Aidos detects it too when exploring the initial state, since it is detected as a dead-end. When Linear Program 2 fails to detect an unsolvable instance, Aidos carries on with a search phase, aided by other components too, and has another chance at finding its unsolvability. In this case, we, however, do not resort to search, but show how to rewrite the model directly, and how to adapt the linear program accordingly.

Even though we introduced ${\displaystyle {\mathcal{L}}_{\mathrm{\Pi }}^{\mathit{\text{op}}}}$ as a linear program, we showed with Lemma 1 that one can also see it as an integer program. Solving an integer program is notoriously harder and slower than solving a linear program. As the integral solutions of the set of equations form a subset of its set of rational solutions, testing the solvability of the program over integral solutions is more likely to prove that the associated planning instance has no solution. Note that Farkas’s lemma does not apply in the integral case, hence the need for Lemma 1.

Since Linear Program 2 is the dual of Linear Program 1, and both programs can thus be used equivalently, we will only use Linear Program 2 in the rest of this paper. This is motivated by the fact that its formulation is more intuitive, since counting the occurrences of each operator in some plan is more tangible than associating an abstract potential to fluents. This allows us to reinvest Linear Program 2 in a variety of ways our initial formulation could not be reused, as will be shown later.

In the next section, we show that, in the case where the criterion introduced here fails, it can still be leveraged to gather additional information about $\mathrm{\Pi }$ .

4. Enhancing the Planning Problem

This section is dedicated to extending and adding information to the initial planning instance, mainly with the goal of proving it unsolvable. Through various methods, we either add or remove elements from the input model $\mathrm{\Pi }$ , or add information about $\mathrm{\Pi }$ that is not directly encodable into the model, but that can nevertheless still be included in the linear program or to make deductions. In order to do so, we will resort to two kinds of methods. In the first one, we build variations of $\mathrm{\Pi }$ so that, if one of these variations is deemed unsolvable through the previous linear program, then some additional information about $\mathrm{\Pi }$ can be deduced. In the second method, we do not consider per se a variation $\mathrm{\Pi }{}^{\prime }$ of $\mathrm{\Pi }$ , but we directly modify the linear program ${\displaystyle {\mathcal{L}}_{\mathrm{\Pi }}^{\mathit{\text{op}}}}$ associated with $\mathrm{\Pi }$ , so that if it is unsolvable, we can deduce new specific information about $\mathrm{\Pi }$ .

In the following, we call operation any such method. In the specific case where the operation answers a boolean question (e.g., Is an action removable?), we call it a test.

Note that ultimately, our goal is to detect unsolvable instances as such. As the set of solution plans is empty, its elements and itself satisfy various otherwise uncommon properties. For instance, any operator can be removed without altering the set of solutions. This is why we search for properties on elements of $\mathrm{\Pi }$ that are unlikely to appear in solvable instances, but that are reasonable in our setting.

In the rest of this section, we illustrate the previous general principles through various operations, that allow us to find new information about the planning instance given as input. As our goal is to detect unsolvable instances, in the following, we assume that the criterion could not detect, at first, that the instance is unsolvable and that we have to gather additional information in order to do so. This section concludes with a very simple example showing that, were the criterion to fail at first, it can still be used to prove an instance unsolvable.

4.1. Operator Counts and Landmarks

4.1.1. Landmark Detection

An operator $a\in O$ is a landmark for $\mathrm{\Pi }$ if $a$ occurs at least once in every solution plan. We maintain throughout our procedure a set $L\subseteq O$ of landmarks. With regard to our framework, we can test if an operator is a landmark by removing it from the model and testing if the instance is deemed unsolvable. More formally,

Lemma 2

Let $\mathrm{\Pi }=⟨F,I,O,G⟩$ and $a\in O$ . If ${\mathrm{\Pi }}_{\mid a}=⟨F,I,O\setminus \{a\},G⟩$ is unsolvable, then $a$ is a landmark.

This allows us to define the landmark detection test below, where ${\mathrm{\Pi }}_{\mid a}$ is as defined in Lemma 2.

4.1.2. Operator Count

One can generalize the notion of landmark, by counting the least number of times an operator appears in any solution plan. This is why we define the function $n^{-}:O\to \mathbb{N}$ , such that $n^{-}(a)$ is the least number of occurrences of action $a$ in any plan. Likewise, we define $n^{+}(a)$ as the maximum number of times $a$ appears in any plan. With this notation, $a\in O$ is a landmark iff $n^{-}(a)\ge 1$ .

Reasoning on the number of occurrences of some operator $a\in O$ can be done through Linear Program 2. Indeed, as the variables correspond to the number of occurrences of each operator in some sequence of actions, one only has to find lower and upper bounds for each variable $y_a$ in a solution of LP 2. This is why one can compute approximate values for $n^{+}(a)$ and $n^{-}(a)$ through an integral and optimization variation of LP 2, that we present below:

Integer Program 1 ( ${\displaystyle {\mathcal{L}}_{\mathrm{\Pi }}^{\mathit{\text{opt}}}(a)}$ )

Let $\mathrm{\Pi }=⟨F,I,O,G⟩$ be a planning instance, with $O=\{a_1,\dots ,a_m\}$ , and ${\displaystyle {\mathcal{L}}_{\mathrm{\Pi }}^{\mathit{\text{op}}}(V,C)}$ the associated Linear Program 2. For $a\in O$ , define ${\displaystyle {\mathcal{L}}_{\mathrm{\Pi }}^{\mathit{\text{opt}}}(a)}$ with the following variables and constraints:

Variables: $\{y_a\mid a\in O\}$ .

Constraints: Same as ${\displaystyle {\mathcal{L}}_{\mathrm{\Pi }}^{\mathit{\text{op}}}}$ except that the $y_a$ are integral.

Objective function $g:{\mathbb{N}}^m⟶\mathbb{N}$ :

$$g:y_{a_1},\dots ,y_{a_m}⟼y_a.$$

Lemma 3

Let $\mathrm{\Pi }$ be a planning instance, $a\in O$ an operator, and consider the integer program ${\displaystyle {\mathcal{L}}_{\mathrm{\Pi }}^{\mathit{\text{opt}}}(a)}$ with objective function $g$ . Then minimizing (respectively, maximizing) $g$ yields a lower (respectively, an upper) bound on the value of $n^{-}(a)$ (respectively, $n^{+}(a)$ ).

Proof.

The proof is a consequence of Lemma 1. We consider only the case where $g$ is minimized, as the proof for the other case is mostly identical. We denote $n_{\mathcal{L}}^{-}$ the value obtained by minimizing $g$ in ${\displaystyle {\mathcal{L}}_{\mathrm{\Pi }}^{\mathit{\text{opt}}}(a)}$ , where $a\in O$ is fixed. Suppose for a contradiction that $n^{-}(a)<n_{\mathcal{L}}^{-}$ . Then there exists a plan ${\pi }_a$ where $a$ occurs exactly $n^{-}(a)$ times, by definition. By Lemma 1, there exists a solution $Y_{{\pi }_a}$ for ${\displaystyle {\mathcal{L}}_{\mathrm{\Pi }}^{\mathit{\text{op}}}}$ where $Y_{{\pi }_a}(a)=n^{-}(a)<n_{\mathcal{L}}^{-}$ , which contradicts the optimality of $n_{\mathcal{L}}^{-}$ . Consequently, we have $n_{\mathcal{L}}^{-}\le n^{-}(a)$ .

This gives the following two tests.

In the rest of this paper, we will often use the notation $\mathsf{\text{OpCount}}(a)$ to refer to the successive application of ${\mathsf{\text{OpCount}}}^{-}(a)$ and ${\mathsf{\text{OpCount}}}^{+}(a)$ .

4.1.3. Using Operator Counts

We use the above tests to maintain estimates of the values of $n^{+}(a)$ and $n^{-}(a)$ . Once a nontrivial value for some $n^{+}(a)$ or some $n^{-}(a)$ has been found (i.e., a finite or nonzero value, respectively), one can reintroduce it into the linear program in the form of additional constraints. These constraints can be introduced in either ${\displaystyle {\mathcal{L}}_{\mathrm{\Pi }}^{\mathit{\text{op}}}}$ or ${\displaystyle {\mathcal{L}}_{\mathrm{\Pi }}^{\mathit{\text{opt}}}}$ , as both programs use the same sets of variables and constraints. As the variables of the linear programs correspond to the number of occurrences of operators in some plan, adding these constraints is straightforward for every $a\in O$ :

$$\begin{array}{rl}{y}_a& \le n^{+}(a),\\ y_a& \ge n^{-}(a).\end{array}$$

4.2. Operator Mutexes

Operator mutexes are unordered pairs of operators $\{a_1,a_2\}$ that cannot both appear in the same solution plan for $\mathrm{\Pi }$ . Such operators can still be part of some solution plan, on their own. As an illustration, suppose that $a_1$ and $a_2$ both include fluent $f$ in their respective positive preconditions and in their delete effects. If $f$ does not belong to the add effects of any operator of $\mathrm{\Pi }$ , then $a_1$ and $a_2$ are operators mutexes, as they are in competition for the nonrenewable resource $f$ . We maintain, throughout the execution of our procedure, a set $M_O$ of operator mutexes. One may think that operator mutexes do not occur often in planning models, as it is a property that concerns the set of solution plans as a whole. However, our aim is to detect unsolvable planning instances, which have by definition no solution plan: all pairs of operators are thus operator mutexes.

4.2.1. Finding Operator Mutexes Through LP

In order to check if two operators $a_1,a_2\in O$ are operator mutexes, it suffices to build the linear program ${\displaystyle {\mathcal{L}}_{\mathrm{\Pi }}^{\mathit{\text{opm}}}(a_1,a_2)}$ and check if it is feasible or not. In essence, ${\displaystyle {\mathcal{L}}_{\mathrm{\Pi }}^{\mathit{\text{opm}}}(a_1,a_2)}$ consists of the same set of constraints as ${\displaystyle {\mathcal{L}}_{\mathrm{\Pi }}^{\mathit{\text{op}}}}$ , except that it has the following additional constraints:

$$\begin{array}{rl}{y}_{a_1}& \ge 1,\end{array}$$

(7)

$$\begin{array}{rl}{y}_{a_2}& \ge 1.\end{array}$$

(8)

If ${\displaystyle {\mathcal{L}}_{\mathrm{\Pi }}^{\mathit{\text{opm}}}(a_1,a_2)}$ does not admit a solution, then it means that both operators cannot appear simultaneously in a plan, and thus are operator mutexes. Note that adding only one of the two inequalities above could also make the linear system unsolvable. In that case, this would mean that either $a_1$ or $a_2$ does not appear in any solution plan. This is something that we test before resorting to operator mutex tests. More generally, we check if some operators can be removed from the planning model. We present various techniques for doing so in the next section. Below, we introduce the notation for the test corresponding to the linear program we presented above:

4.2.2. Using Operator Mutexes

Including the information we have about operator mutexes in the linear program is straightforward. Knowing that $\{a_1,a_2\}$ is an operator mutex translates into barring certain solutions of ${\displaystyle {\mathcal{L}}_{\mathrm{\Pi }}^{\mathit{\text{op}}}}$ from appearing. Concretely, we wish to ensure that, when $y_{a_1}\ge 1$ , then $y_{a_2}=0$ , and conversely.

In order to achieve so, we introduce binary variables of the form $u_a\in \{0,1\}$ , for each operator $a\in O$ . We wish to enforce that $u_a=1$ whenever $y_a\ge 1$ . This can be done through the following set of constraints, which also bars operator mutexes from appearing.

$$\begin{array}{rl}{y}_a-n^{+}(a)\cdot u_a& \le 0(a\in O),\end{array}$$

(9)

$$\begin{array}{rl}{u}_{a_1}+u_{a_2}& \le 1(\{a_1,a_2\}\in M_O).\end{array}$$

(10)

4.3. Detection of Removable Actions

This section is concerned with finding operators $a\in O$ that never appear in any solution plan. Even though some such operators can be detected statically by the parser that we use, some others require additional computation. We present various techniques that allow us to detect if an operator can be immediately removed from the planning instance, without altering its set of solutions.

4.3.1. Through a Modification of the Linear Program

We start by extending ${\displaystyle {\mathcal{L}}_{\mathrm{\Pi }}^{\mathit{\text{op}}}}$ into ${\displaystyle {\mathcal{L}}_{\mathrm{\Pi }}^{\mathit{\text{ro}}}(a)}$ through the addition of the constraint $y_a\ge 1$ . If ${\displaystyle {\mathcal{L}}_{\mathrm{\Pi }}^{\mathit{\text{ro}}}(a)}$ has no solution, then $\mathrm{\Pi }$ has no solution where $a$ occurs at least once and $a$ can thus be removed from the model.

We do not elaborate on this argument further, as it is a special case of the technique seen in Section 4.1. Indeed, it is equivalent to show that $n^{+}(a)=0$ , as it ensures that $a$ does not occur in any solution plan. However, this argument allows us to find removable operators that are not detected by a test proposed later in this subsection.

4.3.2. Unreachable Preconditions

A simple way to prove that some operator $a$ will never be part of any plan is to prove that no reachable state satisfies its precondition. This can be done by testing that the planning instance ${\mathrm{\Pi }}_a^{\mathsf{\text{pre}}}=⟨F,I,O,\mathsf{\text{pre}}(a)⟩$ is unsolvable.

Removing some operators relaxes the linear program ${\displaystyle {\mathcal{L}}_{\mathrm{\Pi }}^{\mathit{\text{op}}}}$ , by the deletion of some of the associated variables and constraints. As a consequence, it can help prove some instances unsolvable. We introduce below the notation for the associated test:

4.3.3. Dead-End Operators

As it is possible to test whether or not there exists a reachable state where $a$ can be applied, it is natural to ask the opposite: does $a$ always lead to a dead-end, where no goal state can be reached?

This paragraph is dedicated to finding such operators, called dead-end operators. In order to do so, we need to restrict ourselves to the few fluents that appear in all states resulting from the application of $a$ , that is to say, the fluents that are true after $a$ is applied either because of the effects of $a$ or by inertia. Indeed, these fluents are the only ones for which we have enough information about their truth value to reason about. Let $F_a=\mathsf{\text{pre}}(a)\cup {\mathsf{\text{eff}}}^{+}(a)\cup {\mathsf{\text{eff}}}^{-}(a)$ . For any set $S$ of literals of $F$ , and $E\subseteq F$ , we note $S_{\mid E}$ the projection of $S$ over the fluents $E$ . Likewise, we denote $a_{\mid E}=⟨\mathsf{\text{pre}}(a{)}_{\mid E},\mathsf{\text{eff}}(a{)}_{\mid E}⟩$ the projection of operator $a$ over $E$ . For any $O^{\prime }\subseteq O$ , we also note $O_{\mid E}^{\prime }=\{a_{\mid E}\mid a\in O^{\prime }\}$ . This leads us to the following lemma:

Lemma 4

Let $\mathrm{\Pi }=⟨F,I,O,G⟩$ be a planning instance and ${\mathrm{\Pi }}_a^{\mathit{\text{post}}}=⟨F_a,I_a^{\mathit{\text{post}}},O_{\mid F_a},G_{\mid F_a}⟩$ , where $I_a^{\mathit{\text{post}}}=(\mathsf{\text{pre}}(a)\setminus {\mathsf{\text{eff}}}^{-}(a))\cup {\mathsf{\text{eff}}}^{+}(a)$ . If ${\mathrm{\Pi }}_a^{\mathit{\text{post}}}$ is unsolvable, then $a$ is a dead-end operator in $\mathrm{\Pi }$ .

Proof.

We prove the contrapositive: suppose that $a$ is not a dead-end operator in $\mathrm{\Pi }$ , and let us show that ${\mathrm{\Pi }}_a^{\mathit{\text{post}}}$ is solvable. Since $a$ is not a dead-end operator in $\mathrm{\Pi }$ , there exists a solution plan for $\mathrm{\Pi }$ where $a$ occurs at least once. Let $\pi =a_1\cdots a_k$ be such a plan, and let $i\in \{1,\dots ,k\}$ be the greatest index such that $a_i=a$ .

Then we show in what follows that ${\pi }^{\mathit{\text{post}}}=a_{i+1\mid F_a}\cdots a_{k\mid F_a}$ is a solution plan for ${\mathrm{\Pi }}_a^{\mathit{\text{post}}}$ , where ${\pi }^{\mathit{\text{post}}}$ is the empty plan when $i=k$ .

Let $s_0{s}_1\cdots s_k$ be the set of states associated with $\pi$ , and let us show by recurrence that the sequence of states associated with the plan ${\pi }^{\mathit{\text{post}}}$ in ${\mathrm{\Pi }}_a^{\mathit{\text{post}}}$ is $s_{i\mid F_a}\cdots s_{k\mid F_a}$ . First, we prove that $I_a^{\mathit{\text{post}}}=s_i\cap F_a$ . As $s_i$ results from the application of $a_i=a$ , we have that $I_a^{\mathit{\text{post}}}\subseteq s_i$ , and thus $I_a^{\mathit{\text{post}}}\subseteq s_i\cap F_a$ . Conversely, let us show that $s_i\cap F_a\subseteq I_a^{\mathit{\text{post}}}$ . Suppose that $f\in s_i\cap F_a$ , and let us proceed by case disjunction on $f\in F_a=\mathsf{\text{pre}}(a)\cup {\mathsf{\text{eff}}}^{+}(a)\cup {\mathsf{\text{eff}}}^{-}(a)$ . If $f\in {\mathsf{\text{eff}}}^{+}(a)$ , then $f\in I_a^{\mathit{\text{post}}}$ . Necessarily, we have that $f\notin {\mathsf{\text{eff}}}^{-}(a)$ , because otherwise $f\notin s_i$ as $s_i$ results from the application of $a$ . Then, we otherwise have $f\in \mathsf{\text{pre}}(a)\setminus {\mathsf{\text{eff}}}^{-}(a)$ , and thus, we have $f\in I_a^{\mathit{\text{post}}}$ . Hence, $I_a^{\mathit{\text{post}}}=s_i\cap F_a$ .

We have shown that the initial state of the sequence of states associated with ${\pi }^{\mathit{\text{post}}}$ is $s_{i\mid F_a}$ . To show the property for the remaining states, it suffices to check that, for any two states $s,s^{\prime }$ of $\mathrm{\Pi }$ , and for any operator $a^{\prime }\in O$ , if we have $s^{\prime }=s[a^{\prime }]$ , then $s_{\mid F_a}^{\prime }=s_{\mid F_a}[a_{\mid F_a}^{\prime }]$ . To see this, observe that $s_{\mid F_a}^{\prime }$ can be obtained in two different ways: 1) by applying $a$ to $s$ , and then projecting the resulting state $s^{\prime }$ over $F_a$ , or 2) by projecting $a$ and $s$ over $F_a$ , resulting in $a_{\mid F_a}$ and $s_{\mid F_a}$ , respectively, and then applying $a_{\mid F_a}$ to $s_{\mid F_a}$ .

Formally, this can be shown by successively applying the definition of the projection of $a^{\prime }$ over $F_a$ , denoted $a_{\mid F_a}^{\prime }$ , and the definition of $s_{\mid F_a}$ . We end up with the following:

$$\begin{array}{rl}{s}_{\mid F_a}[a_{\mid F_a}^{\prime }]& =(s_{\mid F_a}\setminus {\mathsf{\text{eff}}}^{-}(a_{\mid F_a}^{\prime }))\cup {\mathsf{\text{eff}}}^{+}(a_{\mid F_a}^{\prime })\\ & =(s_{\mid F_a}\setminus ({\mathsf{\text{eff}}}^{-}(a)\cap F_a))\cup ({\mathsf{\text{eff}}}^{+}(a)\cap F_a)\\ & =((s\cap F_a)\setminus ({\mathsf{\text{eff}}}^{-}(a)\cap F_a))\cup ({\mathsf{\text{eff}}}^{+}(a)\cap F_a)\\ & =((s\setminus {\mathsf{\text{eff}}}^{-}(a))\cup {\mathsf{\text{eff}}}^{+}(a))\cap F_a\\ & =s_{\mid F_a}^{\prime }.\end{array}$$

As a consequence, we immediately have that $s_{k\mid F_a}\subseteq G_{\mid F_a}$ , and ${\pi }^{\mathit{\text{post}}}$ is a solution plan for ${\mathrm{\Pi }}_a^{\mathit{\text{post}}}$ , which is what we sought to prove.

Experimental trials showed that no operator could be proved to be a dead-end operator. This is why, in Section 5, no results are reported about the above test. However, we still included this test to show that some very small problems derived from the input instance can be of interest.

4.4. Extended Goals

In this section, we propose various methods to find more precise goal states. More specifically, we try to add new literals to the goal, be they positive or negative. Suppose, for instance, that some fluent $f\in G^{+}$ can only be true if some other fluent $f^{\prime }$ is true. Then one can immediately add $f^{\prime }$ to $G^{+}$ . These more precise goals make the program richer and hence more likely to detect unsolvable instances. $G^{-}$ can also be extended in a similar way.

This can be done in our framework through the following simple observation. Let $f\in F$ , and ${\mathrm{\Pi }}_{+f}^G=⟨F,I,O,G\cup \{f\}⟩$ . If ${\mathrm{\Pi }}_{+f}^G$ is unsolvable, then $f$ can be added to the negative goals of $\mathrm{\Pi }$ . Indeed, no goal state $s_G$ such that $s_G\models f$ is reachable: necessarily, in any goal state $s_G$ , we have $s_G\models \mathrm{\neg }f$ . Conversely, let ${\mathrm{\Pi }}_{-f}^G=⟨F,I,O,G\cup \{\mathrm{\neg }f\}⟩$ . If ${\mathrm{\Pi }}_{-f}^G$ is unsolvable, then $f$ can be safely added to the goals of $\mathrm{\Pi }$ without changing the set of solutions.

There is, of course, a symmetrically equivalent test FPosGoal that we could have defined. However, in order to detect positive goals, we would need to test ${\mathrm{\Pi }}_{-f}^G$ , which has negative goals. These negative goals are not used in the formulation of Linear Program 2: as a consequence, our criterion would be powerless at detecting that ${\mathrm{\Pi }}_{-f}^G$ is unsolvable.

4.5. Fluent Mutexes and Unreachable Fluents

A fluent mutex is a set of fluents $M\subseteq F$ for which $s⊭M$ holds in all states $s$ reachable from the initial state $I$ . Some tests presented previously can be seen as testing whether some subset $M\subseteq F$ is a fluent mutex. Let us consider for instance the $\mathsf{\text{PreImp}}$ test presented in Section 4.3: for some operator $a\in O$ , checking that ${\mathrm{\Pi }}_a^{\mathsf{\text{pre}}}=⟨F,I,O,\mathsf{\text{pre}}(a)⟩$ is unsolvable (and thus that operator $a$ can be removed from the instance) is equivalent to checking that $\mathsf{\text{pre}}(a)$ is a mutex. However, our criterion allows us to check if any set of fluents $F^{\prime }\subseteq F$ is a mutex, by testing the unsolvability of ${\mathrm{\Pi }}_{F^{\prime }}^{\mathsf{\text{mut}}}=⟨F,I,O,F^{\prime }⟩$ .

The criterion does not detect all fluent mutexes, and each candidate set of fluents has to be tested individually. Thus, since there exists an exponential number of candidates to test, it is not possible to detect in reasonable time the ones that are within the reach of our method. Finding which sets are interesting to test is a problem in itself; even more so since one has to know how to make use of the newly found information that some $M\subseteq F$ is a mutex.

In the general case, we could not find a way to reinvest into the linear program the knowledge that a set of fluents is a mutex. Indeed, Linear Program 2 reasons over the number of times operators (have to) occur in a plan. As a consequence, we do not have any obvious way to reason about properties concerning states, which is precisely what fluent mutexes are. For that reason, we do not include in our routine computation of mutexes through our linear program, even though we can detect a range of fluent mutexes.

However, some fluents are always false, in the sense that no plan will ever establish them. We call the fluents unreachable fluents, and they can be detected with the same argument as above:

Even though these fluents appear very rarely, as will be shown in the experimental trials, it remains linear to test for all fluents whether they are unreachable or not: thus, the computational burden is significantly lower than for other fluent “mutexes.” When an unreachable fluent is detected, one can project the whole instance on fluents $F\setminus \{f\}$ , and remove the operators that have $f$ in their positive preconditions. Note, however, that any such operator $a$ would also be detected by test PreImp( $a$ ), which is more likely to succeed.

4.6. Example Instance Solved Through Model Refinement

In the rest of this section, we show that, when an instance is unsolvable but could not be detected as such by our criterion, then modifying the model using the above operations can still be enough to show the instance unsolvable.

Consider the instance $\mathrm{\Pi }=⟨F,I,O,G⟩$ , with:

$F=\{p,q,r\}$ ,

$I=\{p\}$ ,

$G=\{p,q\}$ ,

$O=\{a_1,a_2,a_3\}$ such that

–

$a_1=⟨\{p\},\{q,\mathrm{\neg }p\}⟩$ ,

–

$a_2=⟨\{q\},\{p,\mathrm{\neg }q\}⟩$ ,

–

$a_3=⟨\{r\},\{p,q\}⟩$ .

$\mathrm{\Pi }$ is clearly unsolvable, since $p$ and $q$ cannot be both true after the application of $a_1$ or $a_2$ , and $a_3$ can never be applied since its precondition cannot be established and is not true in $I$ .

The associated linear program ${\displaystyle {\mathcal{L}}_{\mathrm{\Pi }}^{\mathit{\text{op}}}}$ is the following, where $y_i$ is the variable associated with $a_i$ for any $i\in \{1,2,3\}$ , and the constraints of the form $y_i\ge 0$ are not explicitly written for the sake of concision:

$$\begin{array}{rl}-y_1+y_2+y_3& \ge 0,\end{array}$$

(11)

$$\begin{array}{rl}{y}_1-y_2+y_3& \ge 1,\end{array}$$

(12)

$$\begin{array}{rl}0& \ge 0,\end{array}$$

(13)

where equations (11), (12), and (13), respectively, correspond to fluents $p$ , $q$ , and $r$ .

The above linear program is solvable (consider for instance the solution where $y_1=y_2=0$ , and $y_3=1$ ), and as a consequence, our criterion fails to detect the instance as unsolvable.

However, let us apply the test $\mathsf{\text{PreImp}}(a_3)$ . This amounts to testing the unsolvability of ${\mathrm{\Pi }}_{a_3}^{\mathsf{\text{pre}}}=⟨F,I,O,\{r\}⟩$ , and the associated linear program is almost the same as the above, except that the right-hand sides of inequalities are adapted to the new goal:

$$\begin{array}{rl}-y_1+y_2+y_3& \ge 0,\\ y_1-y_2+y_3& \ge 0,\\ 0& \ge 1.\end{array}$$

Since the last equation is an immediate contradiction, ${\mathrm{\Pi }}_{a_3}^{\mathsf{\text{pre}}}$ is unsolvable, and the test $\mathsf{\text{PreImp}}(a_3)$ succeeds. As a consequence, $a_3$ can be removed from $\mathrm{\Pi }$ , and we note ${\mathrm{\Pi }}^{\prime }$ this new but equivalent instance. The linear program ${\displaystyle {\mathcal{L}}_{{\mathrm{\Pi }}^{\prime }}^{\mathit{\text{op}}}}$ associated with it is the following:

$$\begin{array}{rl}-y_1+y_2& \ge 0,\\ y_1-y_2& \ge 1,\\ 0& \ge 0,\end{array}$$

which does not admit any solution (the summation of the two upper equations leads to the contradiction $0\ge 1$ ). This shows in turn that ${\mathrm{\Pi }}^{\prime }$ is unsolvable, and thus that the original instance $\mathrm{\Pi }$ does not admit any solution plan either.

Note that the above sequence of operations could have been done equivalently with Linear Program 1 instead.

5. Experimental Evaluation

Our implementation was done in Python 3.10, basing ourselves on the Fast Downward parser (Helmert, 2006). We did not need the entire translator component, but only the functions concerned with the conversion of the instance into STRIPS. For linear programs, we resorted to the GLOP solver (Perron & Furnon, 2019), while integer programs were solved with Gurobi (Gurobi Optimization, LLC, 2023). We also used Google ORTools (Perron & Furnon, 2019) to interface between our program and the solvers. We ran our experiments on a machine running Rocky Linux 8.5, powered by an Intel Xeon E5-2667 v3 processor, with a 30-minute cutoff and using at most 16 GB of memory per instance. Our code is available online at https://github.com/arnaudlequen/MPRefinement.

In addition to the evaluation of the linear program, we also implemented a procedure based on the observations of Section 4. The main loop of this procedure consists of executing sequentially a predetermined list of operations and tests, until the instance is detected as unsolvable or the list is depleted. We elaborate further on this in Section 5.2.

We wished to evaluate our program on two different aspects: first, its ability to detect unsolvable instances, and second, its ability to find additional information when it could not conclude.

Our set of benchmarks consists of the unsolvable instances from the unplannability track of the International Planning Competition 2016 (Unsat IPC), for which we report our results on unsolvable instances. The Unsat IPC also includes solvable instances, which we tested our program on, as a sanity check, with success.

5.1. LP-Based Criteria

In this section, we show that our LP-based criterion suffices to detect a wide range of unsolvable planning instances. Our results are reported in detail in Table 1.

Table 1.

Summary of the Results Returned by the LP-Based Criterion, run on the Unsat Planning Competition Benchmark Set.

Set	Unsat	Total
bag-transport	19	29
bottleneck	25	25
cave-diving	1	25
chessboard-pebbling	23	23
over-tpp	2	30
pegsol-row5	14	15
Tetris	20	20
Remaining	0	180
Total	104	347

Note. Each line corresponds to a domain, which is a set of instances modeling similar problems. The first column reports instances on which our criterion succeeds, while the second column reports the total number of instances in the benchmark set. Domains for which no instance could be solved are summed up in the last line labeled Remaining.

In essence, about 30% of all instances of the Unsat IPC are almost immediately found to be unsolvable by the sole use of the criterion. These results, however, vary greatly from one domain to the other, in a very dichotomous fashion: either the domain is (almost) entirely solved through the criterion, or few to no instances are deemed unsolvable. In the case of domain bag-transport, which seems to be in between, all instances the criterion has been tried on are actually found to be unsolvable: however, as the last 10 instances are too big to be parsed, we could not run the test on them. We can also note that both LP- and IP-based criteria yield the same results and that solving the IP-based program did not allow us to detect more unsolvable instances than through the LP formulation.

Both programs are, however, very lightweight: for most domains, building and solving the program required less than a few seconds. In addition, for the vast majority of instances, the criteria required little more than a few tenths of a second to complete. This further justifies our use of the program in the iterative procedure that we present in the next section.

Our program fails entirely on some domains, where no instance can be solved. While this is often because our criterion simply fails to detect the instance’s unsolvability, this can also be due to the size of the model. This is the case of the bag-gripper, where the first instance has 5,681 fluents and 60,602 operators, which prevents us from building the associated linear program. In our assessments of the performances of the criteria, the limitation always came from memory. In this kind of situation, criteria that work on the FDR of the task might prove more efficient, since for the same problem, 317 facts resulting from 10 variables suffice to describe the first instance of bag-gripper (although 60602 operators are still needed). This may partly explain the success of other FDR-based criteria (Christen et al., 2022; Seipp et al., 2016) in some instances in which our criterion (and thus our procedure) entirely fails because of memory issues.

5.2. Iterative Refinement of the Model

In the case where the criterion could not immediately detect that an instance $\mathrm{\Pi }$ is unsolvable, one can resort to the several operations previously introduced. In addition, the order in which operations are executed is also critical. Consider for instance an operator $a$ that is both recognized as a landmark and as a removable operator by our operations. In the case where the operator is first removed, then it cannot be detected as a landmark, and we thus missed an opportunity to return that the instance is unsolvable. In the case where $a$ is first detected as a landmark, then our routine terminates successfully by detecting that the instance is unsolvable.

5.2.1. Sequences of Operations

We present below the different lists of operations that we chose. Note that all sequences start and end with a simple test of solvability with the criterion: initially with only the information contained in the STRIPS model, and then with the information that was incrementally gathered after each series of operations. The exact sequences of operations can be found in Appendix A.

Linear

This sequence comprises all tests and operations that are linear in the size of the instance, that is, that only require one argument. We tried to put first the tests that were the most likely to succeed, so that the following tests and operations that come after have more information to work with. We successively apply the following tests on all relevant elements, in that order: LMDet, PreImp, $\mathsf{\text{OpCount}}$ , FReach, and FNegGoal. By that, we mean that we run $\mathsf{\text{LMDet}}(a)$ for all $a\in O$ , then $\mathsf{\text{PreImp}}(a)$ for all $a\in O$ , etc.

Quadratic

In addition to the tests found in the linear sequence, the quadratic sequence has a sequence of operator mutexes tests OpMut, which comes right after the linear sequence’s operations. There exists a quadratic (in the size of the instance) number of such tests, as one has to consider every pair of operators successively. Even though the linear sequence is itself costly in terms of computation, it still builds fewer linear programs than the operator mutexes tests alone.

OperatorPreImpossible

As will be reported later, the PreImp tests that check an operator’s reachability are our most successful ones. We wished to gauge the time it requires and its possible impact on the model by itself.

OperatorCount

This sequence consists of finding lower bounds on the number of times each operator has to appear in any plan, and then upper bounds on the number of times each operator can appear in any plan. It aims to show that a linear number of integer programs to optimize can be done in a reasonable time, while also providing interesting information.

5.2.2. Results

We present our results below. As we prune out instances that can be immediately identified as unsolvable, domains that are immediately found unsolvable by the criterion are not reported.

Linear sequence

Table 2 shows statistics for the linear sequence. The main goal of our routine was to extract additional information from the model, either to directly prove the instance unsolvable, or so that another procedure that comes after can show the instance unsolvable more easily. We could indeed notice that our algorithm was sometimes enough to detect unsolvable instances that are otherwise not detected as such by the criterion. There are few examples of such instances (about 9.5% of the entire benchmark set), and they are grouped in only two domains (cave-diving and pegsol). Nonetheless, they suffice to show that a well-chosen sequence of operations can sometimes replace a search and that our work paves the way for further research in that regard.

Table 2.

Statistics for the Linear Sequence.

		Operators			Others
Set	Diff.	PreImp	OpCount	Rem.	LMDet	FReach	FNegGoal
cave-diving (13/24)	$+$ 11	10.0%	14.1%	10.4%	1.1%	4.8%	3.0%
diagnosis (19/20)	0	0%	57.0%	11.6%	18.3%	4.6%	17.6%
doc-transfer (5/20)	0	13.0%	26.4%	27.9%	1.7%	0.0%	39.8%
over-nomystery (2/24)	0	33.4%	25.7%	34.8%	2.1%	0%	7.4%
over-rovers (8/20)	0	27.9%	17.2%	29.3%	0%	<0.1%	0%
over-tpp (6/29)	0	7.4%	54.8%	24.7%	0.3%	0.3%	0%
pegsol (24/30)	+24	13.6%	N/A	13.6%	0.8%	N/A	N/A
sliding-tiles (20/20)	0	0%	0%	0%	0%	0%	69.2%

Note. The first column with the name of the domain also reports the total number of instances for which the procedure terminated entirely within the time and memory limits, out of the total number of instances that constitute the benchmark set that were not solved by the criterion alone. The “Difference” (Diff.) column shows the number of instances that could be found unsolvable during the execution of the procedure, compared to the single use of the criterion reported in Table 1. For example, out of the 25 cave-diving instances in the benchmark set, 24 were not solved by the criterion alone: out of these 24, the Linear procedure terminated on 13 instances, ran out of time on the others, and found 11 instances to be insolvable. The next set of columns shows stats for operations related to the deletion of operators. The first pair of columns show the percentage of success of each test ( $\mathsf{\text{OpCount}}$ comprising both ${\mathsf{\text{OpCount}}}^{+}$ and ${\mathsf{\text{OpCount}}}^{-}$ ), that is, the percentage of such tests that brought new information on the problem. The last column of the set shows the average total percentage of operators removed at the end of the sequence of tests. The last three columns show the percentage of success of three other tests. N/A values indicate that no such test was performed as the program terminated before.

In the cases where our procedure could not conclude, it still manages to gather valuable information about the planning instance. For example, on some domains, almost a third of all operators are pruned on average, among instances on which our procedure terminates.

The termination of our procedure is, however, the main issue of this sequence of operations, which is too computationally costly, and often stops early because of the time and memory limits imposed. In some domains, very few instances could be run through the entire sequence of operations: such domains include over-nomystery, where this sequence terminated on only two instances out of the 24 that could be parsed.

Quadratic sequence

Table 3 shows statistics for the quadratic sequence. As the first part of the quadratic sequence consists of the exact same sequence of operations as the linear sequence, there are at least as many instances solved by the quadratic sequence as by the linear sequence. This is why domains cave-diving and pegsol only exhibit instances that are entirely solved: our procedure detects these instances as unsolvable before reaching the $\mathsf{\text{OpMut}}$ tests (and then running out of time, in the case of cave-diving).

Table 3.

Statistics for the Quadratic Sequence.

		Operator mutexes
Set	Diff.	Av. mut/op	Success %	Av. $|O|$
cave-diving (11/24)	+11	N/A	N/A	1113
diagnosis (15/20)	0	4.8	3.6%	136
over-rovers (3/20)	0	8.2	6.2%	313
over-tpp (1/29)	0	0.8	<0.1%	1675
pegsol (24/30)	+24	N/A	N/A	77
sliding-tiles (10/20)	0	0	0%	193

Note. The number in parenthesis in each row indicates the instances the sequence terminated on, out of the total number of instances that constitute the benchmark set that were not solved by the criterion alone. As in Table 2, the Diff. column reports the instances found unsolvable by our routine, but on which the criterion failed to conclude by itself. The second column reports the average number of mutexes an operator finds itself in, and the third column reports the average percentage of success of $\mathsf{\text{OpMut}}$ tests, that is, the average percentages of tests that led to the finding of a new mutex. This latter column could also be interpreted as the average proportion of operators that are found to be mutex with another fixed operator. The last column reports the average number of operators per instance. Note that our reports concern far fewer instances than for the linear sequence, as the computational cost is significantly greater for the sequence reported here. Domains document-transfer and over-nomystery are not reported as no instance finished before the cutoff.

In general, the use of a quadratic number of operations quickly becomes problematic: compared to the linear sequence, the quadratic sequence can be run in its entirety on significantly fewer instances. In addition, very few tests are actually successful, as even with the most receptive instances, only a few percent of all tests succeed. However, the main issue with our sequence of operations is that it considers all pairs of operators, and checks if they can be marked as mutexes. The quadratic number of such tests is then responsible for the computational cost of the sequence, but the test in itself remains an integer program that can be solved almost instantly.

Yet, even if we were to find operators mutexes, they would be hard to reinvest in the linear program. Indeed, to be included in the linear program, an operator mutex $\{a_1,a_2\}$ requires that $n^{+}(a_1)$ and $n^{+}(a_2)$ are finite (see equation (9)), which is common but not always the case, as reported in Table 5. As very few pairs of operators are detected as mutexes, the next logical step to make the most of operator mutexes is to more efficiently choose which pairs to test, to avoid performing unpromising tests.

Individual Tests

Tables 4 and 5 summarize the statistics for the other sequences, which mostly consist of a series of one or two of the same operations. However, we do not report comprehensive results for all remaining sequences: indeed, in the case of the OperatorDeadLock sequence, no test answered positively, and no dead-end operator could be found.

Table 4.

Performances of the Operator PreImpossible Sequence.

		OperatorPreImpossible
Set	Diff.	Removed	Time (s)
bag-barman (4/20)	0	77.2%	1177.8
cave-diving (16/24)	+4	6.5 $\mathrm{\%}$	147.8
diagnosis (20/20)	0	0%	6.4
document-transfer (13/20)	0	0%	475.7
over-nomystery (10/24)	0	18.8 $\mathrm{\%}$	587.8
over-rovers (11/20)	0	21.9 $\mathrm{\%}$	370.2
over-tpp (12/29)	0	<0.1 $\mathrm{\%}$	268.1
pegsol (24/30)	+6	16.4 $\mathrm{\%}$	0.6
sliding-tiles (20/20)	0	0%	5.6

Note. The number in parenthesis in each row indicates the instances the sequence terminated on, out of the total number of instances that constitute the benchmark set that was not solved by the criterion alone. The “Diff.” column shows the number of instances solved thanks to the iterative refinement, the “Removed” column shows the average percentage of operators that could be removed thanks to the operation, and the “Time” column shows, in seconds, the average time per instance.

Table 5.

Performances of the OperatorCount Sequence.

		OperatorCount
Set	Diff.	${\mathsf{\text{OpCount}}}^{-}$	${\mathsf{\text{OpCount}}}^{+}$	Removed	Time (s)
bag-barman (0/20)	–	–	–	–	–
cave-diving (16/24)	0	0.9%	28.0%	7.0%	329.3
diagnosis (20/20)	0	16.9%	96.3%	19.5%	91.6
document-transfer (8/20)	0	1.7%	50.7%	29.8%	643.2
over-nomystery (3/24)	0	1.4%	87.2%	3.9%	746.2
over-rovers (9/20)	0	0%	62.4%	5.2%	455.1
over-tpp (7/29)	0	0.3%	65.4%	20.2%	428.8
pegsol (24/30)	+22	0%	8.2%	3.0%	0.51
sliding-tiles (20/20)	0	0%	0%	0%	19.4

Note. The number in parenthesis in each row indicates the instances the sequence terminated on, out of the total number of instances that constitute the benchmark set that was not solved by the criterion alone. The Diff. column shows the number of instances solved thanks to the iterative refinement. ${\mathsf{\text{OpCount}}}^{-}$ and ${\mathsf{\text{OpCount}}}^{+}$ columns report the average percentage of success of their respective operations, that is, the average percentages of tests that discovered some new, nontrivial information. The “Removed” column shows the average percentage of operators that could be removed thanks to the ${\mathsf{\text{OpCount}}}^{+}$ operations. The “Time” column shows, in seconds, the average time per instance.

Nonetheless, the results for the other sequences of operations are encouraging. Be it for the sequence centered on PreImp or the one focused on OpCount operations, a significant proportion of operators could be removed. In some cases, it suffices to show that the instance was not solvable, as is the case for the cave-diving or pegsol domains. However, the time required for the computation is significant, which is discussed in the next section.

An interesting property of our $\mathsf{\text{OpCount}}$ tests is that they do not always return $0$ , $1$ , or $+\mathrm{\infty }$ : they sometimes find that some operator $a$ can be applied at most $c$ times, where $c$ is an integer such that $c\ge 2$ .

Note that these sequences of tests are not as powerful as the linear sequence, when it comes to detecting unsolvable instances. This seems to indicate that the combination of different kinds of operations is crucial to draw conclusions, and studying their interactions is crucial in designing more powerful sequences.

6. Related Work

The surge in interest for unsolvability detection, in the last decade, has been embodied by the first Unsolvability Planning Competition in 2016. The competition saw various adaptations of techniques that have shown themselves efficient for finding plans, in a state space search. Such methods include heuristics specifically tailored for unsolvability detection, such as a Merge & Shrink-based heuristic (Helmert et al., 2014) (which precedes the competition). Such heuristics rely on abstractions that do not preserve distance, but merely solvability.

Another heuristic that was successfully adapted was the operator-counting heuristic (Bonet, 2013; Pommerening et al., 2014; Van Den Briel et al., 2007). The heuristic is based on a relaxation of the orderings of the operators. Previous works showed that it admits an LP formulation, similar to the Linear Program 2 or the Integer Program 1 that we propose. However, while we only optimize the variable associated with the count of a single operator, the objective function that they minimize is the total cost of the plan. The adaptation of the linear program to the case of unsolvability detection was carried out by the Fast Downward-based unsolvability planner Aidos (Seipp et al., 2016). It consists of checking the existence of a solution, in the same way as for Linear Program 2. However, Aidos uses this component in a state space search, in order to detect dead ends.

More generally, be it in unsolvable or in solvable planning tasks, the early detection of states that cannot lead to a goal can help prune out whole branches of the search space. In the case of dead-end detection (Cserna et al., 2018), various works have focused on the elaboration of formulas that can be efficiently evaluated, and whose only models are states that cannot lead to a goal state. The notion of dead-end formula has been generalized with the notion of traps (Lipovetzky et al., 2016): a formula $\varphi$ such that, once it is verified in a state $s$ , all states reachable from $s$ will satisfy it too. A formula $\varphi$ that is inconsistent with the goal then shows that the current branch is not worth exploring.

In the case where our algorithm does not manage to find that the task is unsolvable, it still manages to remove unnecessary elements from the planning model, to make the task easier for the next algorithm. Various other methods prune the model in a preprocessing step: in Alcázar and Torralba (2015), the authors show that invariants in the form of mutexes can be leveraged to remove operators that will never be part of a plan. In Fišer et al. (2019), it is shown how to combine symmetries of the planning task and operator mutexes to find operators that are redundant, in the sense that removing them preserves at least one solution plan.

Our algorithm also learns information that is not explicitly expressible in a STRIPS planning instance. In Steinmetz and Hoffmann (2017b), the authors draw inspiration from a well-known technique in SAT solving, to learn clauses that recognize dead ends, through a conflict-driven approach during search. They also show how to learn traps online Steinmetz and Hoffmann (2017a). Learning is ubiquitous in generalized planning, which is a domain concerned with the synthesis of generalized plans, which are procedures that solve multiple instances. For instance, previous work (Ståhlberg et al., 2021) proposed to learn heuristics in the form of logical formulas, out of a set of small examples instances, so as to recognize unsolvable planning instances.

In Christen et al. (2022), another polynomial criterion is proposed to immediately detect a class of unsolvable instances without resorting to search. The authors synthesize a function that separates the initial state from all goal states, through a linear combination of features valued in a finite field, or at least in a ring. Akin to our criterion, their technique is incomplete, but it is very efficient at detecting parity arguments. In practice, they define a system of linear equations that they solve through a Gaussian elimination process, since the variables have domain ${\mathbb{F}}_2=\{0,1\}$ . More generally, in the same paper, the authors formalize the theory of what they named separating functions, which encompasses both their criterion and the one found in Aidos Seipp et al. (2016). Their theory proposes linear programs that are very close, if not identical, to Linear Program 1. However, they require a planning instance in FDR and TNF, and their results do rely on these hypotheses. In this paper, we showed that, in the special case where variables range over ${\mathbb{R}}^{+}$ , and when the planning task is expressed in STRIPS, TNF is not a requirement for the criterion to hold.

7. Discussion

7.1. Additional Operations

We designed more operations than presented in this paper, but we only report those for which a nontrivial amount of tests answered positively. Operations that never succeeded include operator ordering tests: given $a_1$ , $a_2$ two operators, does $a_1$ always appear before $a_2$ in all solution plans? This is the case, for instance, if $a_1$ has some initial fluent $f$ in its precondition, $a_2$ destroys $f$ , and no other operator can establish $f$ . In order to use our framework to test that $a_1$ cannot occur after $a_2$ , one can check that the preconditions of $a_1$ cannot be reached once $a_2$ has been applied. But to do so, the instance has to be projected on the only fluent whose value is known after the application of $a_2$ . As a result, the linear program corresponding to the newly formed instance is loosely constrained, and our experiments did not allow us to conclude.

Other such tests include checking if some fluent $f$ can be added to the negative precondition of operator $a$ , when the STRIPS formalism used allows negative preconditions. This can be done by testing if $\mathsf{\text{pre}}(a)\cup \{f\}$ is reachable from $I$ . If not, then $\mathrm{\neg }f$ can be added to the preconditions of $a$ . Preliminary experiments showed that such tests sometimes succeed, but the proportion of tests that do is often negligible compared to the cost of testing each pair of $F\times O$ , hence of choice of STRIPS with positive preconditions only throughout this paper.

7.2. Perspectives

Section 5 showed that, when our criterion failed to show an instance unsolvable, it was still possible to extract additional information from the model by leveraging the criterion. Even more so, in some cases, otherwise undetected unsolvable instances could be identified as such by this means. Yet, there is still a lot of room for improvement: a more in-depth study of our operations, as well as their interactions, could help us fine-tune the algorithm, and tailor more effective sequences of operations. Indeed, not all sequences of tests are equal in all aspects, and finding a sequence that avoids unnecessary computations is a way to optimize our algorithm and boost its detection power.

In our tests, we choose to simply run predetermined sequences of operations and tests. This means that, regardless of how tests succeed or fail, the algorithm will linearly go through the same sequence of operations, except if it can show preemptively that an instance is unsolvable. However, the outcome of some tests may help in finding which step to take next. For instance, after finding that an operator is a landmark, it might be interesting to check right away if it can be removed. This can be done through a stack of operations, on which are added the operations that are made relevant by the result of another previous operation.

One of the main weaknesses of our iterative refinement algorithm is its computational cost. Even the most lightweight sequences, such as the OperatorPreImpossible sequence, take significant time to complete. Our program builds each linear program from scratch each time a test is performed. However, very few constraints differ from one linear program to the other; thus, one could modify only these constraints from one test to the next, in order to save significant time. In addition to that, the operations are mostly independent of one another: as a consequence, one could perform multiple operations in parallel with minimum loss.

Finally, as future work, we wish to find a method to reinvest the newly found information about the planning model directly into an off-the-shelf planner, in order to assist it during search. This could either be done by refining the planning model as a preprocessing phase, or by allowing the planner to use our procedure as an oracle during search, to ask very specific questions about some particular aspect of the problem at hand.

8. Conclusion

In this article, we showed that a simple criterion was sometimes enough to prove that a planning instance is unsolvable. Even though our program is nonoptimized, we have still managed to show that resorting to a search is not always necessary, as reasoning on the model directly can suffice. Even when our procedure fails, it still gathers valuable information about the instance, that provide insight on the planning instance itself.

Other operations and tests can be thought of and included in our framework. The most important point would be to ensure that the information that they bring is related to the other operations (e.g., checking if an operator $a$ ’s preconditions are removable, and checking if $n^{+}(a)\le 0$ ), or at least that the new information can be reinvested in the linear program.