Olivier Gasquet
email: gasquet@irit.fr

Dominique Longin
email: longin@irit.fr

Frédéric Maris
email: maris@irit.fr

Pierre Régnier
email: regnier@irit.fr

Maël Valais
email: valais@irit.fr

Compact Tree Encodings for Planning as QBF

Keywords: Planning, Quantified Boolean Formula, Encodings

. In terms of execution time over benchmark problems, CTE-EFA and CTE-OPEN always performed better than CTE-NOOP.

Introduction

An algorithmic approach for plans synthesis is automated compilation (i.e., transformation) of planning problems. In the Satplan planner [START_REF] Kautz | Planning as satisfiability[END_REF], a planning problem is transformed into a propositional formula whose models, corresponding to solution plans, can be found using a SAT solver. The SAT approach searches for a solution-plan of fixed length k. In case of failure to find such a plan, this length is increased before restarting the search for a solution. In the classical framework, the complexity of finding a solution to any problem is PSPACE-hard, but the search for a fixed-size solution becomes NP-hard [START_REF] Bylander | The computational complexity of propositional STRIPS planning[END_REF]. This compilation approach directly benefits from improvements in SAT solvers1 . The most obvious example is the planner Blackbox [START_REF] Kautz | BLACKBOX: A new approach to the application of theorem proving to problem solving[END_REF][START_REF] Kautz | Unifying SAT-based and Graph-based planning[END_REF] (and its successors Satplan'04 [START_REF] Kautz | Satplan04: Planning as satisfiability[END_REF] and Satplan'06 [START_REF] Kautz | Satplan04: Planning as satisfiability[END_REF]). These planners won the optimal (in the number of plan steps) planning track of the International Planning Competitions2 IPC-2004 and IPC-2006. This was unexpected because these planners were essentially updates of Blackbox and did not include any real novelty: improved performance was mainly due to progresses in the underlying SAT solver.

Numerous improvements of this original approach have been proposed since then, in particular via the development of more compact and efficient encodings: [START_REF] Kautz | Pushing the envelope: Planning, propositional logic and stochastic search[END_REF][START_REF] Ernst | Automatic SAT-compilation of planning problems[END_REF][START_REF] Mali | Refinement-based planning as satisfiability[END_REF][START_REF] Mali | On the utility of plan-space (causal) encodings[END_REF][START_REF] Rintanen | Symmetry reduction for sat representations of transition systems[END_REF][START_REF] Rintanen | Parallel encodings of classical planning as satisfiability[END_REF][START_REF] Rintanen | Planning as satisfiability: parallel plans and algorithms for plan search[END_REF][START_REF]Proceedings of the Eighteenth International Conference on Automated Planning and Scheduling, ICAPS 2008[END_REF].

Following these works, numerous other similar techniques for encoding planning problems have been developed: Linear Programming (LP) [START_REF] Wolfman | The LPSAT engine & its application to resource planning[END_REF], Constraint Satisfaction Problems (CSP) [START_REF] Binh | Planning as constraint satisfaction: Solving the planning graph by compiling it into CSP[END_REF], SAT Modulo Theories (SMT) [START_REF] Shin | Processes and continuous change in a sat-based planner[END_REF][START_REF] Maris | TLP-GP: new results on temporally-expressive planning benchmarks[END_REF][START_REF] Rintanen | Discretization of temporal models with application to planning with SMT[END_REF]. More recently, a Quantified Boolean Formulas (QBF) approach had been proposed by [START_REF] Rintanen | Asymptotically optimal encodings of conformant planning in QBF[END_REF][START_REF] Cashmore | Planning as quantified boolean formula[END_REF]. Currently SAT solvers outperform QBF solvers and the SAT approach is the most effective because SAT solvers and encodings have been greatly improved since 1992. However, over the past decade, there has been a growing interest in the QBF approach. The competitive evaluation of QBF solvers QBFEVAL3 is now a joint event with the international SAT conference and QBF solvers improve regularly. QBFEVAL'16 had more participants than ever and QBFrelated papers represented 27% of all papers published at SAT'16. Some promising techniques have been adapted

