Property Directed Reachability for Planning Revisited

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.