Hierarchical Task Network Planning Using SAT Techniques

  • Subject:Planning SAT
  • Type:Masterarbeit
  • Date:2018
  • Supervisor:

    Humbert Fiorino, Damien Pellier, Tomas Balyo

  • Student:

    Dominik Schreiber

  • Zusatzfeld:

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

  • Links:PDF
  • 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.