Structure and Problem Hardness: Goal Asymmetry and DPLL Proofs in SAT-Based Planning
Dr Joerg Hoffmann (Max Plank Institute Saarbruecken)
NICTA KRR SEMINARDATE: 2005-11-21
TIME: 14:00:00 - 15:00:00
LOCATION: RSISE Seminar Room, ground floor, building 115, cnr. North and Daley Roads, ANU
CONTACT: JavaScript must be enabled to display this email address.
ABSTRACT:
This is 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(n2) 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(n2). 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.
BIO:
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.
