SAS+ planning as satisfiability (Q2887072)

The article describes a new encoding for planning as satisfiability called SASE. The encoding is based on the so-called SAS+ formalism and encodes transitions into a satisfiability scheme for SAT solvers replacing the common STRIPS-based encodings of actions. The resulting encoding is more compact than previous encodings yielding significant performance and memory gains. The authors provide a detailed explanation of the benefits of their encoding and present further reduction techniques. A comprehensive empirical study using AI planning benchmarks and a review of related work complement the theoretical results.