Humbert Fiorino, Damien Pellier, Tomas Balyo

Dominik Schreiber

Source code: https://gitlab.com/domschrei/htn-sat

Automated planning is useful for a wide range of general decision-making processes
in the area of Artificial Intelligence. The solving approach of encoding a planning
problem into propositional logic and finding a solution with a SAT solver is a well-
established method. Likewise, a planning model called Hierarchical Task Networks
(HTN) which enhances planning problems with expert knowledge can help to find
structured plans more easily and efficiently. This work focuses on combining these
techniques by using SAT solving techniques to resolve HTN planning problems.
Initially, a previous approach to encode HTN problems in SAT is analyzed, and
various shortcomings are identified from today’s perspective. Then, three original
encodings are proposed: Grammar-Constrained Tasks (GCT) which is inspired by one
of the previous encodings and is the first to feature modern HTN domains and re-
cursive task relationships; Stack Machine Simulation (SMS) which is designed for in-
cremental SAT solving and works reliably on all special cases; and Tree-like Reduction
Exploration (T-REX) which leads to a particularly efficient solving process due to its
short amount of needed iterations and various introduced optimizations. All encod-
ings are implemented to exploit existing HTN grounding routines, and the T-REX
approach features a novel abstract formula notation and an efficient Interpreter ap-
plication tailored to the encoding. In addition, an Anytime plan length optimization
within T-REX is proposed.
Experiments show that SMS dominates GCT and that T-REX dominates SMS.
The proposed T-REX planning framework outperforms a state-of-the-art classical
SAT planner on various domains. Regarding run times, T-REX cannot compete with
state-of-the-art HTN planners yet, but is still an appealing planning approach due
to its robustness, its plan length optimization, and its proving abilities.
By the design, implementation and evaluation of T-REX, the work at hand
demonstrates that HTN planning via SAT solving is a viable option and worthy of
the attention of future research.