X i bi=⊥ bi=⊤ right(i) X i-1 bi-1=⊤ X i-1 bi-1=⊥ X i-2 bi-2=⊥ b {i-2,...,1} =⊤ X i-2 b {i-2,...,1} =⊥ bi-2=⊤ X 0 left(i) C C X 0
Figure 1: Both possible transitions in a CTE following the branching structure of a QBF: X 0 → X i (from leaf to node on the left) and X i → X 0 (from node to leaf on the right). Note that i refers to any level (except for the leaf layer), not only the root.

to QBF solving such as counterexample guided abstraction refinement (CEGAR) [START_REF] Clarke | Counterexample-guided abstraction refinement for symbolic model checking[END_REF][START_REF] Janota | Solving QBF by clause selection[END_REF][START_REF] Janota | Solving QBF with counterexample guided refinement[END_REF][START_REF] Rabe | CAQE: A certifying QBF solver[END_REF]. For comparable SAT / QBF encodings, the QBF approach also have the advantage to generate more compact formulas [START_REF] Cashmore | Planning as quantified boolean formula[END_REF]. Even if the QBF approach is not as efficient as the SAT approach, it deserves the interest of the community.

Our paper shows that beyond the implementation of solvers, further work must be done to improve the encodings. In particular, we introduce two new QBF Compact Tree Encodings of STRIPS planning problems: CTE-EFA based on Explanatory frame axioms, and CTE-OPEN based on causal links. Then we compare both of them to [START_REF] Cashmore | Planning as quantified boolean formula[END_REF] where CTE-NOOP based on No-op Actions is proposed. In terms of execution time over benchmark problems, CTE-EFA and CTE-OPEN always performed better than CTE-NOOP.

Planning as QBF

In [START_REF] Cashmore | Planning as quantified boolean formula[END_REF], two different approaches of planning as QBF have been proposed: Flat Encoding, that was first introduced by [START_REF] Rintanen | Partial implicit unfolding in the davis-putnam procedure for quantified boolean formulae[END_REF] as an approach to general reachability, and Compact Tree Encoding (CTE). In [START_REF] Cashmore | Planning as quantified boolean formula[END_REF], authors showed that Compact Tree Encodings outperform Flat Encodings. Both these planning encodings make use of the branching structure of the QBF to reuse a single set of clauses that describes a single step in the plan. The two assignments inside each universal variable represent the first and second half of the plan split around that branch. The assignments to each existential set represent action choices within a single step.

Preliminary Definitions

Let F be a finite set of fluents (atomic propositions). A STRIPS planning problem is a tuple I, A, G where I ⊆ F is the set of initial fluents, G ⊆ F is the set of goal fluents and A is the set of actions. An action a ∈ A is a tuple Pre(a), Add(a), Del(a) where

• Pre(a) ⊆ F is the set of fluents required to be true in order to execute a,

• Add(a) ⊆ F and Del(a) ⊆ F are the sets of fluents respectively added and removed by the action a.

All QBF encodings studied in this paper use propositional variables for actions. The Compact Tree Encoding proposed in [START_REF] Cashmore | Planning as quantified boolean formula[END_REF] is based on the planning graph introduced in [START_REF] Blum | Fast planning through planning-graphs analysis[END_REF] and uses additional no-op actions as frame axioms. We denote it by CTE-NOOP. Considering every action as a propositional variable, we define a set of propositional variables X, given by

X = A ∪ {noop f | f ∈ F }.
In a CTE formula, we want to select two consecutive steps in order to define transitions (Figure 1). For each depth i of the tree, Xi denotes a copy of the set of variables X.

For CTE-NOOP, there exists a single variable ai ∈ Xi for each action and a single variable noop f,i ∈ Xi (no-op action) for each fluent used to determine a transition in the plan. At a same depth i, the value of these variables depends on the node (corresponding to a step in the plan) selected by the values of upper universal branching variables bi+1 . . . b depth . More details can be find in the slides 4 .

