Improvements to the Generate-and-Complete Approach to Conformant Planning

1 Introduction

Conformant planning [Smith and Weld, 1998] aims to generate an action sequence that guarantees goal achievement under uncertainty in initial states and non-determinism of action effects. Conformant planning is computationally challenging, more precisely, EXPSPACE-complete [Haslum and Jonsson, 1999]. Numerous approaches have been developed to tackle the inherent complexity of conformant planning.

A series of competitive approaches are based on heuristic search over belief states. Forward search-based planners: GPT [Bonet and Geffner, 2000], CMBP [Cimatti and Roveri, 2000], KACMBP [Cimatti and Roveri, 2004], conformantFF [Hoffmann and Brafman, 2006], POND [Bryce et al., 2006], T1 [Albore et al., 2011], CPA(H) [Tran et al., 2013], DNF, CNF, PIP [To et al., 2015] start from the initial belief state and repeatedly performing executable actions to reach new belief states towards the goal condition. Backward search-based planners: CGP [Smith and Weld, 1998], YKA

∗Both are corresponding authors.

[Rintanen, 2002] and CAltAlt [Bryce et al., 2006] work as forward search-based ones but in an opposite direction from the goal condition to the initial belief state.

Another series of competitive approaches take advantage of classical planning. Palacios and Geffner [2009] proposed a sound translation from conformant planning problems to classical planning problems. The main idea is to extend each proposition p to propositions Kp/t and K¬p/t for a set T of tags where each tag t ∈ T is a set of unknown literals in the initial formula. Intuitively, Kp/t (resp. K¬p/t) means that p (resp. ¬p) holds in the initial state consistent with t. When T covers the initial formula, the translation becomes complete, but leads to an exponential blowup in the size of T to the width of the problem. T0 [Palacios and Geffner, 2009] firstly attempts to obtain a solution by using a sound and polynomial but incomplete translation and then generates a solution by using a complete translation when the attempt fails.

Grastien and Scala [2020] adopted the counterexampleguided framework, originally proposed in the field of computational learning theory [Angluin, 1987] and used in address the state explosion issue in model checking [Clarke et al., 2003], and developed a novel approach to conformant planning, namely CPCES. It maintains a subset S of initial sets, and computes a candidate solution α that works only for S not the whole set of initial sets. A conformant planning subproblem for S is translated to a classical planning problem via augmenting each proposition p to many copies ps for every state s ∈ S. Unlike the translation proposed by Palacios and Geffner [2009], this translation is complete but unsound. Since the subset S is often small, a conform plan α can be computed by a classical planner. If α is incorrect, then an initial state s, in which α does not hold, is added to S. A new candidate solution, which is guaranteed to be valid for the new set S, is generated. The procedure continues until either a correct plan is found or the problem is proved unsolvable.

Nguyen et al. [2012] designed a conformant planner following the generate-and-complete framework (in short, GC). It firstly finds a candidate plan α that works in an initial state s and then attempts to complete α to be hold in all initial states. If the completion procedure succeeds, it finds a conformant solution for all initial states; otherwise, it tries on another plan that works in s. Both generation and completion procedures are accomplished by a classical planner. Although GC exhibits its exceptional performance on conformant planning, it still has the following two drawbacks: (1) Several procedures of the GC approach explores all initial states. When the number of initial states is large, state exploration incurs a substantial computational overhead, making the problem difficult or even impossible to be solved within a reasonable time. (2) The completion procedure inserts many redundant actions into the solution, hence degrading the solution quality and the overall performance.

This paper is intended to overcome the above two drawbacks. The main contributions are the following. (1) We reduce the correct verification of the candidate solution to a SAT problem, which does not rely on state exploration. (2) We integrate the counterexample-guided framework into the completion procedure so as to avoid state exploration. Additionally, we devise a method to eliminate redundant segments of the candidate solution α by checking if the belief state remains unchanged after executing some segments of α. (3) We modify the main algorithm of the GC approach to accommodate the above two improvements. (4) We evaluate our improved GC approach on benchmarks that includes a total of 50 domains, with 1,179 instances from previous literature and the IPC competitions. The experimental results demonstrate that the improved GC planner outperforms the original one in two aspects: the number of solved instances and the length of solutions. Furthermore, the improved GC planner significantly improves upon every current state-ofthe-art planners, solving 989 instances in comparison to 784, which is the most solved by a state-of-the-art planner DNF.

2 Conformant Planning

