Planning as satisfiability (SAT-Plan) is one of the best approaches to optimal planning, which has been shown effective on problems in many different domains. However, the potential of the SAT-Plan strategy has not been fully exploited. Following the SAT-Plan paradigm, in this paper we formulate a STRIPS planning problem as a maximum SAT (max-SAT) and develop a general two-phase algorithm for planning. Our method first represents a planning problem as a combinatorial optimization in the form of a SAT compounded with an objective function to be maximized. It then uses a goal-oriented variable selection to force goal-oriented search and a accumulative learnt strategy to avoid to learn a learnt clause multiple times. We integrate our new methods with SATPLAN04. We evaluate and demonstrate the efficacy of our new formulation and algorithm with SATPLAN04 on many well-known real-world benchmark planning problems. Our experimental results show that our algorithm significantly outperforms SATPLAN04 on most of these problems, sometimes with an order of magnitude of improvement in running time.
Jul-1-2006, 06:42:17 GMT