An upper bound on the plan length is 2 k+1 -1, where k is the number of alternations of quantifiers in the quantified boolean formula associated with the planning problem. In the case of CTE, k is also the compact tree depth. The number of possible states for a given planning problem is bounded by 2 |F | . Then, the existence of a plan can be determined using a linear QBF encoding with at most k =| F |.

In the sequel, we propose two new encodings of planning problems into QBF. The first, denoted by CTE-OPEN, is based on causal links (plan-space). It has been introduced by [START_REF] Mali | On the utility of plan-space (causal) encodings[END_REF] but needs to be adapted using additional variables for open conditions. The second, denoted by CTE-EFA, is based on explanatory frame axioms (state-space) first introduced by [START_REF] Kautz | Planning as satisfiability[END_REF] and uses variables for fluents as well as for actions.

Causal Link Encoding: CTE-OPEN

The plan-space encodings of [START_REF] Mali | On the utility of plan-space (causal) encodings[END_REF] cannot be directly adapted to the CTE. All these encodings refer to three indexed (not necessarily consecutive) steps of the plan. This is not possible in a CTE because each rule can refer to only one branch of the tree. To overcome this problem, it would be possible to duplicate the tree by adding, for each branching variable bi, two more branching variables b ′ i and b ′′ i , and for each node Xi, two node copies X ′ i and X ′′ i , and equivalence rules

x i ∈X i (xi ↔ x ′ i ) ∧ (xi ↔ x ′′ i ) .
Unfortunately, this would increase the branching factor unnecessarily. So, we propose a new plan-space encoding which allows us to only refer to consecutive steps in the plan.

For every fluent f ∈ F , we create a propositional variable open f to express that f holds in some previous step and must be protected at least until the current step. In Figure 2, the fluent f is an open condition in step Si, entailing that either f ∈ I or an action a ′ which adds f is executed in a previous step S i-k . Open conditions are propagated backwards until the initial state or some step in which they are added by an action. We define the set of "open" variables, denoted as ∆, as ∆ = {open f | f ∈ F }. Considering every action as a propositional variable, we define a set of propositional variables X, given by X = A ∪ ∆.

a f ∈ Pre(a) open f S i-1 S i propagate open f S i-k open f a ′ f ∈ Add(a ′ )
Quantifiers For each depth i of the tree, Xi denotes a copy of the set of variables X. It exists a single variable ai ∈ Xi for each action used to determine last transition in the plan and a single variable open f,i ∈ Xi for each fluent used to determine if f is an open condition. At a same depth i, the value of these variables depends on the node (corresponding to a step in the plan) selected by the values of upper universal branching variables bi+1 . . . b depth .

∃ a∈A a depth . ∃ f ∈F open f,depth . ∀ b depth . ∃ a∈A a depth-1 . ∃ f ∈F open f,depth-1 . ∀ b depth-1 . . . . ∃ a∈A a1. ∃ f ∈F open f,1 . ∀ b1. ∃ a∈A a0. ∃ f ∈F open f,0 .
In the following, a node now refers to a non-leaf node (i.e., an inner node) and depth is the depth of the tree. The predecessor of a node at level i is the rightmost leaf of the left subtree. The successor of a node at level i is the leftmost leaf of the right subtree. In order to select these transitions, we introduce the leaf-to-node operator left(i) defined as:

left(i) ≡ ¬bi ∧ i-1 j=1 bj.
Symmetrically, we introduce the node-to-leaf operator right(i) defined as:

right(i) ≡ bi ∧ i-1 j=1 ¬bj.
Open conditions If an action a is executed in a step of the plan, then each precondition of a must be an open condition at this step (i.e., a causal link is required for this precondition).

depth i=1 f ∈F     open f,i ∧ left(i) ⇒     open f,0 ∨ a∈A f ∈Add(a) a0         depth i=1 f ∈F     open f,0 ∧ right(i) ⇒     open f,i ∨ a∈A f ∈Add(a) ai        

Protect open conditions

