Automatic SAT-Compilation of Planning Problems
Proceedings of the 15th International Joint Conference on Artificial Intelligence (IJCAI 1997), Nagoya, Aichi, Japan, August 23-29, 1997.
Michael Ernst, Todd Millstein, Daniel Weld
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.
[PDF | Implementation]