Plan-Space Explanation via Plan-Property Dependencies: Faster Algorithms & More Powerful Properties

Eifler, Rebecca; Steinmetz, Marcel; Torralba, Álvaro; Hoffmann, Jörg

doi:10.24963/ijcai.2020/566

Plan-Space Explanation via Plan-Property Dependencies: Faster Algorithms & More Powerful Properties

Rebecca Eifler, Marcel Steinmetz, Álvaro Torralba, Jörg Hoffmann

Video Download BibTeX Cite

Proceedings of the Twenty-Ninth International Joint Conference on Artificial Intelligence. Main track. Pages 4091-4097.

https://doi.org/10.24963/ijcai.2020/566

Keywords

Planning and Scheduling: Planning Algorithms
Planning and Scheduling: Search in Planning and Scheduling

Abstract

Justifying a plan to a user requires answering questions about the space of possible plans. Recent work introduced a framework for doing so via plan-property dependencies, where plan properties p are Boolean functions on plans, and p entails q if all plans that satisfy p also satisfy q. We extend this work in two ways. First, we introduce new algorithms for computing plan-property dependencies, leveraging symbolic search and devising pruning methods for this purpose. Second, while the properties p were previously limited to goal facts and so-called action-set (AS) properties, here we extend them to LTL. Our new algorithms vastly outperform the previous ones, and our methods for LTL cause little overhead on AS properties.

