From: Kevin Sikorski (kws_at_cs.washington.edu)
Date: Tue Apr 08 2003 - 11:46:18 PDT
Paper title/author:
Automatic SAT-Compilation of Planning Problems
Michael D. Ernst, Todd D. Millstein, Daniel S. Weld
One-line summary:
The paper proposes a framework of encodings for solving STRIPS, and
provides an optimizing compiler for automatically producing these
encodings.
The (two) most important ideas in the paper, and why:
Recent work shows that reducing STRIPS-style planning problems into
satisfiability problems is an efficient approach to planning. However,
previous such approaches used hand-encodings to convert the problems.
Producing a compiler to automate this process is a natural continuation of
this, and frees humans from producing such reductions manually.
The optimizations themselves are what make automated compilation feasible.
Without them, the resulting formulae are too complex to solve in a timely
fashion. Specifically, Factoring seems to be the more important
optimization, as it produces the best average optimization ratio.
The one or two largest flaws in the paper:
Finding new optimizations to perform on the converted SAT problems could
dramatically improve efficiency. For example, the four types of action
representations represent points in the continuum of tradeoffs between the
number of variables and the number of clauses. Having more than four
points could provide a better tradeoff.
The authors admit that they did not perform serious experiments to
determine if a linear search or binary search is more efficient when the
plan length is unknown. I do not have much experience in solving
real-world SAT problems, but I understand that worst-case exponential time
problems are fairly rare in practice. Thus, for problems with only very
long plans as solutions, it may be that binary search is faster than
linear solutions. In fact, it may be advantageous to use both approaches
- interleaving them, or choosing one based on a heurisitic that estimates
plan length based on SAT-formula complexity.
Identify two important, open research questions on the topic,
and why they matter:
The approach assumes that a potential user has a STRIPS-compatible
problem, or can formulate its problem in STRIPS form. It would be nice to
see how easily this approach of automatically compiling and optimizing
problems into a satisfiability problem could be adapted to other problem
frameworks.
From a theoretical standpoint, one could say that all NP-complete problems
are equivalent in that if you can solve one, you can solve them all. But
is SAT the best problem to be translating STRIPS problems into? I believe
that it is probably the most intuitive problem to reduce planning to, but
converting to another analogous problem may yield better optimizations.
This archive was generated by hypermail 2.1.6 : Tue Apr 08 2003 - 11:46:19 PDT