An open condition in a given step cannot be removed in the previous step. This guarantees not to break any causal link in the plan.

depth i=1 f ∈F     open f,i ∧ left(i) ⇒ a∈A f ∈Del(a) ¬a0     depth i=1 f ∈F     open f,0 ∧ right(i) ⇒ a∈A f ∈Del(a) ¬ai    
Prevent negative interactions In a given step, if an action removes a fluent which is needed or added by another action, then these two actions cannot be both executed in this step.

depth i=0 a∈A f ∈(Add(a)∪Pre(a)) a ′ ∈A a =a ′ f ∈Del(a ′ ) ¬ai ∨ ¬a ′ i 2.

State-Space Encoding: CTE-EFA

In this encoding, we define the set of propositional variables as X = A ∪ F . Each step is now defined by a transition (as in CTE-OPEN) as well as the resulting state (valuation of the fluents in F ). The formula is an adaptation to the CTE of the well known state-space SAT encoding rules based on explanatory frame axioms of [START_REF] Kautz | Planning as satisfiability[END_REF].

Quantifiers At each depth i of the tree, it exists a single variable ai for each action used to determine last transition in the plan and a single variable fi for each fluent used to determine the state. At a same depth i , the values of these variables depend on the node (corresponding to a transition in the plan and the resulting state) selected by the values of upper universal branching variables bi+1 . . . b depth .

∃ a∈A a depth . ∃ f ∈F f depth . ∀ b depth . ∃ a∈A a depth-1 . ∃ f ∈F f depth-1 . ∀ b depth-1 . . . . ∃ a∈A a1. ∃ f ∈F f1. ∀ b1. ∃ a∈A a0. ∃ f ∈F f0.
Goal In the state after the last plan transition (i.e. the rightmost leaf of the tree), all goal fluents must be achieved.

depth i=1 bi ⇒ f ∈G f0
Conditions and effects of actions If an action a is executed in a transition of the plan, then each effect of a occurs in the resulting state and each condition of a is required in the previous state.

depth i=0 a∈A   ai ⇒   f ∈Add(a) fi   ∧   f ∈Del(a) ¬fi     depth i=1 a∈A   ai ∧ left(i) ⇒ f ∈Pre(A) f0   depth i=1 a∈A   a0 ∧ right(i) ⇒ f ∈Pre(A) fi  
Moreover, an action which do not have all conditions in initial state cannot be executed in the first plan transition (i.e. the leftmost leaf of the tree):

depth i=1 ¬bi ⇒ a∈A Pre(a) ⊂I ¬a0
Explanatory frame axioms If the value of a fluent changes between two consecutive states, then an action which produces this change is executed in the plan transition between these states.

depth i=1 f ∈F     (¬f0 ∧ fi ∧ left(i)) ⇒     a∈A f ∈Add(a) ai         depth i=1 f ∈F     (¬fi ∧ f0 ∧ right(i)) ⇒     a∈A f ∈Add(a) a0         depth i=1 f ∈F     (f0 ∧ ¬fi ∧ left(i)) ⇒     a∈A f ∈Del(a) ai         depth i=1 f ∈F     (fi ∧ ¬f0 ∧ right(i)) ⇒     a∈A f ∈Del(a) a0        
An extra rule is also required to describe explanatory frame axioms for the first plan transition from initial state (i.e. the leftmost leaf of the tree):

f ∈F \I       f0 ∧ depth i=1 ¬bi ⇒ a∈A f ∈Add(a) Pre(a)⊂I a0       f ∈I       ¬f0 ∧ depth i=1 ¬bi ⇒ a∈A f ∈Del(a) Pre(a)⊂I a0      
Prevent negative interactions Unlike in CTE-NOOP and CTE-OPEN, contradictory effects are already disallowed by previous rules (effects of actions). Then, this rule only need to prevent interactions between conditions and deletes of actions. If an action removes a fluent which is needed by another action, then these two actions cannot be both executed in a same plan transition.

depth i=0 a∈A f ∈Pre(a) a ′ ∈A a =a ′ f ∈Del(a ′ ) ¬ai ∨ ¬a ′ i 3

