This paper introduces SibylSatOpt, a novel approach to finding optimal plans for Totally-Ordered HTN (TOHTN) problems by leveraging greedy search techniques with MaxSAT. Unlike previous SAT-based HTN planners that employed a blind breadth-first search strategy, SibylSatOpt is guided by an admissible heuristic. This heuristic combines a relaxed MaxSAT encoding of the problem with the Task Decomposition Graph (TDG) heuristic. As we demonstrate, the admissibility of the heuristic guarantees that the found solution is optimal. Experimental results on IPC benchmarks show that SibylSatOpt significantly outperforms existing optimal TOHTN planners in both runtime and problem coverage.

This paper presents SibylSat, a novel SAT-based method designed to efficiently solve totally-ordered HTN problems (TOHTN). In contrast to prevailing SAT-based HTN planners that employ a breadth-first search strategy, SibylSat adopts a greedy search approach, enabling it to identify promising decompositions for expansion. The selection process is facilitated by a heuristic derived from solving a relaxed problem, which is also expressed as a SAT problem. Our experimental evaluations demonstrate that SibylSat outperforms existing SAT-based TOHTN approaches in terms of both runtime and plan quality on most of the IPC benchmarks, while also solving a larger number of problems.