Review of Automatic SAT-Compilation of Planning Problems

From: Alexander Yates (ayates_at_cs.washington.edu)
Date: Tue Apr 08 2003 - 13:26:44 PDT

  • Next message: Rhoiclya: "FW: Academic Software Discounts"

    "Automatic SAT-Compilation of Planning Problems" by Michael Ernst, Todd
    Millstein, and Dan Weld.

    This paper describes eight different strategies for automatically
    translating STRIPS planning problems into SAT problems, and it reports on
    experimental results testing the relative merits of the strategies.

    This paper describes a parameterized view of the space of possible encodings
    into SAT, with one dimension being the action representation and the other
    being the choice of frame axioms. The ability to parameterize this space is
    important for the purpose of understanding and comparing different
    representations, and in this work leads to the result that encodings using
    explanatory frame axioms outperform those using classical frame axioms. A
    second important contribution is the idea of factoring the encodings of
    various axioms and the split action shemas to reduce clause size and the
    number of clauses. These are forms of automatic symmetry detection that can
    greatly reduce the solution time.

    Because some of the encodings (classical, explanatory-split) did not allow
    parallel actions and others did allow them, I felt that a comparison along
    this dimension was lacking. The regular explanatory encoding and the
    bitwise explanatory encoding both performed well (regular was one of the
    best) in terms of encoding size and solution time, but from the results
    reported it was difficult to sort out to what extent the solution times were
    the result of better encoding size and to what extent they were the result
    of allowing or not allowing parallelism.

    I thought the most interesting opportunity for future research lay in the
    possibility of detecting such domain-specific symmetries as had been encoded
    by hand in the direct encodings of certain domains. It's clear that such
    symmetries are important for speed, and the examples provided by the direct
    encodings may give some intuition about how to find those symmetries.

    Alex


  • Next message: Rhoiclya: "FW: Academic Software Discounts"

    This archive was generated by hypermail 2.1.6 : Tue Apr 08 2003 - 13:26:45 PDT