Advancing Property Directed Reachability for Classical and Fully Observable Nondeterministic Planning

Abstract

Property Directed Reachability (PDR) is a powerful search paradigm that has been developed in the 21st century for model checking hardware and software systems, as well as for automated planning. To solve classical planning problems, PDR searches iteratively solve a series of small decision problems about whether a particular state can be progressed a single step toward the goal. Unlike earlier monolithic bounded model checking paradigms, which form the basis of many existing SAT-based planning tools, PDR does not unroll the system transition function over multiple steps, reasoning only about one step at a time. This approach results in a smaller memory footprint compared to monolithic bounded model checking. Additionally, PDR can detect when a problem has no solution without requiring a completeness threshold. However, by not reasoning about multi-step formulae, PDR misses out on the powerful multi-step propagation that underpins the strong performance of some SAT-based planning procedures. To address this, in our first contribution we develop two new PDR algorithms for classical planning that operate by solving small multi-step decision problems rather than single-step problems. Our results show that in certain domains a multi-step approach leads to more efficient search.

We then turn to parallel computing environments to further explore how to accelerate PDR. We introduce new parallel PDR algorithms for classical planning that significantly outperform serial procedures and existing parallel baselines from the model-checking literature. Our first algorithm, called Parallel State PDR (PSPDR), evaluates many decision problems in parallel using a pool of incremental SAT workers. PSPDR distinguishes itself from other distributed PDR algorithms by centrally maintaining a single queue of decision problems, enabling a more focused and efficient search compared to a PDR portfolio approach. Our second algorithm, Parallel Decomposition PDR (PDPDR), takes a compositional approach, decomposing the problem into subproblems and sequencing them according to the concrete problem structure. These subproblems are solved in parallel, and a concrete plan is constructed by combining the individual subproblem solutions. In problems with compositional structure, this can result in orders of magnitude speedup.

Finally, we extend PDR for the first time to tackle the Fully Observable Non-Deterministic (FOND) planning problem, which generalizes classical planning by allowing actions to have multiple possible outcomes chosen nondeterministically at execution. We evaluate our algorithm against leading FOND planners across a range of benchmarks, including cases where strong cyclic policies do and do not exist. Our results demonstrate the competitiveness of our approach, and the effectiveness of using PDR in planning under uncertainty. Show more