Automatic SAT-compilation

From: Danny Wyatt (danny_at_cs.washington.edu)
Date: Wed Nov 05 2003 - 08:22:21 PST

  • Next message: Alan L. Liu: "Paper review: Automatic SAT-Compilation of Planning Problems"

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

    Summary:

    The authors describe an optimizing compiler for transforming STRIPS
    planning problems into propositional satisfiability problems.

    Two Most Important Ideas:

    Optimizations in compiling planning problems into propositional logic
    can be automated. To comment in the context of this course: Russel &
    Norvig mentioned that ways of optimizing split clauses exist, but the
    example they gave seemed to rely on problem-specific knowledge. I
    wondered how amenable optimizations were to full automation and how much
    they had to be done by hand. This paper (particularly section 3)
    certainly answered that question. (Indeed, the example in R&N looks
    like it would have been factored by the A \Rightarrow P,E factoring
    described in 3.1.)

    These optimizations might not have a large noticeable effect. I was
    impressed with splitting and the factoring that it allowed, but the
    results of its use on sample problems didn't show much---if
    any---improvement over compilations that used unsplit actions. Indeed,
    representations with split actions performed more poorly than unsplit
    representations most of the time. So while they definitely reduce the
    worst case bound, that might not be worth their effect on the average case.

    Two Flaws:

    There are no flaws in this paper. I think it a crime that the authors
    have yet to win the Turing award. That said, I would like to hear more
    about the type optimizations since the authors credit them with
    contributing the most to the efficiency of their representations.

    Two Open Questions:

    How would this compiler's results change with a different sat
    algorithm? R&N mention that DPLL performs better than WalkSAT for
    planning problems, so I'd like to see how DPLL compares to WalkSAT on
    the compilers output. Though the number of variables or clauses won't
    change, their forms might and a different solver may handle them
    differently.

    There are more optimizations to be considered. Splitting, factoring
    split representations, and type optimizations seem like just a few of
    the possible optimizations that can be performed. What others can be
    found and how will they compare?


  • Next message: Alan L. Liu: "Paper review: Automatic SAT-Compilation of Planning Problems"

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