Optimal STRIPS planning by maximum satisfiability and accumulative learning

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.