Amol D. Mali and Subbarao Kambhampati, Arizona State University
Recently, casting planning as propositional satisfiability has been shown to be a very promising technique for plan synthesis. It has been claimed that SAT encodings for planning problems can be derived from each of the traditional refinement planning paradigms. Although encodings based both on state-space planning and on plan-space (causal) planning have been proposed, most implementations and trade-off evaluations primarily use state-based encodings. This is surprising given both the prominence of plan-space planners in traditional planning, as well as the recent claim that lifted versions of causal encodings provide the smallest encodings. In this paper we attempt a systematic analytical and empircial comparison of plan-space (causal) encodings and state-space encodings. We start by characterizing a large spectrum of plan-space encodings, and provide several encodings that are much smaller than those previously proposed. We then show that the smallest causal encodings cannot be smaller in size than the smallest state-based encodings. We shall show that the "lifting" transformation does not affect this relation. Finally, we will present some empirical results that demonstrate that the relative encoding sizes are indeed correlated with the hardness of solving them. We end with a discussion on why it is reasonable that the primacy of traditional plan-space planners over state-space planners does not carry over to their respective SAT encodings.