From: Keith Noah Snavely (snavely_at_cs.washington.edu)
Date: Wed Nov 05 2003 - 02:21:41 PST
"Automatic SAT-Compilation of Planning Problems" by Ernst,
et. al. describes a compiler from a language of planning problems to
instances of SAT, and uses it to evaluate the speed of solving
planning problems under eight ways of encoding to propositional logic.
The most important contributions of this work seems to be the fact
that solving planning problems using SAT solvers, shown to be fast in
previous work by Kautz, can now be done automatically with a compiler.
In addition, this compiler provides a testbed for comparing various
encodings of planning problems in the language of propositional logic.
The value of this is shown in empirical tests performed by the authors
themselves, which contradict certain expectations.
The compiler also performs several optimizations to reduce the size of
the output formula. However, the formulae it produces take longer to
solve than hand-coded formulae. There was a suggestion that the
hand-coded SAT instances could be solved quickly compared to the speed
of other planners, but from this work it is not clear how
automatically compiled SAT instances stand compared to other methods.
Also, the paper gives the solve times but not compile times for the
output SAT instances; it mentions that for larger problems the solve
time dominates the compile time. As the optimization stage gets more
complicated, however, this might change (for instance, like SAT, some
optimizations for traditional compilers, e.g. register allocation, are
NP-complete). Just as there are possible tradeoffs between encodings,
there may also be tradeoffs for optimizations such as finding
domain-specific axioms. One other thing that I wasn't sure about was
the overall structure of compiled SAT instances, and how much the
structure changes from problem to problem (e.g. does the monkey1
formula look like the fridge2 formula)? If common elements of these
instances could be characterized, perhaps specialized SAT solvers
could be built for them, or Walksat parameters can be chosen more
intelligently.
This archive was generated by hypermail 2.1.6 : Wed Nov 05 2003 - 02:21:42 PST