From: Karthik Gopalratnam (karthikg_at_cs.washington.edu)
Date: Wed Nov 05 2003 - 09:27:27 PST
Automatic SAT-Compilation of Planning Problems
- Michael Ernst, Todd Millsteiin, Daniel Weld.
(Review by Karthik Gopalratnam)
This paper presents a generlized compiler to convert planning
problems into propositional logic, without incorporating specialized
domain knowledge. The paper aims to leverage the advances in solving
satisfiability problems, specifically the WalkSAT algorithm, to solve
general planning problems.
The major ideas in the paper are:
* It is possible to formulate planning problems in the mold of
propositional satisfiability problems without incorporating domain
specific knowledge, since the SAT problems can be (in general) practically
solved using stocastic search as shown by the WalkSAT algorithm. In light
of this intuition, the paper presents a formalized framework to encode
planning problems as SAT problems. The paper characterizes the space of
encodings along two orthogonal directions - Action representations, and
frame axioms, and analyzes the theoretical aspects of the eight such
general encodings in this space.
* From a practical point of view, the paper demonstrates the
construction of a compiler to make use of the framework analyzed earlier.
The MEDIC planner that is presented in the paper makes use of various
optmization techniques to minimize the collective size of the SAT problem
presented to the SAT solver. These optminizations are performed through
factoring, and the paper presents the methods of factoring all the frame
axioms discussed, and uses these methods in the implementation of the
MEDIC planner.
The paper does not seem to address the effectiveness of the MEDIC planner
on specific planning problems. Of course, given the intuitions of the
paper, it is reasonable to assume that the plans generated are as good as
the underlying SAT solver, but it is difficult to guage the encodings
qualitatively - i.e. are the solution plans the shortest length, etc.
In light of the general framework presented here, it would be
interesting (if not already explored) to extend this framework to allow
for specifying domain specific information in converting planning problems
into SAT problems, and whether the inclusion of such intuition in the
compilation process itself results in better plans.
This archive was generated by hypermail 2.1.6 : Wed Nov 05 2003 - 09:27:29 PST