From: Krzysztof Gajos (kgajos_at_cs.washington.edu)
Date: Tue Apr 08 2003 - 12:45:43 PDT
Automatic SAT-Compilation of Planning Problems
by Enrst, Millstein and Weld
This paper describes a number of boolean encodings for STRIPS plans,
examines their relative sizes, and explores their relative usefulness
for solving STRIPS-based planning problems with boolean satisfiability
methods.
This paper builds on earlier results that show that hand-converted
planning problems could be solved efficiently using modern SAT
solvers. The particular contributions of this paper were:
-- enlarging the space of possible encodings to cover broader set of
possibilities in the tradeoff between minimizing number of clauses
and minimizing the number of variables
-- providing an automated method for creating this encodings out of
STRIPS plan descriptions
-- producing experimental results indicating which of these methods
were best suited for different classes of problems in practice.
One of the ideas that I found most interesting in the paper was the
use of explanatory frames as an alternative to classical frames for
tying actions with their effects.
A somewhat worrying aspect of this work (and, it seems, SAT-based plan
solving in general) is that the plan length has to be prespecified.
If it is not known, the system needs to make guesses regarding the
right plan length. If a minimum length plan is desired, up to log(max
length) searches need to be attempted where max length is an uppper
limit on how long the plan can possibly be. Finally, the authors
permit parallel plans in their implementation and are able to find the
minimal length parallel plans but cannot make any guarantees that the
solution will also have the shortest linearization.
As far as the future work is concerned, however, it seems that a
restricted version of temporal planning could be accomplished using
this method without much difficulty given that notion of time is
already very explicit in the resulting encoding.
This archive was generated by hypermail 2.1.6 : Tue Apr 08 2003 - 12:45:44 PDT