Throughout this paper, we fix a set X of propositions. We use lower case letter (e.g., x, y, z) for propositions and upper case letters (e.g., Y, Z) for subsets of propositions. A literal l is a proposition p or it negation ¬p. A propositional formula ϕ is built from the set X of propositions, the connectives ¬, ∨, ∧, oneof and two Boolean constants ⊤ (truth) and ⊥ (falsity). The oneof connective is widely used in formulating conformant planning problems [To et al., 2015; Nguyen et al., 2011; Nguyen et al., 2012]. Intuitively, oneof(ϕ1, · · · , ϕn) means that there is an unique formula ϕi holds. A term is a conjunction of literals. For simplicity, we sometimes use a set {l1, · · · , ln} of literals to denote a term l1 ∧ · · · ∧ ln. A disjunctive normal form (in short, DNF) formula is of the form ψ1∨· · ·∨ψn and a oneof normal form (in short, ONF) formula is of the form oneof(ψ1, · · · , ψn) where each ψi is a term.

A state s is a subset of propositions. Given a state s and a formula ϕ, the notation s |= ϕ means that s satisfies ϕ, which is defined as usual. A model of ϕ is a state satisfying ϕ. We use �ϕ� for the set of models of ϕ. A belief state S is a set of states and can be represented as a propositional formula.

Definition 1. A deterministic conformant planning problem P is a tuple ⟨X , A, I, G⟩ where

• X: a finite set of propositions;
• A: a finite set of actions;
• I: a formula denoting the initial belief state;
• G: a formula denoting the goal condition.

We say a state s is an initial state, iff s ∈ �I�. We define P(s) = ⟨X,A, s, G⟩ as a subproblem of P where s ∈ �I�. Definition 1 allows the initial formula I and the goal formula G to be arbitrary propositional formulas. As in [To et al., 2015; Nguyen et al., 2011; Nguyen et al., 2012], we impose restrictions on I and G: (1) I is restricted to a conjunction of Il, Io and Id where Il is a set of literals, Io is a set of ONF-formulas and Id is a set of DNF-formulas, and (2) G is restricted to a conjunction of Gl and Gd where Gl is a set of literals and Gd is a set of DNF-formulas.

Each action a ∈ A is defined as a pair ⟨pre(a), eff(a)⟩ where pre(a) is a set of literals indicating the precondition and eff(a) is a non-empty set of conditional effects representing the effect. A conditional effect e is defined as a pair ⟨con(e), lit(e)⟩ where con(e) and lit(e) are sets of literals. Intuitively, if every literal of con(e) holds before the execution of e, then every literal of lit(e) holds after; otherwise, nothing is changed. A conditional effect e is applicable in s, iff s |= con(e). The positive condition con+(x, a) of an action a for a proposition x is defined as ∨e∈eff(a),x∈lit(e) con(e). Similarly, the negative condition con-(x, a) is ∨e∈eff(a),¬x∈lit(e) con(e). Intuitively, the positive (resp. negative) condition holds before performing a implies that x become true (resp. false) after. The positive effect eff+(s, a) of an action a in a state s is a set of propositions defined as {x | e ∈ eff(a), s |= con(e), x ∈ lit(e)}. Similarly, the negative effect eff-(s, a) is defined as {x | e ∈ eff(a), s |= con(e), ¬x ∈ lit(e)}. We require every action a to be self-contradictory, formally, eff+(s, a) ∩ eff-(s, a) = ∅ for every state s.

The resulting state τ(s, a) of executing an action a in a state s is s \ eff-(s, a) ∪ eff+(s, a). The resulting state Γ(s, [a1, · · · , an]) of executing an action sequence [a1, · · · , an] in a state s is recursively defined by Γ(s, [a1, · · · , an-1, an]) = τ(Γ(s, [a1, · · · , an-1]), an) and Γ(s, ε) = s where ε is an empty sequence. An action a is executable in a state s iff s |= pre(a). An action sequence [a1, · · · , an] is executable in a state s iff s |= pre(a1) and Γ(s, [a1, · · · , ai]) |= pre(ai+1) for i ≥ 1.

Given an action sequence α : [α1, · · · , αn], we use αi for the i-th action ai. An action sequence α is a solution to P, iff it is executable in every initial state and every resulting state by performing α from every initial state is a goal state.

We illustrate conformant planning with the robot navigation problem proposed in [Cimatti and Roveri, 2004].

Example 1. A robot can move in four directions in a 5 × 5 grid. Each cell (i, j) in the grid can be represented by two propositions xi and yj . For example, x1 ∧ y2 means that the robot is at cell (1, 2). The robot initially start at any position and its goal is to reach the center cell (3, 3).

• X = {xi | 1 ≤ i ≤ 5} ∪ {yj | 1 ≤ j ≤ 5};
• I = oneof(x1 , · · · , x5 ) ∧ oneof(y1 , · · · , y5 );
• G = x3 ∧ y3 ;
• A = {left, right, up, down};
• pre(left) = pre(right) = pre(up) = pre(down) = ∅;

Algorithm 1: GC(P)

