From: Lillie Kittredge (kittredl_at_u.washington.edu)
Date: Wed Nov 05 2003 - 01:53:27 PST
Lillie Kittredge reviewing
Automatic SAT-Compilation of Planning Problems,
Micheal Ernst, Todd Millstein, Dan
Summary:
This paper describes a way to compile classical planning problems into any of eight encodings
of propositional satisfiability.
Important ideas:
-The paper shows by example that the space of SAT encodings can be neatly parameterized
along two dimensions, giving eight discreet subspaces. This is useful for those who make use
of SAT encodings, since it allows for clear comparison.
-It also shows by example that a compiler can be constructed to generate the encodings, and
that this compiler can be optimized to reduce the number of variables and the size of the
formula. So not only is it an automatic compiler, it produces a pretty good, efficient result.
Flaws:
Looks fine to me, once I figured out what was going on. Could stand to be clearer. And it
wouldn't hurt to compare it with more other planning methods, on maybe a larger suite of
planning programs.
Future directions:
This paper compiled SAT problems out of STRIPS. Can the same be done for more complex
systems than STRIPS? Can the optimization of the compiler be improved?
This archive was generated by hypermail 2.1.6 : Wed Nov 05 2003 - 01:53:28 PST