Counting and Reasoning with Plans

TL;DR

The paper studies counting and reasoning on plan spaces in classical planning under polynomially bounded plan lengths. It encodes planning tasks into propositional formulas and compiles them into $d$-DNNF to enable efficient counting and reasoning, culminating in the Planalyst tool. The work provides a formal complexity taxonomy for qualitative and quantitative plan-space reasoning (e.g., $NP$-complete, $coNP$-complete, $C^P_{=}$-complete, and $D^P$-complete) and introduces facet reasoning to obtain practical, NP-complete queries without full counting. Empirically, Planalyst scales to very large plan spaces, enabling conditional probability queries, sampling, and explainable planning, and offering a practical alternative to enumeration-based planning in domains with trillions of plans.

Abstract

Classical planning asks for a sequence of operators reaching a given goal. While the most common case is to compute a plan, many scenarios require more than that. However, quantitative reasoning on the plan space remains mostly unexplored. A fundamental problem is to count plans, which relates to the conditional probability on the plan space. Indeed, qualitative and quantitative approaches are well-established in various other areas of automated reasoning. We present the first study to quantitative and qualitative reasoning on the plan space. In particular, we focus on polynomially bounded plans. On the theoretical side, we study its complexity, which gives rise to rich reasoning modes. Since counting is hard in general, we introduce the easier notion of facets, which enables understanding the significance of operators. On the practical side, we implement quantitative reasoning for planning. Thereby, we transform a planning task into a propositional formula and use knowledge compilation to count different plans. This framework scales well to large plan spaces, while enabling rich reasoning capabilities such as learning pruning functions and explainable planning.

Figures (2)

• Figure 1: State space of our running example task $\Pi_1$. The initial state is denoted by $s_0$; the goal state is denoted by $s_*$.
• Figure 2: Quantitative reasoning is a fine-grained reasoning mode between brave and cautious reasoning. It asks whether a literal matches $\geq p\cdot 100\%$ of the plans for planning task $\Pi$.

Theorems & Definitions (25)

• Example 1: Running Example
• Example 2
• Definition 3
• Remark 4
• Example 5
• Lemma 5: $\star$
• Definition 6: Probability Reasoning
• Example 7: Probability Reasoning
• Theorem 7: $\star$
• Theorem 7: $\star$