From: Stefan B. Sigurdsson (stebbi_at_cs.washington.edu)
Date: Tue Apr 08 2003 - 10:30:11 PDT
Summary - Earlier work (Kautz 92, 96) demonstrated the feasibility of manually converting planning problems in STRIPS-like domains to propositional satisfiability (SAT) problems, and subsequently deriving a valid plan by applying a reverse conversion to the output of a SAT solver. This paper examines different methods to automate the conversion. The main contributions are in the form of (a) an analytical model for classifying different approaches to conversion, and (b) experimental results collected by using a SAT compiler created by the authors to apply each approach to a corpus of planning problems.
Key ideas
- The analytical model classifies conversion methods along two axes; (a) the granularity of the conversion of plan actions to boolean propositions, and (b) the use of boolean statements that enumerate objects that are not affected by an action ("classical") vs. statements that enumerate what possible actions may be the cause of a state change ("explanatory").
- Exclusion is introduced to ensure that derived partial-ordered plans have a well-defined conversion to totally-ordered plans.
- The discussion of factoring is easily the most involved aspect of the paper. The objective here is to decrease the size of the SAT problem. I'm sure this has subleties that I didn't get - it would be good to spend time on this in class.
Questions
- I find it easier to regard this paper as a study into the feasibility of automated SAT compilation, rather than an end result demonstrating the superior value of a particular approach, or class of approaches. This is due to a lack of clear patterns in the graphs presented in the experimental results (or perhaps I simply couldn't discern these patterns). However, the graphs do show clearly that automated compilation is viable, which is a valuable result on its own.
- The most valuable pattern that can be discerned is probably that explanatory frame axioms are superior to classical ones, which is intuitively comforting as long as the test problems are characterized by a relatively low number of actions per time step, compared with the number of domain objects. However, if during any (most) time steps the majority of objects were operated on, I would expect use of classical frame axioms to result in smaller plans. Is the authors' assumption of "small" action effects generally valid?
- I thought the discussion of searching for minimal plans was a bit weak. Intuitively this seems quite a big issue since each invocation of the SAT solver only searches for plans of a certain length.
Directions
- The main downside to the paper is that the test corpus does not reveal sufficiently clear distinctions between different compilation methods. This points to further attempts at corpus generation and classification.
- Given a more systematic understanding of the test corpus (by the community, or just me ;) the most obvious next step to follow up on this research would be to classify the value of different compilation methods according to the characteristics of different corpus problems, and then attempt to automate the selection of compilation method to find the one "best" suited to the specific problem at hand.
- This may be naive. Notice that (a) complex propositions are always equivalent to conjunctions/disjunctions of simple ones, and (b) STRIPS actions and objects can always be represented by propositions. Given these facts (?) should it not be possible to classify the complexity of a planning problem? Could such a classification lead to analytical bounds on the resource consumption of a SAT compiler? Could it form the basis for automating the "correct" selection of compilation method for a given planning problem?
This archive was generated by hypermail 2.1.6 : Tue Apr 08 2003 - 10:30:12 PDT