Automatic SAT-Compilation of Planning Problems (Ernst et al., 1997)

From: Daniel Lowd (lowd_at_cs.washington.edu)
Date: Wed Nov 05 2003 - 00:48:07 PST

  • Next message: Lillie Kittredge: "paper 3 review"

    "Automatic SAT-Compilation of Planning Problems" (Ernst et al. 1997)

    This paper compared the relative performance of different methods for
    representing planning problems as SAT instances.

    The most important contributions of this paper are a proof (by demonstration)
    that planning problems can be automatically solved by way of SAT, and an
    analysis of different methods for doing so. By proving the idea viable,
    it could inspire work by other researchers that might have better compilation
    approaches, yielding a better planner. Furthermore, by representing a
    planning problem as SAT, one can readily apply all improvements in SAT
    solvers to a planner. This paper further demonstrated some of the different
    options and optimizations to consider when doing this transformation,
    and the effects of each choice. The level of specificity, though somewhat
    painful to read, makes the work possible to reproduce even without the
    source code. All the cumbersome details also demonstrate the difficulty
    of doing this transformation effectively, so that the problem is tractable.

    While it succeeded in presenting a number of dimensions to this problem,
    it failed to compare the SAT planner to any traditional planning approaches.
    Is the new planner faster or slower? If it's faster, then we should start
    using it on more planning problems. If it's slower, then we should look for
    improvements or keep it in mind as an alternative.

    It remains an open question if there is a unified approach that will always
    yield a strictly better compilation than any individual approach, for any
    planning problem. While two methods came out ahead overall, it would be nice
    not to have to choose between them. Furthermore, it would be good to know if
    this approach could be extended to continuous variables, or if the explosion
    imposed by a discretization makes it intractible. Many planning problems,
    such as directing a manipulator arm on a robot, involve many continuous
    variables, and it would be nice to solve these as well.


  • Next message: Lillie Kittredge: "paper 3 review"

    This archive was generated by hypermail 2.1.6 : Wed Nov 05 2003 - 00:48:08 PST