[ CogSci Summaries home | UP | email ]
http://www.jimdavies.org/summaries/

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.

@InProceedings{aaai96-2*1194,
  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:

System: never named but later referred to as SATplan.
A new planning paradigm, namely planning as propositional satisfiability solved by local search.
Planning as stochastic search (Walksat) in the space of propositional SAT problems (as opposed to the traditional view of planning as systematic search in the state space or the space of partial plans).
Knowledge representation:
The choice of encoding influences performance: graphplan-based vs. direct (linear or state-based) encodings.
A representation based on fluents can make the encoding of a planning problem more compact and a solution easier to obtain.
As in ASP, compactness of the representation is increased using an arity-decreasing trick.

Summary

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 |
   +------------------------------------------------------+
                               |
                            encoding
                               |
                               V
+------------------------------------------------------------+
| propositional SAT problem (i.e., a ground sentence in CNF) |
+------------------------------------------------------------+
                               |
                         simplification
                               |
                               V
             +----------------------------------+
             | a shorter ground sentence in CNF |
             +----------------------------------+
                               |
                  stochastic/systematic search
                               |
                               V
   +---------------------------------------------------+
   | solution to the SAT problem in the form of a set  |
   | of assignments of truth values to ground literals |
   +---------------------------------------------------+
                               |
                        plan extraction
                               |
                               V
                       +---------------+
                       | solution plan |
                       +---------------+

Comparison	Traditional planning framework	SATplan
Representation language	STRIPS or 1st order logic	propositional sentence in CNF
Search space	state or plan space	space of SAT problem
	implicitly represented	explicitly represented
	operator-based	state-based
Type of search	systematic	stochastic
Complenetess	yes	no
Directedness	progression or regression	random
Scaling	poor	good

Detailed outline

Encoding step

Graphplan-based encodings can be obtained automatically (i.e., transformation of planning graphs into propositional sentences in CNF).
Linear encodings lead to totally ordered plans.
In state-based encodings, axioms relate fluents (ground atoms) between adjacent states. There are no frame axioms, no description of operators nor of conflicts between them.

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

It is very memory intensive.
It is not complete when using stochastic SAT procedures.
It needs to work iteratively if the optimal plan length is not known in advance.
The quality (compactness, expressive power) of the encoding is crucial for good performance but it is still an art at this point(i.e., it is not automated yet).
It is not clear how to do conditional planning and how to interleave planning and acting since the search is not directed like in progression/regression planners.

Summary author's notes:

Thanks to Sven Koenig for discussions of SATplan.

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