Input: P = ⟨X , A, I, G⟩: a conformant planning problem Output: α: a solution to P 1 I ′ ← Combine(I) 2 s ←a state of �I ′ � 3 repeat 4 α← FindNextPlan(P(s)) 5 if α = ∅ then return ∅; 6 α← Complete(P, �I ′ �, α) 7 if Verify(P, α) ̸= ∅ then return α ; 8 until true;

Algorithm 2: Complete(P, S, α)

Input: P = ⟨X , A, I, G⟩: a conformant planning problem; S: a set of initial states; α: a plan to be completed. Output: α: a possible solution to P. 1 for i = 1 to k do 2 foreach s ∈ S do 3 if VerifyClassicPlan(P(s), α) = true then 4 s′ ← s 5 continue 6 α ← Extend(P, s, s′ , α) 7 if α = ∅ then return ∅ ; 8 return α

• eff(left) = {⟨{xi+1 }, {xi , ¬xi+1 }⟩ | 1 ≤ i ≤ 4}; · eff(right) = {⟨{xi }, {xi+1 , ¬xi }⟩ | 1 ≤ i ≤ 4}; · eff(up) = {⟨{yi+1 }, {yi , ¬yi+1 }⟩ | 1 ≤ i ≤ 4}; · eff(down) = {⟨{yi }, {yi+1 , ¬yi }⟩ | 1 ≤ i ≤ 4} .

One solution to this problem is [left×4, up×4, right× 2, down×2]. The plan α is always executable since all actions have valid precondition. She can move from any initial cell to the upper-left corner (x1 , y1 ) via performing four consecutive up actions followed by four consecutive left actions. She finally reaches the center cell (x3 , y3 ) by executing two consecutive right and two consecutive down actions.

3 The Generate-And-Complete Approach

In this section, we briefly introduce the generate-andcomplete approach to conformant planning, proposed by Nguyen et al. [2012].

The GC approach utilizes a classical planner Ω, which is required to not only generate one single solution for a classical planning problem but also enumerate many different solutions in an iterative manner. The procedure FindNextPlan aims to iteratively generate a new solution via utilizing a classical planner Ω and it returns ∅ when Ω cannot find any new solution. The basic idea behind the GC approach, illustrated in Algorithm 1 1 , is as follows. It first generates a solution α of the subproblem P(s) where s is an initial

1 The pseudocodes of Algorithms 1 and 2 are slightly different from that in [Nguyen et al., 2012] since the pseudocodes in our paper is based on the latest implementation of the GC[LAMA] planner.

Algorithm 3: Extend(P, s, s′ , α)

Input: P = ⟨X , A, I, G⟩: a conformant planning problem; s: the current state; s′ : the state where α is a solution to P(s′ ); α: a plan to be extended. Output: α: a solution to P(s). 1 s0 ← s 2 for j = 1 to |α| do 3 G′ ← GenerateGoal(αj, Γ(s′ , [α1, · · · , αj-1])) 4 βj ← FindNextPlan(⟨X,A, sj-1, G′ ⟩) 5 if βj = ∅ and sj-1 ̸|= pre(aj) then return ∅ ; 6 sj ← Γ(sj-1, βj ◦ αj) 7 βG ← FindNextPlan(P(s|α|)) 8 if βG = ∅ then return ∅ ; 9 α← β1 ◦ α1 ◦ · · · ◦ β|α| ◦ α|α| ◦ βG 10 return α

state if it exists (line 4). Since α may not be a solution of the original problem P, it then attempts to repair α to account for all of initial states (line 6). If the completion procedure fails to repair α, then it continues to find the next solution of P(s). The above steps repeat until no more solution of P(s) is found by Ω (line 5) or a solution of P is generated (line 7).

We say a conformant planner is sound iff it returns a plan α only if α is a solution to the conformant planning problem P; it is complete iff it returns ∅ only if P has no solution; and it is strongly complete for k iff it enumerates all solutions to P with length up to k, and returns ∅ when such all solutions exhaust. The above properties for classical planner can be similarly defined. Since the correctness of α is guaranteed in line 7, the GC approach is sound. Haslum and Jonsson [1999] proved that if a conformant planning problem has a solution, then it has a solution with length up to 22|X| where |X| is the number of propositions. In addition, every solution to P is also a solution to P(s). In summary, if the underlying classical planner Ω is strongly complete for 22|X| , then the GC approach is complete. The completeness of Ω cannot ensure the completeness of GC since Ω is not guaranteed to generate all solutions to P(s) with length up to 22|X| and the completion procedure is incomplete.

There are three remaining issues of Algorithm 1: (1) how to obtain an initial state s; (2) how to verify the correctness of a candidate plan α; and (3) how to repair a candidate plan α.

