Accelerating SAT-Based HTN Plan Verification by Exploiting Data Structures from HTN Planning

Plan verification is the task of deciding 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, which has been proved to be NP-complete when partial order (PO) is involved. We will develop a novel SAT-based approach exploiting the data structures solution order graphs and path decomposition trees which encodes an HTN plan verification problem as a SAT one. We show in our experiments that this new approach outperforms the current state-of-the-art (SOTA) planning-based approach for verifying plans for POHTN problems.