[Baier and McIlraith, 2006] Jorge A. Baier and Sheila A. McIlraith. Planning with first-order temporally extended goals using heuris- tic search. In Proc. AAAI, pages 788-795, 2006.
[Baier et al., 2009] Jorge A. Baier, Fahiem Bacchus, and Sheila A. McIlraith. A heuristic search approach to planning with tempo- rally extended preferences. AI, 173(5-6):593-618, 2009.
[Cashmore et al., 2019] Michael Cashmore, Anna Collins, Ben- jamin Krarup, Senka Krivic, Daniele Magazzeni, and David Smith. Towards explainable AI planning as a service. In ICAPS XAIP, 2019.
[Chinneck, 2007] John W. Chinneck. Feasibility and Infeasibil- ity in Optimization: Algorithms and Computational Methods. Springer-Verlag, 2007.
[De Giacomo et al., 2014] Giuseppe De Giacomo, Riccardo De Masellis, and Marco Montali. Reasoning on LTL on finite traces: Insensitivity to infiniteness. In AAAI, pages 1027-1033, 2014.
[Domshlak and Mirkis, 2015] Carmel Domshlak and Vitaly Mirkis. Deterministic oversubscription planning as heuristic search: Ab- stractions and reformulations. JAIR, 52:97-169, 2015.
[Edelkamp and Kissmann, 2009] Stefan Edelkamp and Peter Kiss- mann. Optimal symbolic planning with action costs and prefer- ences. In Proc. IJCAI, pages 1690-1695, 2009. IJCAI
[Edelkamp, 2006] Stefan Edelkamp. On the compilation of plan constraints and preferences. In ICAPS, pages 374-377, 2006.
[Eifler et al., 2020] Rebecca Eifler, Michael Cashmore, Jörg Hoff- mann, Daniele Magazzeni, and Marcel Steinmetz. A new ap- proach to plan-space explanation: Analyzing plan-property de- pendencies in oversubscription planning. In AAAI, 2020.
[Fox and Long, 1998] Maria Fox and Derek Long. The automatic inference of state invariants in TIM. JAIR, 9:367-421, 1998.
[Fox et al., 2017] Maria Fox, Derek Long, and Daniele Magazzeni. Explainable planning. In ICAI XAI, 2017.
[Gerevini et al., 2009] Alfonso Gerevini, Patrik Haslum, Derek Long, Alessandro Saetti, and Yannis Dimopoulos. Deterministic planning in the fifth international planning competition: PDDL3 and experimental evaluation of the planners. AI, 173(5-6):619- 668, 2009.
[Göbelbecker et al., 2010] Moritz Göbelbecker, Thomas Keller, Patrick Eyerich, Michael Brenner, and Bernhard Nebel. Coming up with good excuses: What to do when no plan can be found. In Proc. ICAPS, pages 81-88, 2010.
[Grastien et al., 2011] Alban Grastien, Patrik Haslum, and Sylvie Thiébaux. Exhaustive diagnosis of discrete event systems through exploration of the hypothesis space. In DX, 2011.
[Grastien et al., 2012] Alban Grastien, Patrik Haslum, and Sylvie Thiébaux. Conflict-based diagnosis of discrete event systems: Theory and practice. In Proc. KR, pages 489-499, 2012.
[Haslum and Geffner, 2000] Patrik Haslum and Hector Geffner. Admissible heuristics for optimal planning. In Proc. AIPS, pages 140-149, 2000.
[Haslum, 2012] Patrik Haslum. Incremental lower bounds for addi- tive cost planning problems. In Proc. ICAPS, pages 74-82, 2012.
[Helmert, 2006] Malte Helmert. The Fast Downward planning sys- tem. JAIR, 26:191-246, 2006.
[Helmert, 2009] Malte Helmert. Concise finite-domain representa- tions for PDDL planning tasks. AI, 173:503-535, 2009.
[Katz et al., 2019] Michael Katz, Emil Keyder, Dominik Winterer, and Florian Pommerening. Oversubscription planning as classi- cal planning with multiple cost functions. In ICAPS, pages 237- 245, 2019.
[Krarup et al., 2019] Benjamin Krarup, Michael Cashmore, Daniele Magazzeni, and Tim Miller. Towards model-based contrastive explanations for explainable planning. In ICAPS XAIP, 2019.
[Laborie and Ghallab, 1995] Philippe Laborie and Malik Ghallab. Planning with sharable resource constraints. In IJCAI, pages 1643-1651, 1995. IJCAI
[Laborie, 2014] Philippe Laborie. An optimal iterative algorithm for extracting MUCs in a black-box constraint network. In Proc. ECAI, pages 1051-1052, 2014.
[McMillan, 1993] Kenneth L. McMillan. Symbolic Model Check- ing. Kluwer Academic Publishers, 1993.
[Miller, 2019] Tim Miller. Explanation in artificial intelligence: In- sights from the social sciences. AI, 267:1-38, 2019.
[Nakhost et al., 2012] Hootan Nakhost, Jörg Hoffmann, and Martin Müller. Resource-constrained planning: A Monte Carlo random walk approach. In Proc. ICAPS, pages 181-189, 2012.
[Reiter, 1987] Raymond Reiter. A theory of diagnosis from first principles. AI, 32(1):57-95, 1987.
[Rintanen, 2000] Jussi Rintanen. An iterative algorithm for synthe- sizing invariants. In Proc. AAAI, pages 806-811, 2000.
[Smith, 2004] David E. Smith. Choosing objectives in over- subscription planning. In ICAPS, pages 393-401, 2004.
[Smith, 2012] David Smith. Planning as an iterative process. In AAAI, pages 2180-2185, 2012.
[Sreedharan et al., 2019] Sarath Sreedharan, Siddharth Srivastava, David Smith, and Subbarao Kambhampati. Why can't you do that HAL? explaining unsolvability of planning tasks. In IJCAI, pages 1422-1430, 2019. IJCAI
[Steinmetz and Hoffmann, 2017a] Marcel Steinmetz and Jörg Hoffmann. Search and learn: On dead-end detectors, the traps they set, and trap learning. In IJCAI, pages 4398-4404, 2017. IJCAI
[Steinmetz and Hoffmann, 2017b] Marcel Steinmetz and Jörg Hoffmann. State space search nogood learning: On- line refinement of critical-path dead-end detectors in planning. AI, 245:1-37, 2017.
[Torralba et al., 2014] Álvaro Torralba, Vidal Alcázar, Daniel Bor- rajo, Peter Kissmann, and Stefan Edelkamp. SymBA*: A sym- bolic bidirectional A* planner. In IPC 2014 abstracts, 2014.
[Torralba et al., 2017] Álvaro Torralba, Vidal Alcázar, Peter Kiss- mann, and Stefan Edelkamp. Efficient symbolic search for cost- optimal planning. AI, 242:52-79, 2017.
[Torres and Baier, 2015] Jorge Torres and Jorge A Baier. Polynomial-time reformulations of LTL temporally extended goals into final-state goals. In IJCAI, pages 1696-1703, 2015. IJCAI
[Vaquero et al., 2013] Tiago Stegun Vaquero, José Reinaldo Silva, Flavio Tonidandel, and J. Christopher Beck. itSIMPLE: To- wards an integrated design system for real planning applications. Knowledge Engineering Review, 28(2):215-230, 2013.
[Yu et al., 2017] Peng Yu, Brian Charles Williams, Cheng Fang, Jing Cui, and Patrik Haslum. Resolving over-constrained tem- poral problems with uncertainty through conflict-directed relax- ation. JAIR, 60:425-490, 2017.

