Amol D. Mali and Subbarao Kambhampati
Casting planning problems as propositional satisfiability problems has recently been shown to be an effective way of scaling up plan synthesis. Until now, the benefits of this approach have only been utilized in primitive action-based planning models. Motivated by the conventional wisdom in the planning community about the effectiveness of hierarchical task network (HTN) planning models, in this paper we adapt the ``planning as satisfiability'' approach to HTN planning models. HTN planning models can be thought of as an augmentation of primitive action based planning models with a grammar of legal solutions, provided in the form of non-primitive tasks and task reduction schemas. Accordingly, we argue that any action-based encoding scheme can be generalized to handle HTN planning models. Informally, this generalization involves adding constraints to the encoding to ensure that the solutions produced by solving the encoding will conform to the grammar provided by the HTN planning model. The constraints can be added in either a ``top-down'' or ``bottom-up'' fashion, resulting in two HTN encoding schemes for each primitive action-based encoding scheme. We illustrate this process by providing three different HTN encodings. We discuss the asymptotic sizes of these encodings, as well as the complexity of finding models for them.