From: Alan L. Liu (alanliu_at_u.washington.edu)
Date: Wed Nov 05 2003 - 08:27:23 PST
Paper title: Automatic SAT-Compilation of Planning Problems
Authors: Ernst, Millstein, and Weld
Summary: The paper describes a novel way of solving STRIPS planning
problems by using a compiler to encode them to SAT.
Important ideas:
By converting a problem space from one domain to another, one can
exploit the solution algorithms in the new domain that might have no
equivalent in the old domain. In this case, by processing STRIPS
planning problems into SAT, one can benefit from the average
running-time of WalkSAT. The paper shows that it is possible and
feasible to do this conversion automatically.
Another important idea is the idea of testing experimental variables. In
this case, the authors compare 8 different encodings, examining the
speed at which they were solved, and gleaned insight on some properties
that affect the solving speed.
Flaws:
In the introduction, there is a tantalizing bit about how this could
make the "world's fastest STRIPS-style planner." However, the paper
makes no mention of other state-of-the-art planning methods, so there is
no way to compare.
I may have missed it, but what kind of running time does the compiler
take (although I assume it's polynomial to some factor of the problem
definition).
Future directions:
Could this technique of conversion to SAT be used to make fast methods
for other domains, besides planning? What other optimizations can be
done to make the compiler output even faster (the paper says that Kauthz
and Selman were able to hand-craft SAT encodings that were roughly half
the size, so there's an achievable goal right there)?
This archive was generated by hypermail 2.1.6 : Wed Nov 05 2003 - 08:27:19 PST