References were extracted automatically from the PDF and may contain errors.

Full text extracted automatically from the PDF; figures, tables and equations may differ. The PDF is the version of record.

1 Introduction

As has been pointed out by Smith [2012] for space applications, the goal preferences for a planning task may be difficult to elicitate, calling for planning as an iterative process that suggests plan candidates for human inspection. Arguably this applies, for example, also to variants of production planning (Industry 4.0) and robot-aided disaster recovery. A key step in such a process is a variant of plan explanation answering user questions of the form "Why does the plan π you suggest not satisfy my preference p?". Eifler et al. [2020] recently introduced a framework addressing this explanation problem via plan-property entailments.

A plan property p is a Boolean function on plans, and p entails q if all plans that satisfy p also satisfy q. The answer to the above question could then be "Because achieving p would necessitate to either forego p′ or use > 100 energy units". This is a form of contrastive explanation [Miller, 2019]. Some previous works [Smith, 2012; Fox et al., 2017; Cashmore et al., 2019; Krarup et al., 2019] suggested to answer the question by comparing π to an alternative plan π′ that satisfies p. In Eifler et al.'s framework, the answer consists instead of the properties shared by all possible such π′ .

Eifler et al. [2020] (henceforth: "Eif20") assume a given set P of plan properties, and address oversubscription planning (OSP) [Smith, 2004; Domshlak and Mirkis, 2015] where not all of P can be satisfied. They identify all exclusion dependencies of the form ∧p∈X p ⇒ ¬ ∧p∈Y p where X, Y ⊆ P . Such dependencies are naturally suited to the desired Q/A pattern: "Why does the plan not satisfy the properties in X?" "Because then we would have to forego a property in Y ".

∗Contact Author

Eif20 compile each plan property into a goal fact g. As ∧g∈X g entails ¬ ∧g∈Y g iff ∧g∈X∪Y g is unsolvable, and as smaller property sets are stronger on each side of the entailment, the algorithmic problem thus boils down to computing all minimal unsolvable goal subsets (MUGS).

Eif20 compute MUGS through a meta-search over goal subsets G, where each search node invokes a planner to decide solvability of G. They devise information flow across nodes through nogood transfer. Performance is reasonable in international planning competition (IPC) benchmarks constraining plan cost as in OSP [Katz et al., 2019].

Our first contribution are two new algorithms for MUGS computation, as follows. (1) Run a symbolic search once to obtain a BDD representing the reachable state space, serving to implement the solvability tests efficiently. (2) Run a single explicit state-space search maintaining the set Gcurr of solvable goal subsets found so far, adapting previous pruning and nogood learning techniques [Steinmetz and Hoffmann, 2017b] to detect states fromwhich Gcurr cannot be improved. Both (1) and (2) vastly outperform Eif20's methods.

Interestingly, we also obtain highly competitive results in a basic form of OSP, namely finding a largest solvable goal subset, which is solved as a side effect of finding all MUGS. Both (1) and (2) significantly outperform the most recent OSP solver [Katz et al., 2019] on that problem.

