Exploiting Solution Order Graphs and Path Decomposition Trees for More Efficient HTN Plan Verification via SAT Solving

The task of plan verification is to decide whether a given plan is a solution to a planning problem. In this paper, we study the plan verification problem in the context of Hierarchical Task Network (HTN) planning. Concretely, we will develop a new SAT-based approach via exploiting the data structures solution order graphs and path decomposition trees employed by the state-of-the-art SAT-based HTN planner which transforms an HTN plan verification problem into a SAT formula. Additionally, for the purpose of completeness, we will also reimplement the old SAT-based plan verifier within an outdated planning system called PANDA₃ and integrate it into the new version called PANDA_π.