Casting planning problems as propositional satis ability problems has recently been shown to be an effective way of scaling up plan synthesis. Until now, the bene ts of this approach have only been utilized in primitive action-based planning models. Motivated by the conventional wisdom in the planning community about the e ectiveness of hierarchical task network (HTN) planning models, in this paper we adapt the \planning as satis ability" 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. ...