For the first issue, Algorithm 1 enumerates a collection �I� of initial states and choose one state from �I� as the initial state s (lines 1 - 2). In general, large-scale planning problems involves an enormous number of initial states. To reduce the number of initial states, Tran et al. [2013] proposed oneof-combination technique that generates a new initial formula I ′ by combining some ONF-formulas of the initial formula I into one. The formula I ′ has two characteristics: (1) I ′ entails I; and (2) every solution of the new conformant planning problem ⟨X,A, I ′ , G⟩ is also a solution of the original problem P and vice versa. For the details of oneofcombination technique, please refer to [Tran et al., 2013].

The verification procedure addresses the second issue. The GC approach reduces the problem of checking if α is a solution to every classical planning problem P(s) for every state s ∈ �I ′ �. The latter can be solved in the following. It applies the effects of actions α1, · · · , αi progressively to obtains each immediate state Γ(s, [α1, · · · , αi]) for 0 ≤ i ≤ |α|. The plan α is a solution to P(s) iff (1) α is executable in s; and (2) the final state Γ(s, α) satisfies the goal condition G.

The completion procedure, illustrated in Algorithm 2, aims to fix the third issue. It attempts to extend the solution α of the subproblem P(s) to a solution to P. For each initial state s ∈ S, the inner loop (lines 2 - 7) sequentially inserts a few actions into α. At each iteration, s′ is the last state where no action is needed to be inserted (line 4). Based on s′ and the current initial state s, actions are inserted into α to ensure that α becomes a solution for P(s) (line 6), if this is impossible, the algorithm terminates (line 7). The completed sequence α is not guaranteed to remain a solution to the subproblem for previously visited states. As a result, the inner loop will be invoked by k times where k = 3 in the implementation.

Algorithm 3 inserts some actions into the solution α to a subproblem P(s′ ) so that α becomes a solution to P(s). An action sequence βj is first generated by using the underlying classical planner and then is inserted between αj-1 and αj (line 4). To this end, an immediate goal G ′ is generated based on action αj and state s′j : Γ(s′ , [α1, · · · , αj-1]) (line 3). Three strategies for generating G ′ are proposed in [Nguyen et al., 2012]: Ignorant: pre(αj); Greedy: pre(αj) ∧ ∧e∈eff(αj),s′j |=con(e) con(e)); and Hybrid: pre(αj) ∧ ∧e∈eff(αj),s′j |=con(e),|con(e)|≤1 con(e). All strategies require αj to be executable. The greedy strategy ensures that the execution of αj preserves the execution of every applicable conditional effect of αj in s′j while the ignorant strategy does not. The hybrid strategy is a balance between them, which considers only applicable conditional effects whose condition is ⊤ or a single literal. The empirical results reported in [Nguyen et al., 2012] demonstrated that the hybrid strategy outperforms the other two. If the subproblem ⟨X,A, sj, G ′ ⟩ has no solution and αj is not executable in state sj, then repairing α to fit s is impossible and the algorithm terminates without a solution (line 5). Otherwise, we compute the resulting state sj+1 of executing the sequence βi ◦ αj in sj (line 6). To achieve the goal condition G, an additional action sequence βG is generated in a similar way to βj (lines 7 and 8). Finally, we insert each subsequence βj between αj-1 and αj and append βG to α (line 9).

4 Some Improvements to the GCApproach

In this section, we first analyze two drawbacks of the GC approach (Sec. 4.1). Then, we observe that the drawbacks lie in the two verification and completion procedures and hence propose SAT-based verification procedure (Sec. 4.2) and counterexample-guided completion procedure (Sec. 4.3). Finally, we integrate the two above improved procedures into the main GC algorithm (Sec. 4.4).

4.1 Two Drawbacks of the GCApproach

Although the GC approach is effective in conformant planning, it has the following two significant drawbacks. (1)

In some conformant planning problems, even using one-of combination technique, the number of initial states is still extremely large. For example, the or-dispose problem with 4 objects on 4 × 4 grids has 248 initial states. The overall efficiency of GC drops considerably since the three procedures: state enumeration, completion and verification traverses through all initial states. Even the state enumeration procedure sometimes runs timeout. (2) The complete procedure often introduces a substantial number of redundant actions. This results in an overly long solution, which negatively impacts the performance of verification procedure and the overall efficiency of the GC approach. For example, in the uts-l problem with 90 nodes, the GC approach generates a solution with length 4269, approximately 15 times longer than the shortest solution with only length 268.

4.2 SAT-Based Verification Procedure

We adopt a SAT-based verification procedure, proposed in [Hoffmann and Brafman, 2006; Grastien and Scala, 2020], which is a reduction from correctness verification of candidate solutions to a SAT problem. The major advantage of the SAT-based method over the verification in the original GC approach is that it does not exhaustively enumerates all initial states.

