Block Compression and Invariant Pruning for SAT-based Totally-Ordered HTN Planning

Translations into propositional logic are currently one of the most efficient techniques for solving Totally-Ordered HTN planning problems. The two current encodings both iterate over the maximum allowed depth of decomposition. Given this depth, they compute a tree that represents all possible decompositions up to this depth. Based on this tree, a formula in propositional logic is created. We show that much of the computed tree is actually useless as it cannot possibly belong to a solution. We provide a technique for removing (parts of) these useless structures using state invariants. We further show that is often not necessary to encode all leafs of this tree as separate timesteps, as the prior encodings did. Instead, we can compress the leafs into blocks and encode all leafs of a block at one timestep. We show that these changes provide an improvement over the state-of-the-art in HTN planning.