Automatic  SAT-Compilation  of Planning Problems

Ernst, Millstein, and Weld

Summary

The  system  that  the  paper  introduces  compiles,  typechecks,  and
optimizes planning problems to SAT rivaling hand-optimized encoding to
a factor of two.

The  most  striking  feel that the paper gives is that it looks like a
1956  paper  describing  compiling  a high-level language to assembler
without  much  loss of speed, but taken to planning problems. It's all
in  there:  peephole  optimizations,  deciding  between alternate data
representations,  a  type  system,  factoring  (can  you  say  "common
subexpression  elimination"?)  and  so on. This paper really marks the
dawn  of  automated  language  translation  (with  all  of its body of
knowledge,  frameworks,  methods,  and  strengths)  into  the  problem
planning world.

Two most important ideas

The  most  important  idea  of  the  paper  is  that encoding planning
problems  into SAT can be performed automatically, and that there is a
generous space of optimization opportunities that can be performed.

Another  important  idea  is  that  the  compiler  can investigate and
analyze  statically various tradeoffs (often conflicting ones, such as
bitwise splitting versus number of clauses). For large problems, it is
likely the compiler can do a better job than a human.

Flaws

NO FLAW. Dan is among the authors :o).

Kidding.

I  would  have enjoyed seeing the authors pursuing the matter further.
They  seem  to  have  stopped research in that area, and therefore the
impact  of  their  work  is maybe not as strong as it could have been.
Other  researchers  haven't  continued  the  work either, according to
CiteSeer; maybe the AI community is ok with encoding planning problems
to  SAT  by  hand,  or the performance numbers haven't been compelling
enough.  Or  a  combination of the two. At any rate, maybe a follow-up
paper  showing  better  optimizations  and stronger results would have
increased the impact of these ideas.


Best regards -- Andrei