Suppose that P = ⟨X,A, I, G⟩ is a conformant planning problem and α is an action sequence. To distinguish the truth value of a proposition x on different time points during performing α, we use x0 to represent the value of x in the initial state, and xi to denote the value of x after executing the prefix [α1, · · · , αi] one by one. Given a formula ϕ and an index i, we use ϕi for the formula resulting from ϕ via replacing every occurrence of proposition x by the i-th time-stamped version xi.

The core of the SAT-based verification procedure is the successor state axiom ψi,x,a for proposition x and action a at time point i, which is defined as:

Intuitively, ψi,x,a means that at the time point i, x holds after executing a iff the positive condition of a for x holds before, or x holds before and the negative condition does not.

The trace axiom ϕP,α is defined as

Let ϕ be a formula over ⋃0≤i≤|α| Xi. We say a state s is the initial-projection of an assignment t of ϕ, if for every x ∈ X , we have x ∈ s iff x0 ∈ t.

The following theorem ensures that if the SAT-based verification procedure produces an initial state s, then α is not a solution to P(s).

Theorem 1 ([Grastien and Scala, 2020]). A state s is the initial-projection of an assignment of ϕP,α iff α is not a solution to P(s) and s ∈ �I�.

As a corollary, if the SAT-based verification procedure returns no assignment, then α is a solution to P, and vice versa.

Corollary 1 ([Grastien and Scala, 2020]). The action sequence α is a solution to P iff ϕP,α is unsatisfiable.

Algorithm 4: CG-Complete(P, s′ , α)

Input: P = ⟨X , A, I, G⟩: a conformant planning problem; s′ : a state; α: a plan to be completed. Output: α: a possible solution to P. 1 S ← {s′ } 2 repeat 3 s ← Verify(P, α) 4 if s = ∅ then return α ; 5 S ←S ∪ {s} 6 α← Extend(P, s, s′ , α) 7 s′ ← s 8 if α = ∅ then return α ; 9 α← EliminateRedundantAct(S, α) 10 until true; 11 return α

The trace axiom ϕP,α involves |X |×(|α|+1) propositions where |X| is the number of propositions and |α| is the length of α. The performance of SAT solvers is highly sensitive to the number of propositions and the length of the formula. To accelerate the verification phase, we will simplify the trace axiom via forgetting some redundant propositions. Due to space limit, we introduce the simplification of trace axioms in extended version.

Example 2. We continue the robot navigation problem illustrated in Example 1. Suppose that a plan α = [left, up]. We first construct the successor state axiom. Since left action contains only the conditional effect ⟨{x2 }, {x1 , ¬x2 }⟩ affecting x1 , the positive condition con+(x1 , left) of left for x1 is x2 and the negative condition con-(x1 , left) is ⊤. Hence, the successor state axiom ψ1,x1 ,left is x11 ↔ x20 ∨ (x10 ∧ ⊤). The other successor state axioms can be similarly constructed.

Finally, the trace axiom ϕP,α is the conjunction of the following formulas:

• oneof(x10 , · · · , x50 ) ∧ oneof(y1 0 , · · · , y5 0 );
• ∧5i=1 (ψ1,xi,left ∧ ψ1,yi,left ∧ ψ2,xi,up ∧ ψ2,yi,up );
• ¬(x32 ∧ y3 2 ).

It can be verified that ϕP,α is satisfiable and hence α is not a solution to P.

4.3 Counterexample-Guided Completion Procedure

We will introduce two improvements to the completion procedure, shown in Algorithm 4. The first improvement is to adopt the counterexample-guided (CG) framework to avoid explicit state explosion drawback. The CG completion procedure maintains a subset S of initial states that is used to eliminate redundant actions, which will be illustrated later. Initially, it contains only one state s′ (line 1). It firsts checks if α is a solution of P. If it fails the verification, it will generate an initial state s, which serves as a witness to the fact that α is not a solution to P and add s into S (lines 3 and 5). Unlike the original completion procedure, the improved one does not iterate over �I ′ � to extend the candidate plan

α. Instead, it extends α only for each newly generated initial state s (line 6). Afterward, s′ will be set to the witness s for the next iteration since α is extended to be a solution of P(s) (line 7). The above steps repeat until a solution to P is found (line 4) or α cannot be extend to a solution to P(s) (line 8).

During the extension process, several redundant actions may be introduced into the candidate plan α, which degrades both the quality of solutions and the efficiency of the verification procedure. To mitigate this drawback, we will remove redundant actions from α (line 9). We start from an initial belief state S0, and generate an evolving sequence of belief states [S0, · · · , Sn] by sequentially executing each action of α where S0 = S and Si = {Γ(s, [α1, · · · , αi]) | s ∈ S0} for 1 ≤ i ≤ |α|. If two belief states Si and Sj are identical, then the action subsequences [αi+1, · · · , αj] can be considered redundant. This is because, for each state s ∈ S, the original candidate plan α is a solution to P(s) iff the removed plan [α1, · · · , αi, αj+1, · · · , α|α|] is a solution to P(s). We repeatedly seek for two identical belief states Si and Sj and remove the segment [αi+1, · · · , αj] from α until all belief states are distinct. The experimental evaluation shows that each Si has at most 3789 states. Hence, each Si is explicitly represented as a set and this implementation of the elimination process is effective, which costs at most 200s.

