Automatic SAT-Compilation of Planning Problems

From: Raphael Hoffmann (raphaelh_at_u.washington.edu)
Date: Thu Sep 04 2003 - 22:56:03 PDT

  • Next message: Masaharu Kobashi: "Review on Paper 3"

    "Automatic SAT-Compilation of Planning Problems"
    by Michael D. Ernst, Todd D. Millstein, Daniel S. Weld

    The paper discusses the efficient solving of planning problems by compiling
    their STRIPS representations into SAT. Several representations of actions,
    frame axioms and factoring techniques are being explained and their
    efficiency is evaluated.

    The authors performed an unbiased comparison of eight different encodings;
    the test data comprised 24 planning problems. At first glance, the results
    appear pretty mixed, as the rankings of the encodings differ across the
    planning problems. However, the two best and two worst encodings can be
    identified and the results are surprising: The best encodings were dismissed
    by Kautz and Selman, while the worst encoding (bitwise) was the smallest
    encoding before simplification. This clearly underlines the importance of
    research in this field. Furthermore, the magnitudes of efficiency gained
    through encoding optimizations is indeed impressive, and even leads to the
    suggestion that compilation to SAT might yield the fastest planner.

    It is pointed out that Kautz and Selman’s encodings which used hand-coded,
    domain-specific information that could not be specified in STRIPS,
    dramatically speeded up the computation. My personal impression is that
    STRIPS is not the ideal choice in many applications. Its limited expressive
    power makes it impossible to formulate certain conditions. One would expect,
    that STRIPS limited expressive power at least allows to speed up
    computations. However, as this research paper shows this is not always the
    case (e.g. the number of variables quickly increases). I assume that it
    could be a good idea to allow domain-specific axioms in real-world
    applications.
    Further research might give answers to questions such as “How/When can I
    extend the language to speed-up computation and/or increase expressiveness”.

    The encodings were evaluated by solving 24 planning problems. Since the
    results differed across some tests, the total number of tests appears rather
    low. If we had a huge set of tests, we might even be able to make an
    a-priori optimal choice of the encoding by looking at the characteristics of
    the planning problem.
    I am wondering if it is possible to automatically generate a set of relevant
    and important planning problems. These could be used as input to comparing
    the encodings.


  • Next message: Masaharu Kobashi: "Review on Paper 3"

    This archive was generated by hypermail 2.1.6 : Tue Nov 04 2003 - 22:56:16 PST