Abstract
Solving planning problems via translation to satisfiability (SAT) is one of the most successful approaches to automated planning. We propose a new encoding scheme which encodes a planning problem represented in the SAS+ formalism using a relaxed Exist-Step semantics of parallel actions.
The encoding by design allows more actions to be put inside one parallel step than other encodings and thus a planning problem can be solved with fewer SAT solver calls. The experiments confirm this property.
In several non-trivial cases the entire plans fit inside only one parallel step. In our experiments we also compared our encoding with other state-of-the-art encodings such as SASE and Rintanen’s Exist-Step encoding using standard IPC benchmark domains.
Our encoding can outperform both these encodings in the number of solved problems within a given limit as well as in the number of SAT solver calls needed to find a plan.