Example 3. Table 1 shows the run of counterexample-guided completion procedure for the navigation robot problem. Algorithm 4 takes s′ = {x5 , y5 } and α = [left, up, left, up] as input. At the 1st iteration, the SAT-based verification procedure prove that α is not a solution to the navigation robot problem with an initial state {x4 , y4 }. Now, the belief state S contains two states {x4 , y4 } and {x5 , y5 }. An action sequence [left, right × 2, up, down × 2] will be inserted inbetween the first left action and the first up action of α so that α becomes a solution for the state {x4 , y4 }. Algorithm 4 discovers that S = {Γ(s, [left, right]) | s ∈ S} and that {Γ(s, [left, right × 2]) | s ∈ S} = {Γ(s, [left, right × 2, up, down]) | s ∈ S}. So the two segments [left, right] and [up, down] can be eliminated from α. We obtain a simplified candidate plan α : [right, down, left, up, left, up].

However, the above plan α is not the solution for every initial state. At the 2nd iteration, the verification procedure returns a witness {x1 , y1 } that is added into S. Then, α is extended to an plan [right × 3, down × 3, right, down, left, up, left, up]. None of actions in the above plan is redundant according to the three states: {x1 , y1 }, {x4 , y4 } and {x5 , y5 }. Finally, the new plan α is a solution to the navigation robot problem.

4.4 The ImprovedMain Algorithm

The last two subsections introduce improvements to the verification and completion procedures. We are ready to propose the modification to the main algorithm of the GC approach, illustrated in Algorithm 5. The improved GC approach works as the original GC approach except the following. (1) It generates a model of I ′ as the initial state s via utilizing the SAT solver rather than firstly enumerates all states of �I ′ � and then select one of �I ′ � as s (lines 1 and 2). (2) It uses SAT-based verification procedure and CG completion procedure instead the original two procedures. (3)

Algorithm 5: iGC(P)

Input: P = ⟨X , A, I, G⟩: a conformant planning problem Output: α: a solution to P 1 I ′ ← Combine(I) 2 s ←a state of �I ′ � 3 repeat 4 α← FindNextPlan(P(s)) 5 if α = ∅ then return ∅; 6 α← CG-Complete(P, s, α) 7 if α ̸= ∅ then return α ; 8 until true;

The verification procedure is invoked in the CG completion procedure rather than the main algorithm.

Similarly to the GC approach, we obtain the following two theorems regarding the soundness and completeness of the improved GC approach.

Theorem 2 (Soundness). If Algorithm iGC returns a plan α for P, then α is a solution to P.

Theorem 3 (Completeness). Let Ω be the underlying classical planner. If Ω is strongly complete for 22|X| where |X| is the number of propositions and P has a solution, then Algorithm iGC will terminate with a solution to P.

4.5 Comparisons to CPCES

We illustrate the main differences between CPCES and our approach in the following. (1) The main algorithm of our approach is still the generate-and-complete approach while CPCES is based on the counterexample-guided framework. We only integrate the CG framework into completion procedure. (2) When a candidate plan α is not a solution, CPCES completely discards α and computes a new solution. In contrast, we attempt to augment α to make it valid for all initial states.

5 Experimental Evaluation

5.1 Implementation and Experimental Setup

We implemented the improved GC approach, namely iGC, on top of the source code of the GC[LAMA] planner. Like GC[LAMA], we use LAMA [Richter and Westphal, 2010] as the underlying classical planner. Since the trace formula defined in Section 4.2 is arbitrary propositional formula, we employ Z3 [de Moura and Bjørner, 2008] as the underlying SAT solver of the verification procedure. For the generation of the immediate goal G′ (line 3 in Algorithm 3), we adopt the greedy strategy, which is able to solve domains like btc, grid-empty and grid-wall, which are solved by neither ignorant nor hybrid strategies.

We collect 50 domains with a total of 1179 instances, including 7 domains from IPC-5 [Bonet and Givan, 2006]:

