Friends or Foes? On Planning as Satisfiability and Abstract CNF Encodings

Abstract

Planning as satisfiability, as implemented in, for instance, the SATPLAN tool, is a highly competitive method for finding parallel step-optimal plans. A bottleneck in this approach is to *prove the absence* of plans of a certain length. Specifically, if the optimal plan has N steps, then it is typically very costly to prove that there is no plan of length N-1. We pursue the idea of leading this proof within solution length preserving abstractions (over-approximations) of the original planning task. This is promising because the abstraction may have a much smaller state space; related methods are highly successful in model checking. In particular, we design a novel abstraction technique based on which one can, in several widely used planning benchmarks, construct abstractions that have exponentially smaller state spaces while preserving the length of an optimal plan.





Surprisingly, the idea turns out to appear quite hopeless in the context of planning as satisfiability. Evaluating our idea empirically, we run experiments on almost all benchmarks of the international planning competitions up to IPC 2004, and find that even hand-made abstractions do not tend to improve the performance of SATPLAN. Exploring these findings from a theoretical point of view, we identify an interesting phenomenon that may cause this behavior. We compare various planning-graph based CNF encodings F of the original planning task with the CNF encodings F_abs of the abstracted planning task. We prove that, in many cases, the shortest resolution refutation for F_abs can never be shorter than that for F. This suggests a fundamental weakness of the approach, and motivates further investigation of the interplay between declarative transition-systems, over-approximating abstractions, and SAT encodings.