Skip to Main content Skip to Navigation
Journal articles

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

Carmel Domshlak 1 Joerg Hoffmann 2 Ashish Sabharwal 3
2 MAIA - Autonomous intelligent machine
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
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.
Document type :
Journal articles
Complete list of metadata

Cited literature [58 references]  Display  Hide  Download
Contributor : Joerg Hoffmann <>
Submitted on : Friday, November 12, 2010 - 6:01:37 PM
Last modification on : Friday, June 11, 2021 - 5:12:08 PM
Long-term archiving on: : Friday, October 26, 2012 - 3:27:02 PM


Files produced by the author(s)




Carmel Domshlak, Joerg Hoffmann, Ashish Sabharwal. Friends or Foes? On Planning as Satisfiability and Abstract CNF Encodings. Journal of Artificial Intelligence Research, Association for the Advancement of Artificial Intelligence, 2009, 36, pp.415-469. ⟨10.1613/jair.2817⟩. ⟨inria-00430781⟩



Record views


Files downloads