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 FΘ2 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 the presence of a polynomial bound on plan length.