Automatic SAT-compilation of planning problems

Download: PDF, Medic implementation.

“Automatic SAT-compilation of planning problems” by Michael D. Ernst, Todd D. Millstein, and Daniel S. Weld. In IJCAI-97, Proceedings of the Fifteenth International Joint Conference on Artificial Intelligence, (Nagoya, Aichi, Japan), August 23-29, 1997, pp. 1169-1176.


Recent work by Kautz et al. provides tantalizing evidence that large, classical planning problems may be efficiently solved by translating them into propositional satisfiability problems, using stochastic search techniques, and translating the resulting truth assignments back into plans for the original problems. We explore the space of such transformations, providing a simple framework that generates eight major encodings (generated by selecting one of four action representations and one of two frame axioms) and a number of subsidiary ones. We describe a fully-implemented compiler that can generate each of these encodings, and we test the compiler on a suite of STRIPS planning problems in order to determine which encodings have the best properties.

Download: PDF, Medic implementation.

BibTeX entry:

   author = {Michael D. Ernst and Todd D. Millstein and Daniel S. Weld},
   title = {Automatic {SAT}-compilation of planning problems},
   booktitle = {IJCAI-97, Proceedings of the Fifteenth International Joint
	Conference on Artificial Intelligence},
   pages = {1169--1176},
   address = {Nagoya, Aichi, Japan},
   month = {August~23--29,},
   year = {1997}

(This webpage was created with bibtex2web.)

Back to Michael Ernst's publications.