Planning as satisfiability is a principal approach to planning with
many eminent advantages. The existing planning as satisfiability
techniques usually use encodings compiled from the STRIPS
formalism. We introduce a novel SAT encoding scheme based on the SAS+
formalism. It exploits the structural information in the SAS+
formalism, resulting in more compact and efficient SAT instances.
The new encoding scheme models a planning problem with a
search space consisting of two hierarchical subspaces. The top
subspace is the space of transition plans, and the lower
subspace is the space of supporting action plans corresponding
to feasible transition plans. We analyze and compare the worst case search space sizes, in the original STRIPS-based search
space and the new hierarchical search space.
We show that, because of the new search space's structure, in which the lower level search can be decomposed based on time steps without backtracking, our encoding scheme typically has a smaller search space.
We would like to convey special thanks to Malte Helmert, for making the parser of Fast-Downward available. We also thank the authors of SatPlan, Minisat and PrecoSAT, along with various anonymous reviewers.