Our second contribution consists in extending Eif20's framework to deal with more powerful plan properties. Eif20 consider goal facts as a simple canonical form of plan properties, and consider what they call action-set (AS) properties as a more complex form. AS properties pφ are defined by a propositional formula φ over atoms {A1, . . . ,An}, with Ai being true iff the plan uses at least one action a ∈ Ai. Eif20 devise a simple compilation of AS properties into goal facts.

Here, we tackle plan properties formulated in linear temporal logic, specifically LTLf interpreted over finite traces [Baier et al., 2009]. This strictly generalizes AS properties, and covers all but one of the preferences formulatable in PDDL3 [Gerevini et al., 2009]. To compile LTLf into Eif20 solve AllMUGS through a meta-search over softgoal subsets G, either starting with Gsoft and working downwards (systematic weakening, SysW), or starting with ∅ and working upwards (systematic strengthening, SysS). Each node in the meta-search invokes a planner to decide solvability. Towards efficiency, Eif20 employ recent nogood learning methods in the planner calls [Steinmetz and Hoffmann, 2017b; Steinmetz and Hoffmann, 2017a], and transfer the learned nogoods across nodes in the meta-search. This is always possible in SysS, and is possible in SysWwhenever the goals a nogood depends on are still present.

In our example, say we consider the plan properties 1 : use(T1,L0,L4), 2 : not use(T0,L0,L1), 3 : not use(T1,L1,L2), and 4 : same(P0, P1). Then the MUGS are {2, 3} and {1, 2, 4}. So, for example, the answer to the user question "Why does the plan not drive T1 from L0 to L4?" is "Because then either T0 has to drive from L0 to L1, or P0 and P1 cannot be transported with the same truck."

3 Solving AllMUGS with Symbolic Search

The planner calls in Eif20's SysW and SysS meta-searches all solve the same planning task, except for the changing goal subset. Eif20 leverage this connection for nogood transfer, thus avoiding some redundant work. However, as all the solvable goal subsets can be read off one and the same state space, the redundant work can be avoided altogether. We introduce two methods to this end, based on (1) computing a BDD that represents all reachable states (in the present section), respectively (2) a single explicit state-space search maintaining a list of solvable goal subsets (in the next section).

Symbolic search is a well-known paradigm that uses Binary Decision Diagrams (BDDs) to compactly represent sets of states, often using exponentially less memory than their explicit enumeration. Successor-state generation can be directly implemented on the BDD representation, via BDD operations whose runtime depends only on the BDD size, not on the number of states represented. Symbolic search has been shown to be a powerful tool for state space exhaustion in model-checking [McMillan, 1993] and planning [Edelkamp and Kissmann, 2009; Torralba et al., 2017].

Assembling this machinery for our purposes, the main difference to previous work is that we need to adhere to the cost bound. To this end, given an OSP task τ = (V, A, c, I, Ghard , Gsoft , b), we run a symbolic forward uniform-cost search. We terminate when we reach the cost-bound b, when we reach a state satifying Ghard ∪ Gsoft , or when all reachable states have been generated. The result is a BDD, that we denote βτ , which represents the set of states reachable in τ.

The BDD βτ can be used to test solvability of each goal G in SysS and SysW efficiently: 1. produce a BDD βG representing ∧g∈G g; 2. conjoin βτ and βG to obtain a BDD for βτ ∧ βG; and 3. test whether that latter BDD represents the empty set. Operation 1 takes time linear in |G|, operations 2 and 3 take time linear in the size of βτ times |G|. Given this fast test, using SysS vs. SysW hardly makes a performance difference anymore; in our experiments, we use SysS.

Note that, as a side effect, this algorithm solves cardinalityoptimal OSP. A largest solvable goal subset G can be identified by maintaining flags alongside SysW/SysS. Given such G, one can easily extract a cardinality-optimal plan from the BDDs βg produced by symbolic uniform-cost search for each g-cost value encountered. We implemented this technique as well, and will show that it yields interesting results.

4 AllMUGS Pruning and Nogood Learning