Experimental Trials

To compare these three encodings on a same basis we used our translator TouIST5 [START_REF] Comte | Twist your logic with touist[END_REF] that can use several QBF solvers. We ran all available STRIPS IPC benchmarks (1 through 8, except for the 7th which was not available and authors did not answer) on an Intel Xeon CPU E7-8890 v4 @ 2.20GHz, 512 GB of RAM. The domains tested include Gripper, Logistics, Mystery, Blocks, Elevator, Depots, DriverLog, ZenoTravel, FreeCell, Airport, Pipesworld-NoTankage, Pipesworld-Tankage, PSR, Satellite, OpenStacks, Pathways, Rovers, Storage, TPP, Trucks, ChildSnack, Hiking, VisitAll and the non-IPC Ferry.

We tried to consider as many QBF solvers as possible using the QBFEval 2017 as a reference. Qute (version of 2017-07-09, based on dependency learning QCDCL) and CaQE (version of 2017-07-08, based on CEGAR clausal abstraction) were not able to give a valuation for the outer existential quantifier. AIGSolve and Qell weren't available for download. GhostQ was skipped (but we should have included it). DepQBF (version 6.03 of 2017-08-02, based on "generalized Q-resolution", described in [START_REF] Lonsing | Depqbf 6.0: A search-based QBF solver beyond traditional QCDCL[END_REF]) and RAReQS (version 1.1 of 2013-05-07, based on a CEGAR approach, detailed in [START_REF] Janota | Solving QBF with counterexample guided refinement[END_REF]) were the only solvers left. RAReQS was consistently twice as fast as DepQBF, we thus dismissed DepQBF and only shown results for RAReQS. Finally, we did not apply any QBF preprocessor (e.g., Bloqqer). We ran these benchmarks using our new encodings CTE-EFA and CTE-OPEN as well as the state-of-the-art compact tree encoding (CTE-NOOP). We compared them two-by-two by considering the time needed to prove the existence of a plan (decision time, Figure 3) and the overall time required to obtain a plan (extraction time, Figure 5). The "decision" step consists of launching incrementally the QBF solver on a CTE of increasing depth until the solver returns true or reaches the upper bound (total number of fluents). The "extraction" step consists of one solver launch per node of the tree in order to retrieve the plan. Each experiment had a 60 minutes6 timeout for searching the plan and 60 minutes for extracting it. The benchmark results are available as an Excel file 7 .

The results show that our encodings CTE-EFA and CTE-OPEN are more efficient than CTE-NOOP both in plan existence as well as in plan extraction. CTE-EFA by a factor of 2.1 (1/0.4843) and CTE-OPEN by a factor of 1.7 (1/0.5953). Also, the comparison between CTE-EFA and CTE-OPEN (Figure 4, Figure 6) consistently shows that CTE-EFA outperforms CTE-OPEN by a factor of 1.4 (1/0.7266). Table 1 gives a summary of the benchmark results.

Contrary to what happens with flat encodings, the gain over CTE-NOOP cannot be explained by the difference in quantifier alternations as the depth is the same in the three encodings. However, the way actions are represented in these encodings may explain this difference.

Discussion

In order to identify the source of these improvements, we propose two hypothesis: clause has different contexts depending on the selected branch. The idea is that clauses based on different contexts slow the solver down. As displayed in Table 1, this hypothesis does not appear to be correct experimentally: although CTE-OPEN shows a lower transitions-to-nodes ration, it does not lead to the best performance gain. On the contrary, CTE-EFA has a poorer ratio, although being the most efficient compared to CTE-NOOP. We thus refute this hypothesis as we did not see any noticeable correlation supporting it, although we noticed a slight tendency where the decrease of time and of number of clauses were correlated.

Through these hypotheses, we tried to understand the causes of these enhancements. None of these hypothesis proved to be useful.

Conclusion