adder-ipc5, coins, comm, uts-k, uts-l, uts-r, and sortnet; 6 domains from IPC-6 [Bryce and Buffet, 2008]: uts-cycle, raos-key, forest, dispose, adder-ipc6, and block; 7 domains from [Hoffmann and Brafman, 2006]: logistics, bomb, ring, grid, omlette, cleaner, and safe; 7 domains from [Palacios and Geffner, 2009]: cube-center, sqr-center, corners-sqr, cornerscube, look-and-grab, 1-dispose, and push-to; 10 domains from [To et al., 2015]: new-dispose, new-push, new-ring, new-uts-cycle, new-uts-k, or-1-dispose, or-coins, or-dispose, or-new-push, and or-push-to; 2 domains from [Grastien and Scala, 2020]: grid-empty and grid-wall; 5 domains from [Nguyen et al., 2012]: 1-dispose-disappear, hall-a, hall-r, marker-enc1, and look-and-grab-disappear; 2 domains from [Eiter et al., 2003]: bt and btc; 3 domains from others: retrieve, reward and to-trash; and 1 domain we propose: or1-dispose-disappear, a variant of or-1-dispose, which action pickup randomly drops the item at any location if it is held.

We compare our approach, namely iGC, with 8 state-ofthe-art planners: DNF, CNF, PIP, T1, CPA(H), gCPCES, iCPCES and GC[LAMA]. The experiments were run on Ubuntu 24.04, with an Intel 8086K 4.0 GHz CPU and 64GB RAM. The memory limit is 16GB, and the time limit is 3600s.

5.2 Comparative Analysis

We first make comparisons among 8 planners together with the iGC in terms of coverage of solved instance. Then, we compare the iGC with three most closely solvers GC[LAMA], gCPCES and iCPCES in detail.

Table 2 summarizes the total number of instances solved by each planner in each domain. We can make several observation from Table 2. (1) iGC solves the highest number of instances (989), followed by DNF, which ranks second with 784 instances. Moreover, iGC solves the most instances in 29 domains and ranks second in 8 domains. (2) It is worth noting that iGC is the only planner capable of solving 77 instances across 6 domains: 1-dis-dis, look-and-grab, new-dispose, or-1-dis-dis, ring, to-trash. (3) iGC is able to solve all instances in 24 domains, while GC and DNF handles all instances in 20 and 16 domains, respectively. (4) iGC has the same performance as gCPCES in the challenging domains grid-empty and grid-wall introduced in [Grastien and Scala, 2020]. Other planners except T1 are unable to solve any instance of the above two domains. (5) For 101 instances with high uncertainty in the initial state (including or-1-dis-dis, or-1-dis, or-coins, or-dispose, or-new-push, and or-push-to), iGC solves a total of 56 instances, which is just fewer than 84 instances solved by CNF and 78 instances solved by PIP. In particular, in the or-1-dis-dis domain, iGC outperforms CNF and PIP by solving 11 instances as opposed to 5 solved by CNF and PIP. (6) iGC fails to solve any instance on some domains. In domains: 1-dis, or-1-dis, omlette, marker-enc1 and new-uts-k, the underlying planner LAMA cannot enumerate every solution with length 22|X| for the classical planning problem P(s) since it lacks strong completeness. In addition, our completion procedure cannot extend any solution for P(s) supplied by LAMA to a correct solution for all initial states. The built-in PDDL file parser of GC used by iGC fails to interpret the PDDL file of the 3 domains adder-ipc5, adder-ipc6 and cleaner as presented in Table 5, and misinterprets some non-mutex propositions into a multi-valued proposition in domain new-uts-cycle.

iGC vs GC: It can be observed from Table 2, iGC successfully solves some instances of the 8 domains: btc, grid-empty and grid-wall, or-1-dis-dis, or-coins, or-dispose, or-new-push and or-push-to of which no instance can be solved by GC. Table 3 highlights some instances with an extremely large number of initial states (at least 65.5K), where GC is unable to find solutions. This is because the initial formula contains no oneof formulas and oneof-combination technique is invalid in these instances. In contrast, iGC excels in these instances incredibly quickly since it only deals with a minuscule subset of initial states to derive a solution. For example, in the instance coins-21 with 1016 initial states, iGC requires only 84 initial states to construct a correct solution within 24s. As illustrated in Table 4, iGC produces a solution with average length shorter compared to GC in 21 domains thanks to the elimination of redundant segments in solutions. In particular, for domains 1-dis-dis, forest, look-and-grab-dis, look-and-grab, new-ring, raos-key, to-trash and uts-l, iGC compute the solutions with length only half of those generated by GC. iGC generates solutions that are at least 60% longer than those of GC in the 4 domains: coins, retrieve, reward and uts-cycle. This is because the completion procedure in the original GC generates more succinct solutions than the improved planner. In summary, iGC demonstrates clear advantages over GC in both the number of solved instances and the quality of solutions across most domains.

