Planning as satisfiability

We develop a formal model of planning based on satisfiability rather than deduction. The satisfiability approach not only provides a more flexible framework for stating different kinds of constraints on plans, but also more accurately reflects the theory behind modern constraint-based planning systems. Finally, we consider the computational characteristics of the resulting formulas, by solving them with two very different satisfiability testing procedures. 1 Introduction Planning has traditionally been formalized as deduction [Green, 1969; McCarthy and Hayes, 1986; Rosenschein, 1981; Pednault, 1988; Allen, 1991]. Although the details of the different formalisms vary, all use axioms which state that the effects of an action are implied by the occurrence of the action when its preconditions hold. Planning is then formalized as the process of finding a deductive proof of a statement that asserts that the initial conditions together with a sequence of actions imply the goal conditions. Th...