*Katrina Ray, Matthew L Ginsberg*

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.

*Subjects:* 1.11 Planning; 9.2 Computational Complexity

*Submitted: *Jun 27, 2008

This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.