iGC vs CPCES: As shown in Table 6, with the exception of grid-wall, new-push, new-ring, and safe, iGC takes less time on average for verification than iCPCES and gCPCES. For example, in cube-center, iGC and iCPCES solve problems with comparable average iterations and solution lengths. However, iGC completes verification in only 0.31s while iCPCES takes 3.99s. In or-dispose, although iGC uses 118.5 iterations on average, while iCPCES has 41.69 iterations, but the verification time of the former is significantly faster than that of the latter (1.62s versus 41.29s). This is due to our simplification strategy on the trace axioms and elimination strategy on solutions in iGC which effectively reduces the number of propositions and the length of the trace axiom, thereby accelerating the SAT-based verification procedure. However, iGC performs worse than CPCES in the four domains: cleaner, new-push, new-ring and safe. In cleaner and newring, iGC takes a majority of time in parsing PDDL file. For example, the cleaner-5-5 instance takes 98.03s to parse but only 0.01s to solve, while new-ring-10 requires 109.99s for parsing and just 9.90s for solving. In addition, some instances requiring excessive time for parsing PDDL in iGC are shown in Table 5. In the two domains: new-push and new-ring, iGC requires much more iterations than iCPCES to construct the solution. For example, in new-push-4-4 and new-ring-7, iGC requires 2871 and 1066 iterations while gCPCES needs only 13 and 2 iterations, respectively. In the safe domain, the number of propositions in the trace axiom generated by CPCES is only half of that in iGC due to different PDDL file parsers used by iGC, iCPCES and gCPCES. Overall, iGC is faster than both iCPCES and gCPCES in the majority of domains.

5.3 Ablation Study

Table 7 shows the results about the 42 domains solvable by iGC with and without optimizations. We use iGC for the iGC approach without simplification on trace axioms and elimination of redundant fragements, iGC+S for iGC with only simplification, iGC+E for iGC with only elimination and iGC+SE for iGC with both optimizations. For iGC+S, 14 domains have an increase of 50 solved instances relative to iGC. However, 7 domains experience a reduction of 31 solved instances, with notable decreases observed in the 1-dis-dis and new-push domains, where the number of solved instances drops by 18 and 6, respectively. Totally, iGC+S increases the total number of solved instances by 19. In comparison, iGC+E improves performance in 13 domains, yielding an additional 64 solved instances, while three domains show a reduction of 13 solved instances. In summary, iGC+E solves 51 more instances than iGC without optimizations. When both optimizations are applied together, 14 domains collectively achieve an increase of 73 solved instances, whereas three domains demonstrate a reduction of 10 instances. The total number of solved instances rises by 62, showing the complementary nature of these two optimizations.

Regarding solving time, iGC+S exhibits superior performance across 28 domains by simplifying trace axioms, which significantly reduce verification time. Similarly, iGC+E is faster than iGC in 27 domains. When both optimizations are employed, the approach iGC+SE is faster in 33 domains compared to iGC. However, performance degradation is observed in certain domains, primarily due to the counterexamples returned by the SAT solver. Different trace axioms generates different initial states, and hence affects the overall performance of iGC planner. For instance, in the 1-dis-dis domain, instances solvable by iGC fail with iGC+S due to memory overflow during the subproblem completion process.

In terms of solution length, iGC+E effectively eliminates redundant actions in 34 domains. Notably, 76.5% of the domains achieve length reductions exceeding 20%. The new-push domain demonstrates the most substantial improvement, with a 91.4% reduction in solution length. These results undercover significant enhancements in solution quality. Although simplifying optimization sometimes increases solution lengths, the combination with elimination optimization mitigates this issue.

6 Conclusions

In this paper, we have observed two major drawbacks of the GC approach: the computational overhead due to state exploration and the insertion of many redundant actions. To solve these two drawbacks, we have proposed SAT-based verification procedure and counterexample-guided completion procedure, and have integrated them into the GC approach, resulting in an improved GC planner, namely iGC. We have demonstrated the superior performance and scalability of iGC by evaluating it on standard benchmarks for conformant planning. In particular, iGC is the top planner in terms of coverage, solving 989 out of 1179 instances. Compared with the original GC planner, iGC exhibit the quality advantage of solutions and the ability to solve instances with a huge number of initial states.

Acknowledgements

We are grateful to Mingwei Zhang for his constructive comments on the paper. We sincerely thank Zexin Cai, Yuchun Zhong and Sijie Yin for their contributions to collecting and modifying PDDL files of each instance used in the experiments. This paper was supported by National Natural Science Foundation of China (Nos. 62206110, 62276114 and 62377028), Guangdong Basic and Applied Basic Research Foundation (Nos. 2023B1515120064 and 2024A1515011762), Guangzhou Science and Technology Planning Project (Nos. 202206030007, 2025A03J3565, Nansha District: 2023ZD001 and Development District: 2023GH01) and Major Key Project of PCL (Nos. PCL2024A04 and PCL2024AS204).