KR2023Proceedings of the 20th International Conference on Principles of Knowledge Representation and ReasoningProceedings of the 20th International Conference on Principles of Knowledge Representation and Reasoning

Rhodes, Greece. September 2-8, 2023.

Edited by

ISSN: 2334-1033
ISBN: 978-1-956792-02-7

Sponsored by
Published by

Copyright © 2023 International Joint Conferences on Artificial Intelligence Organization

Property Directed Reachability for Planning Revisited

  1. Ava Clifton(Australian National University)
  2. Charles Gretton(Australian National University)


  1. Belief revision and update, belief merging, information fusion
  2. Reasoning about actions and change, action languages
  3. Knowledge-driven decision making
  4. KR and autonomous agents and multi-agent systems


Property Directed Reachability (PDR) is a relatively new SAT-based search paradigm for classical AI planning. Compared to earlier SAT-based paradigms, PDR proceeds without unrolling the system transition function, and therefore without having the underlying procedure reason about potentially computationally expensive multi-step formulae. By maintaining a queue of obligations - i.e., a state at a timestep - and knowledge about what is possible at each planning step, PDR iteratively evaluates whether an obligation can be progressed by one step towards the goal. We develop and evaluate two new distributed PDR algorithms for planning, and additionally implement serial and portfolio PDR algorithms for planning. We are the first to consider distributed PDR for planning and the first to consider PDR based on incremental SAT solving in that setting. Our first new algorithm, PS-PDR, evaluates many obligations independently in parallel using a pool of incremental SAT workers. PS-PDR is unique amongst distributed PDR algorithms in centrally maintaining a single queue of obligations, enabling an efficient focused search compared to a PDR portfolio. Our second new algorithm, PD-PDR, sequences subproblems according to the compositional structure of the concrete problem at hand. Subproblems are solved independently in parallel, with a concrete plan obtained by combining subproblem plans. Our experimental evaluation exhibits strong runtime gains for both new algorithms in both satisfiable and unsatisfiable planning benchmarks.