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.
Type de document :
Article dans une revue
Journal of Artificial Intelligence Research, Association for the Advancement of Artificial Intelligence, 2009, 36, pp.415-469. 〈10.1613/jair.2817〉
Liste complète des métadonnées

Littérature citée [58 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00430781
Contributeur : Joerg Hoffmann <>
Soumis le : vendredi 12 novembre 2010 - 18:01:37
Dernière modification le : jeudi 11 janvier 2018 - 06:19:50
Document(s) archivé(s) le : vendredi 26 octobre 2012 - 15:27:02

Fichier

jair09b.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

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〉

Partager

Métriques

Consultations de la notice

209

Téléchargements de fichiers

175