Propositional Planning as Optimization

Planning as Satisfiability is a most successful approach to optimal propositional planning. Although optimality is highly desirable, for large problems it comes at a high, often prohibitive, computational cost. This paper extends planning as propositional satisfiability to planning as pseudo-boolean optimization. The approach has been implemented in a planner called PseudoSATPLAN, that follows the classic solve and expand method of the SATPLAN algorithm, but at each step it seeks to maximize the number of goals that can be achieved. The utilization of the achieved goals at subsequent steps opens up the possibility of implementing various strategies. The method essentially splits a planning problem into smaller subproblems, and employs various techniques for solving them fast. Although PseudoSATPLAN cannot guarantee the optimality of the generated plans, it aims at computing solutions of good quality. Experimental results show that PseudoSATPLAN can generate parallel plans of high quality for problems that are beyond the reach of the existing implementations of the planning as satisfiability framework.