The Complexity of Optimal Planning and a More Efficient Method for Finding Solutions

We present a faster method of solving optimal planning problems and show that our solution performs up to an order of magnitude faster than Satplan on a variety of problems from the IPC-5 benchmarks. Satplan makes several calls to a SAT solver, discarding learned information with each call. Our planner uses a single call to a SAT solver, eliminating this problem. We explain our technique by describing a new theoretical framework which allows us to prove that a single call to a SAT solver is sufficient to solve every problem in 2. (This does not imply that NP is equal to 2; only that SAT solvers' capabilities are greater than previously realized.) We also prove that optimal planning is F2 Complete when the plan length is bounded by a polynomial; optimal planning is thus harder than SAT even in the presence of such a bound. Despite the relative complexities, the 2 capability of DPLL and the fact that 2 2 show that a single satisfiability call can solve optimal planning problems in ...

• Type: Conference
• Year: 2008
• Where: AIPS
• Authors: Katrina Ray, Matthew L. Ginsberg
• Keywords: AIPS 2008, Artificial Intelligence, Optimal Planning, Optimal Planning Problems, SAT Solvers