From: Xu Miao (xm_at_u.washington.edu)
Date: Wed Nov 05 2003 - 09:33:43 PST
Title: Automatic SAT-compilation of planning problems
Author: Michael D.Ernst, Todd D. Millstein, and Daniel S. Weld
Reviewer: Xu Miao
Summary:
This paper analyzed the worst case problem size in term of
asymptotic numbers of literals for eight major encodings. And using a MEDIC
compiler test the plan problem solving-time. With all these information,
this paper compare the properties of these eight encodings.
Background:
Kautz el. Al. provides a scheme to solve the plan problem by
translating them to a clausal form and then sovling them by WalkSAT. There
are eight major encoding methods generated by combination of four action
representations and two frame axioms. The problem is which one of them could
be the best choice.
Important ideas:
1. Made a framework of generating the eight encodings(non-casual)
2. The solving time by WalkSAT could be analyzed by the asymptotic
analysis based on not only the number of variables but also the number of
clauses. The paper give a theoretical analysis of the worst case problem
size in terms of literals (the product of the number of variables and the
number of clauses)
3. The MEDIC compiler can implement all these encodings, so the
authors analyzed the solving time complexity based on this planner
experimentally. So that with these two analysis, they can conclude that the
smallest encodings are the regular and simply spilt explannatory encodings.
Flaw:
I think the worst case analysis could not be appropriate for a
general conclusion of whether the encoding is effiecents or not. The average
case analysis could be stronger. Actually in the experiment, our observation
is based on average complexity too.
Open questions:
1. Automatically generating domain-specific axioms could be one of
the directions, because that is the major difference between hand-coded and
machine-coded encoding.
2. Average case analysis or other analysis of the characteristics of
the solve-time of encodings could be another directions, because that will
give more accurate analysis of decide which encoding is better.
This archive was generated by hypermail 2.1.6 : Wed Nov 05 2003 - 09:33:11 PST