|
TITLE: Structure and Problem Hardness: Goal Asymmetry and DPLL Proofs in SAT-Based Planning
PRESENTER: Joerg Hoffmann, http://www.mpi-sb.mpg.de/~hoffmann/, hoffmann@mpi-sb.mpg.de
AFFILIATION:Max Planck Institute for Computer Science, Saarbruecken, Germany, http://www.mpi-sb.mpg.de
DATE: Friday 25th November 2005
TIME: 12:00:00
PLACE: CSE Seminar Room, Level 1, K17
ABSTRACT:
This is the joint work with Carla Gomes and Bart Selman (Cornell Unv.)
In AI Planning, as well as Verification, a successful method is to
compile the application task into boolean satisfiability (SAT), and
solve it with state-of-the-art DPLL-based procedures. There is a
lack of formal understanding why this works so well. Focussing on
the Planning context, we identify a structural parameter, called
AsymRatio, that measures a kind of asymmetry in the cost of
achieving the individual planning goals. AsymRatio ranges between
0 and 1, and we show empirically that it correlates strongly
with SAT solver performance in a broad range of Planning benchmarks,
including the domains used in the 3rd International Planning
Competition. We then examine carefully crafted synthetic
planning domains that allow to control the value of AsymRatio,
and that are clean enough to allow a rigorous analysis of the
combinatorial search space. The domains are parameterized by size
n, and by a structure parameter k, so that AsymRatio is
asymptotic to k/n. The CNFs we examine are unsatisfiable, encoding
one planning step less than the length of the optimal plan; they
have O(n^2) variables. We prove upper and lower bounds on the
size of the best possible DPLL refutations, under different setting
of k, as a function of n. We also identify the best possible
sets of branching variables. With minimum AsymRatio, we
prove exponential lower bounds, and identify minimal branching sets
of size O(n^2). With maximum AsymRatio, we identify
logarithmic DPLL refutations (and branching sets) of size
O(log n), showing a doubly exponential gap between the two
structural extreme cases. This provides a concrete insight into the
practical efficiency of modern SAT solvers.
BIOGRAPHY OF SPEAKER:
Joerg Hoffmann received a Diploma and PhD in Computer Science from
Freiburg University, Germany, in 1999 and 2002 respectively. Since 2004 he
is a researcher at the Max Planck Institute for Computer Science,
Saarbruecken, Germany. He has been involved in AI Planning research since
1997, and is currently investigating topics from Planning, Satisfiability,
and Model Checking. He is the receiver of several awards, including the
2002 ECCAI Dissertation Award, the ICAPS 2004 Best Paper Award, and the
JAIR 2005 Best Paper Price.
Host:
Alfredo Gabaldon
Seminar Convenor:
Van Hai Ho
|
