From: Christophe Bisciglia (chrisrb_at_cs.washington.edu)
Date: Tue Apr 08 2003 - 13:00:31 PDT
Automatic SAT-Compilation of Planning Problems . M. Ernst, T. Millstein,
D. Weld
This paper discusses means to automatically compile STRIPS planning
problems to SAT problems.
I am personally having a bit of trouble swallowing the whole paper, but
even with my lesser experence in this area, I think I have a reasonable
grasp on the two main ideas from the paper. First, Kautz showed in his
earlier work that planning problems could be reduced to satisfiability
problems, and the solution to the SAT could be converted back into a plan.
However, Kautz used hand conversion to SAT, which I can only imagine was
time consuming, but nevertheless, very compact. This paper shows that this
process can be automated by a SAT compiler. The paper emprically compares
the difference between 4 action representaions, and 2 frams axioms leading
to 8 different encodings. This is where I get a bit sketchy, but I think
the next main point is as such. A direct compilation seems to be bloated,
but the paper addresses this through optimizations that can be made to the
formula. Specifically, factoring dampens an exponential blowup in the size
of the formula (it was stated that in the worst case, it has no effect,
but in practice is quite useful).
The largest flaw in this paper I could detect had to do with explaining
the results. Even after staring at the graphs in figure 6, the dense data
points left me confused. Although section 5 explains some of this, when it
refers back to the graphs, it looses me. The most convincing explanations
of the experiments to me were in section 5.3 and the comparison to
Satplan. I was impressed that an automated compiler could come within a
factor of 2 of a hand generated compilation. Another aspect of this paper
was mention earlier by Krzysztof, and I to find it concerning that path
lengths must be specified ahead of time. This seems to work sell with
familiar problems, but I question how well it would generalize to more
complicated, less familiar problems.
What interests me with respect to further research stems form an
assumption about how things are working with solving SAT. Since SAT is
NP-C, I.m assuminmg some heuristic solution is being used. Since NP-C
problems are all reducible to eachother, I wonder if NP-C problems with
better heuristic solutions might yield better planners. Another thing that
would be interesting to explore, and this may be naïve, but since this
approach requires the path length to be specified up front, I wonder if
one could come up with a way to make an educated guess at the path length
from the problem description, and start looking for paths around that
length, and then exploring paths of lenths farther off.
This archive was generated by hypermail 2.1.6 : Tue Apr 08 2003 - 13:00:32 PDT