From: MAUSAM (mausam_at_cs.washington.edu)
Date: Tue Apr 08 2003 - 10:57:15 PDT
Automated SAT-Compilation of Planning Problems
Ernst, Millstein and Weld
This paper extends the SATPLAN work by Kautz and Selman to generate
automatic SAT encodings of domains expressed in STRIPS representation.
There were a bunch of important ideas in the paper. The paper mentioned
different types of encodings including various split encodings which
might be useful in reducing the number of literals. Moreover, the paper
discussed different ways to generate the axioms. The authors also realised
that sometimes one could use split encodings to our advantage by factoring
the axioms thus reducing the size of SAT encoding. Finally the authors
mentioned several optimisations that could be employed to reduce the size
of the encoding like a consistency analysis of fluents which could be true
(or false) etc.
The experiments although done comprehensively have not been done with a
clear thought behind. The authors test everything on every problem they
consider. This leads the graphs to be highly confusing (as there are many
data points) and it becomes difficult to gather meaningful conclusions
from them. Some of the surprising results like split encodings are not
helpful compared to the regular ones should have been dealt in more
detail. It seems that there is major trade-off between number of
literals and size of encoding going on here.
The authors mentioned that regular and simply-split explanatory are the
best, the graphs suggest that regular-explanatory are the best. There are
very few cases where simply split work better than regular. Does that mean
there is no effect of factoring??? Or what are the other possibilities?
The authors tried several optimizations. But, they only showed usefulness
of the type optimizations. Some details about others would have been
helpful.
I think the authors should also have shown the results of the times taken
by other non-SAT planners like Graphplan etc. just to prove the usefulness
of this whole exercise.
I think the most important future work is to try and formalize the notion
of different types of domains so that by doing some static analysis of the
domains we get to know which encoding and what type of axioms to use.
Moreover, since we saw that regular explanatory encoding outperform the
others, it suggests that there are not much gains in splitting the
encoding since the number of axioms play a more dominant role. Hence, we
need to look for other ways to write the axioms which may tend to reduce
the size and thus the time.
This archive was generated by hypermail 2.1.6 : Tue Apr 08 2003 - 10:57:16 PDT