Our second new AllMUGS algorithm extracts all MUGS from a single explicit state-space search, exhausting all states reachable within the cost bound (or when a state is reached that satisfies Ghard ∪Gsoft ). During the exploration, we maintain reachability information for goal subsets, namely the set Gcurr of set-inclusion maximal goal subsets reached so far. When search terminates, Gcurr contains all maximal solvable goal subsets. The MUGS can be computed from this by first extending all G ∈ Gcurr with one more soft-goal fact in all possible ways, and then keeping the set-inclusion minimal sets from the outome. We denote the result by MUGS(Gcurr). Note that, through the computation of Gcurr, the algorithm also computes cardinality-optimal plans as a side effect.

Pruning To avoid exhausting the entire state space, one can prune states s from which it is not possible to achieve "something new", i. e., from which one cannot reach any Gnew ⊆ Gsoft with Gnew ̸⊆ Gold for any Gold ∈ Gcurr. Observe that this condition is satisfied iff s cannot reach any Gnew ∈ MUGS(Gcurr). The question now is how to adopt known reachability approximations for this purpose.

Assume any admissible classical planning heuristic h. One can prune a state s with remaining budget bs if (*) for all Gnew ∈ MUGS(Gcurr), h(s,Ghard ∪ Gnew) > bs. However, MUGS(Gcurr) may become large, and each call to h may incur a computational cost. So, with the pruning test conducted on every state during search, implemented na¨ıvely this approach is bound to cause substantial overhead. Here we show how to implement the approach more effectively for two particular heuristic functions, namely the critical-path heuristics hmax [Haslum and Geffner, 2000] and hC [Haslum, 2012]. Both allow to approximate (*) through a single computation of the heuristic, plus some additional processing:

In a nutshell, hmax approximates the cost-to-go by the cost of reaching each fact individually. This allows to extract, from a single hmax computation, the set P>bs of facts whose hmax estimate exceeds bs. Then (*) is entailed if Ghard ∩ P>bs ̸= ∅; or if there exists G ∈ Gcurr such that Gsoft \ P>bs ⊆ G.
The hC heuristic generalizes hmax by taking into account the cost to jointly achieve the fact sets (the conjunctions) contained in the parameter C. From a single hC computation, one can extract the set P C >bs of conjunctions whose hC estimate exceeds bs. Then (*) is entailed if P C >bs contains a subset of Ghard , i. e., ex. c ∈ P C >bs with c ⊆ Ghard ; or if, for every Gnew ∈ MUGS(Gcurr), P C >bs contains a subset of Ghard ∪ Gnew.

To make use of hC , we need to obtain the set C of conjunctions to consider. To this end, we extend Steinmetz and Hoffmann's [2017b] nogood learning approach to our context.

Rebecca Eifler, Marcel Steinmetz, Álvaro Torralba, and Jörg Hoffmann. 2020. Plan-Space Explanation via Plan-Property Dependencies: Faster Algorithms & More Powerful Properties. In Proceedings of the Twenty-Ninth International Joint Conference on Artificial Intelligence, IJCAI-20. IJCAI, 4091–4097. https://doi.org/10.24963/ijcai.2020/566

