From: Masaharu Kobashi (mkbsh_at_cs.washington.edu)
Date: Tue Nov 04 2003 - 22:58:42 PST
Title: Automatic SAT-Compilation of Planning Problems
Authors: Michael D. Ernst, Todd D. Millstein, Daniel Weld
[Summary]
This paper reports the successful creation of an innovative
compiler to convert planning problems into propositional
satisfiability problems.
[Most important ideas]
Needless to say, the value of this paper comes from the
creation of, presumably the first, compiler which can
automatically convert the planning problems to SAT problems
with remarkable efficiency.
Second, their compiler is feature rich with the capability
of generating as many as eight encodings, and they incorporated
many nice ideas into the compiler such as type optimizations,
partial action execution etc.
Finally, they made the code of the compiler open and
available for inspection and testing to the public.
That is a very important point and should not be
underestimated. It is worth more than thousands of words.
[Shortcomings of the paper]
First, its effect on the qualitative behavior of planning
is not covered.
Second, the significance of the conversion of the
planning problem to SAT-problem in the planning world
has not been addressed.
Third, if I am not misunderstanding the context of the paper,
some actions taken by the designer of the compiler may
have problematic effect on the behavior of the resulting
planning. For example, the factoring of exclusion axioms
by removing all possibilities of simultaneous actions, etc.
(It may be due to my lack of understanding the paper.)
[Two important open research questions]
First, there may be better encoding than those investigated
in this paper.
Second, research on the automatic generation of domain-specific
axioms, as mentioned in the paper, is an important open question.
This archive was generated by hypermail 2.1.6 : Tue Nov 04 2003 - 22:58:42 PST