Recently, casting planning as propositional satisfiability has been shown to be a very promising technique for plan synthesis. 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 empirical comparison of plan-space (causal) encodings and state-space encodings. We start by pointing out the connection between the different ways of proving the correctnhess of a plan, and the spectrum of possible SAT encodings. We then characterize the dimensions along which causal proofs, and consequently, plan-space encodings, can vary. We provide two 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 when the primacy of traditional plan-space planners over state-space planners might carry over to their respective SAT encodings.
展开▼