We have proposed two new QBF Compact Tree Encodings: CTE-OPEN based on causal links (plan-space) and CTE-EFA based on explanatory frame axioms (state-space). We compared these encodings with the state-ofthe-art QBF encoding CTE-NOOP. In average over all available STRIPS IPC benchmarks, CTE-EFA performed twice as fast as CTE-NOOP (respectively 1.7 times faster for CTE-OPEN).

Through experiments, we refuted the two hypotheses we had formulated in order to explain the causes of this enhancement: neither the difference in the number of literals and clauses nor the transitions-to-nodes ratio between the three encodings allow us to draw conclusions.

Although it is fair to say that the work we are presenting lacks explanations on the reasons for the gain in performance, we think that this paper aims at showing the interest of systematically studying the statistical properties of the various action representations in encodings in order to understand the ontological choices related to these action representations.

Furthermore, it is noticeable that the performance ranking of the various action representations of SAT encodings (e.g., No-op performs better than EFA) is different in QBF (as we showed, EFA performs better than No-op in the CTE encoding). It would be interesting to study more broadly the methods used in SAT for encoding actions and see how their QBF counterpart behave.

Figure 2 :

 2 Figure 2: Causal link: a ′ produces f for a.



  In the last plan step leading to the goal (i.e. the rightmost leaf of the tree), all the goal fluents must be either open conditions or added by actions executed in this step.Propagate and closeNo conditions should remain open in the first plan step (i.e. the leftmost leaf of the tree) if it is not provided in the initial state.depth i=1 ¬bi ⇒ f ∈F \I ¬open f,0Any open condition in a step must either remain open or be added (closed) by an action in the previous step.

  seconds (CTE-OPEN) Time in seconds (CTE-NOOP)

Figure 3 :

 3 Figure 3: Plan decision time (EFA/OPEN vs NOOP).

  seconds (CTE-EFA) Time in seconds (CTE-OPEN)

Figure 6 :

 6 Figure 6: Plan extraction time (EFA vs OPEN).

Table 1 :

 1 Comparison of the presented encodings across 65 STRIPS domains from IPC 1 through 8 (IPC 7 excepted) with a total of 2112 problems. Decision time, literals count, clauses count and the transitionsover-nodes ratio are averages. The transitions-over-nodes ratio measures the quantity (in average) of transition-based constraints over node-based constraints.

	Encoding	Solved problems	Decision Time Literals Clauses Transitions-over-nodes ratio
	CTE-NOOP 412 over 2112 (20%)	0%	0%	0%	30%
	CTE-EFA	463 over 2112 (22%)	-55%	-26%	+15%	47%
	CTE-OPEN 445 over 2112 (21%)	-41%	-2%	-28%	17%

http://www.satcompetition.org/

http://www.icaps-conference.org/index.php/Main/Competitions

http://www.qbflib.org/index_eval.php

https://www.irit.fr/ ~Frederic.Maris/documents/coplas2018/slides.pdf

https://www.irit.fr/touist

The grounding step (i.e., action instantiation) is not included in the elapsed time.

Context and expansion are defined in[START_REF] Cashmore | Planning as quantified boolean formula[END_REF]. Intuitively, the expansion is a tree representing the QBF and a context is a leaf in that tree.

Hypothesis 1 "The performance gain is correlated to a decrease in the number of clauses and/or literals across encodings". Although the size of the problem is known to be noticeably non-correlated with its hardness in SAT, we wondered if we could see the same non-correlation. As shown in Table 1, we do not observe any clear tendency: CTE-EFA tends to have a slightly higher number of clauses (+15%) than CTE-NOOP although having less variables (-26%). CTE-OPEN has the same number of literals and much less clauses than CTE-NOOP, but resulting in a lower performance gain (-41%) than CTE-EFA (-55%). This noncorrelation leads us to reject this hypothesis.

Hypothesis 2 "The performance gain is due to a difference in the number of transition-based constraints compared to the number of node-based constraints". Intuitively, one can think that a lower ratio of transitionbased constraints over node-based constraints would ease the solving process: in node-based constraints, a clause has the same context 8 across the whole QBF expansion. In branch constraints, the corresponding