From: Bhushan Mandhani (bhushan_at_cs.washington.edu)
Date: Wed Nov 05 2003 - 12:57:31 PST
Title: Automatic SAT-Compilation of Planning Problems
Authors: Michael Ernst, Todd Millstein and Daniel Weld
Summary: The paper uses an automatic compiler that takes as input, a
STRIPS-style planning problem, compiles it into a satisfiability problem
in propositional logic using one of eight different methods, and solves
the SAT problem to solve the planning problem. The eigth different
encodings are generated by choosing one of regular, simple operator
splitting, overloaded operator splitting and bitwise representations for
representing actions, and either classical or explanatory frame axioms to
take care of unaffected fluents for an action. The goal is to compare the
usefulness of these different encodings.
Important Ideas:
1. The regular and simply split encodings with explanatory frames were the
smallest encodings. Typically, one would expect regular encoding to be the
largest. But type optimizations built into the compiler kept it small.
Type optimizations were found to be quite important.
2. Factoring axioms (which allows us to have variables refer to parts of
an action rather than the complete action) is important, and results in
significant reduction in clause size and number of literals.
3. Explanatory frames are clearly superior to classical frame axioms.
Flaw:
Figure 6 in the paper has symbols of 9 different types scattered in the
graph, making it a little difficult to interpret it. It could have been
supplemented with tabular data.
Future Directions:
1. Extending type optimizations to discovering more general
domain-specific axioms from the problem.
2. Exploring novel and hybrid encodings. For example, using bitwise
representation to encode the fluents of split actions (note that this
doesn't cause the disadvantages that occurred when actions were encoded
bitwise).
This archive was generated by hypermail 2.1.6 : Wed Nov 05 2003 - 12:57:33 PST