Structure and Problem Hardness: Goal Asymmetry and DPLL Proofs in SAT-Based Planning

In AI Planning, as well as Verification, a successful method is to compile the application 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 form of problem structure concerned with the symmetrical or asymmetrical nature of the cost of achieving the individual planning goals. We quantify this sort of structure with a simple numeric parameter called AsymRatio, ranging between

• Type: Conference
• Year: 2006
• Where: AIPS
• Authors: Jörg Hoffmann, Carla P. Gomes, Bart Selman
• Keywords: AIPS 2006, Artificial Intelligence, Boolean Satisfiability, Simple Numeric Parameter, State-of-the-art Dpll-based Procedures