@inproceedings{ijcai2020p566,
  title     = {Plan-Space Explanation via Plan-Property Dependencies: Faster Algorithms & More Powerful Properties},
  author    = {Eifler, Rebecca and Steinmetz, Marcel and Torralba, Álvaro and Hoffmann, Jörg},
  booktitle = {Proceedings of the Twenty-Ninth International Joint Conference on
               Artificial Intelligence, {IJCAI-20}},
  publisher = {International Joint Conferences on Artificial Intelligence Organization},
  editor    = {Christian Bessiere},
  pages     = {4091--4097},
  year      = {2020},
  month     = {7},
  note      = {Main track},
  doi       = {10.24963/ijcai.2020/566},
  url       = {https://doi.org/10.24963/ijcai.2020/566},
}

TY  - CPAPER
TI  - Plan-Space Explanation via Plan-Property Dependencies: Faster Algorithms & More Powerful Properties
AU  - Eifler, Rebecca
AU  - Steinmetz, Marcel
AU  - Torralba, Álvaro
AU  - Hoffmann, Jörg
T2  - Proceedings of the Twenty-Ninth International Joint Conference on Artificial Intelligence, IJCAI-20
PB  - International Joint Conferences on Artificial Intelligence Organization
PY  - 2020
SP  - 4091
EP  - 4097
DO  - 10.24963/ijcai.2020/566
UR  - https://doi.org/10.24963/ijcai.2020/566
ER  -

[1] [Baier and McIlraith, 2006] Jorge A. Baier and Sheila A. McIlraith. Planning with first-order temporally extended goals using heuris- tic search. In Proc. AAAI, pages 788-795, 2006.

[2] [Baier et al., 2009] Jorge A. Baier, Fahiem Bacchus, and Sheila A. McIlraith. A heuristic search approach to planning with tempo- rally extended preferences. AI, 173(5-6):593-618, 2009.

[3] [Cashmore et al., 2019] Michael Cashmore, Anna Collins, Ben- jamin Krarup, Senka Krivic, Daniele Magazzeni, and David Smith. Towards explainable AI planning as a service. In ICAPS XAIP, 2019.

[4] [Chinneck, 2007] John W. Chinneck. Feasibility and Infeasibil- ity in Optimization: Algorithms and Computational Methods. Springer-Verlag, 2007.

[5] [De Giacomo et al., 2014] Giuseppe De Giacomo, Riccardo De Masellis, and Marco Montali. Reasoning on LTL on finite traces: Insensitivity to infiniteness. In AAAI, pages 1027-1033, 2014.

[6] [Domshlak and Mirkis, 2015] Carmel Domshlak and Vitaly Mirkis. Deterministic oversubscription planning as heuristic search: Ab- stractions and reformulations. JAIR, 52:97-169, 2015.

[7] [Edelkamp and Kissmann, 2009] Stefan Edelkamp and Peter Kiss- mann. Optimal symbolic planning with action costs and prefer- ences. In Proc. IJCAI, pages 1690-1695, 2009. IJCAI

[8] [Edelkamp, 2006] Stefan Edelkamp. On the compilation of plan constraints and preferences. In ICAPS, pages 374-377, 2006.

[9] [Eifler et al., 2020] Rebecca Eifler, Michael Cashmore, Jörg Hoff- mann, Daniele Magazzeni, and Marcel Steinmetz. A new ap- proach to plan-space explanation: Analyzing plan-property de- pendencies in oversubscription planning. In AAAI, 2020.

[10] [Fox and Long, 1998] Maria Fox and Derek Long. The automatic inference of state invariants in TIM. JAIR, 9:367-421, 1998.

[11] [Fox et al., 2017] Maria Fox, Derek Long, and Daniele Magazzeni. Explainable planning. In ICAI XAI, 2017.

[12] [Gerevini et al., 2009] Alfonso Gerevini, Patrik Haslum, Derek Long, Alessandro Saetti, and Yannis Dimopoulos. Deterministic planning in the fifth international planning competition: PDDL3 and experimental evaluation of the planners. AI, 173(5-6):619- 668, 2009.

[13] [Göbelbecker et al., 2010] Moritz Göbelbecker, Thomas Keller, Patrick Eyerich, Michael Brenner, and Bernhard Nebel. Coming up with good excuses: What to do when no plan can be found. In Proc. ICAPS, pages 81-88, 2010.

[14] [Grastien et al., 2011] Alban Grastien, Patrik Haslum, and Sylvie Thiébaux. Exhaustive diagnosis of discrete event systems through exploration of the hypothesis space. In DX, 2011.

[15] [Grastien et al., 2012] Alban Grastien, Patrik Haslum, and Sylvie Thiébaux. Conflict-based diagnosis of discrete event systems: Theory and practice. In Proc. KR, pages 489-499, 2012.

[16] [Haslum and Geffner, 2000] Patrik Haslum and Hector Geffner. Admissible heuristics for optimal planning. In Proc. AIPS, pages 140-149, 2000.

[17] [Haslum, 2012] Patrik Haslum. Incremental lower bounds for addi- tive cost planning problems. In Proc. ICAPS, pages 74-82, 2012.

[18] [Helmert, 2006] Malte Helmert. The Fast Downward planning sys- tem. JAIR, 26:191-246, 2006.

[19] [Helmert, 2009] Malte Helmert. Concise finite-domain representa- tions for PDDL planning tasks. AI, 173:503-535, 2009.

[20] [Katz et al., 2019] Michael Katz, Emil Keyder, Dominik Winterer, and Florian Pommerening. Oversubscription planning as classi- cal planning with multiple cost functions. In ICAPS, pages 237- 245, 2019.

[21] [Krarup et al., 2019] Benjamin Krarup, Michael Cashmore, Daniele Magazzeni, and Tim Miller. Towards model-based contrastive explanations for explainable planning. In ICAPS XAIP, 2019.

[22] [Laborie and Ghallab, 1995] Philippe Laborie and Malik Ghallab. Planning with sharable resource constraints. In IJCAI, pages 1643-1651, 1995. IJCAI

[23] [Laborie, 2014] Philippe Laborie. An optimal iterative algorithm for extracting MUCs in a black-box constraint network. In Proc. ECAI, pages 1051-1052, 2014.

[24] [McMillan, 1993] Kenneth L. McMillan. Symbolic Model Check- ing. Kluwer Academic Publishers, 1993.

[25] [Miller, 2019] Tim Miller. Explanation in artificial intelligence: In- sights from the social sciences. AI, 267:1-38, 2019.

[26] [Nakhost et al., 2012] Hootan Nakhost, Jörg Hoffmann, and Martin Müller. Resource-constrained planning: A Monte Carlo random walk approach. In Proc. ICAPS, pages 181-189, 2012.

[27] [Reiter, 1987] Raymond Reiter. A theory of diagnosis from first principles. AI, 32(1):57-95, 1987.

[28] [Rintanen, 2000] Jussi Rintanen. An iterative algorithm for synthe- sizing invariants. In Proc. AAAI, pages 806-811, 2000.

[29] [Smith, 2004] David E. Smith. Choosing objectives in over- subscription planning. In ICAPS, pages 393-401, 2004.

[30] [Smith, 2012] David Smith. Planning as an iterative process. In AAAI, pages 2180-2185, 2012.

[31] [Sreedharan et al., 2019] Sarath Sreedharan, Siddharth Srivastava, David Smith, and Subbarao Kambhampati. Why can't you do that HAL? explaining unsolvability of planning tasks. In IJCAI, pages 1422-1430, 2019. IJCAI

[32] [Steinmetz and Hoffmann, 2017a] Marcel Steinmetz and Jörg Hoffmann. Search and learn: On dead-end detectors, the traps they set, and trap learning. In IJCAI, pages 4398-4404, 2017. IJCAI

[33] [Steinmetz and Hoffmann, 2017b] Marcel Steinmetz and Jörg Hoffmann. State space search nogood learning: On- line refinement of critical-path dead-end detectors in planning. AI, 245:1-37, 2017.

[34] [Torralba et al., 2014] Álvaro Torralba, Vidal Alcázar, Daniel Bor- rajo, Peter Kissmann, and Stefan Edelkamp. SymBA*: A sym- bolic bidirectional A* planner. In IPC 2014 abstracts, 2014.

[35] [Torralba et al., 2017] Álvaro Torralba, Vidal Alcázar, Peter Kiss- mann, and Stefan Edelkamp. Efficient symbolic search for cost- optimal planning. AI, 242:52-79, 2017.

[36] [Torres and Baier, 2015] Jorge Torres and Jorge A Baier. Polynomial-time reformulations of LTL temporally extended goals into final-state goals. In IJCAI, pages 1696-1703, 2015. IJCAI

[37] [Vaquero et al., 2013] Tiago Stegun Vaquero, José Reinaldo Silva, Flavio Tonidandel, and J. Christopher Beck. itSIMPLE: To- wards an integrated design system for real planning applications. Knowledge Engineering Review, 28(2):215-230, 2013.

[38] [Yu et al., 2017] Peng Yu, Brian Charles Williams, Cheng Fang, Jing Cui, and Patrik Haslum. Resolving over-constrained tem- poral problems with uncertainty through conflict-directed relax- ation. JAIR, 60:425-490, 2017.