[ CogSci Summaries home | UP | email ]

H. Kautz and B. Selman (1996). Pushing the Envelope: Planning, Propositional Logic and Stochastic Search, Proceedings of the Thirteenth National Conference on Artificial Intelligence (AAAI-96), Portland, OR.

The paper is online.

  author =       "Henry Kautz and Bart Selman",
  title =        "Pushing the Envelope: Planning, Propositional Logic
                 and Stochastic Search",
  pages =        "1194--1201",
  ISBN =         "0-262-51091-X",
  booktitle =    "Proceedings of the Thirteenth National Conference on
                 Artificial Intelligence and the Eighth Innovative
                 Applications of Artificial Intelligence Conference",
  month =        aug # "~4--8",
  publisher =    "AAAI Press / MIT Press",
  address =      "Menlo Park",
  year =         "1996",

Author of the summary: David Furcy, 1999, dfurcy@cc.gatech.edu

Cite this paper for:


In the new paradigm, planning reduces to finding a model for a ground propositional sentence in conjunctive normal form (or CNF). This sentence captures the constraints that exist between states and actions. Note that in the translation process, most of the structural information of the domain is compiled away. Then a model (that is an interpretation that makes the sentence true) is found using stochastic or systematic SAT algorithms (i.e., search algorithms). The whole process can be summarized as follows:

   | planning problem description in STRIPS-like language |
| propositional SAT problem (i.e., a ground sentence in CNF) |
             | a shorter ground sentence in CNF |
                  stochastic/systematic search
   | solution to the SAT problem in the form of a set  |
   | of assignments of truth values to ground literals |
                        plan extraction
                       | solution plan |

ComparisonTraditional planning frameworkSATplan
Representation language STRIPS or 1st order logic propositional sentence in CNF
Search spacestate or plan space space of SAT problem
implicitly representedexplicitly represented
Type of searchsystematicstochastic
Directednessprogression or regressionrandom

Detailed outline

Encoding step

Simplification step

This is a straightforward simplification of the propositional sentence using standard logic inference rules such as unit propagation, subsumption and deletion of unit clauses.

Resolution of the SAT problem

Both a systematic and a stochastic search algorithms have been tested. The systematic tableau procedure is based on the Davis-Putnam procedure (it is not described here).

On the other hand, Walksat is a randomized greedy local search method for satisfiability testing. This method, combined with state-based encoding clearly outperforms both the systematic procedure and Graphplan. Note that this new paradigm is in sharp contrast with the use in standard planners of specialized and systematic search techniques using the structure of the domain.

Finally, systematic search methods present the advantage of providing lower bounds for the optimal plan length whereas stochastic procedures scale better and can actually find (possibly non-optimal) solutions to harder problems.

Plan extraction step

Once a solution to the SAT problem has been found, a plan can be constructed by searching for and chaining operators that explain changes between temporally adjacent states. This process can be performed in linear-time for the domains that were tested.

Strengths of SATplan

SATplan is most efficient when using walksat and direct encodings. In particular in the chosen domains, SATplan is orders of magnitude faster than Graphplan while still finding optimal plans. Several reasons are proposed for this success. The first one is the use of compact and very expressive propositional encodings. Another is the speed of new SAT algorithms (specifically walksat). Finally, another advantage of the approach is that it does not worry about operators' interactions and subgoal ordering. This is possible because the corresponding structure is abstracted away in a near-linear logical sentence.

Drawbacks of SATplan

Summary author's notes:

Back to the Cognitive Science Summaries homepage
Cognitive Science Summaries Webmaster:
JimDavies ( jim@jimdavies.org )
Last modified: Mon Apr 19 12:53:57 EDT 1999