Towards Numerical TOHTN Planning with SMT-based HTN-SAT Encoding

# Towards Numerical TOHTN Planning with SMT-based HTN-SAT Encoding
Source: [https://arxiv.org/html/2609.03938](https://arxiv.org/html/2609.03938)
###### Abstract

While HTN planning has received significant attention in recent years, support for numerical reasoning remains very limited\. In this paper, we investigate numerical Totally\-Ordered HTN \(TOHTN\) planning and show how standard SAT\-based encodings can be naturally extended with SMT to handle numeric fluents\. In addition, we introduce a benchmark suite for numerical TOHTN planning, providing a first common basis for evaluation in this setting\. Experimental results show that this simple encoding already constitutes a competitive baseline\. This work opens the way to more expressive approaches to HTN planning\.

1Univ\. Grenoble Alpes, France

\{takudzwa\.togarepi, gaspard\.quenard, damien\.pellier, humbert\.fiorino\}@univ\-grenoble\-alpes\.fr

## Introduction

Hierarchical Task Network \(HTN\) planning\([Erol, Hendler, and Nau 1994](https://arxiv.org/html/2609.03938#bib.bib7)\)is a planning paradigm that decomposes complex tasks into simpler subtasks using domain\-specific knowledge\. Unlike classical planning, HTN introduces abstract tasks, which cannot be executed directly, and methods, which describe how these tasks can be refined into partially ordered sets of subtasks including both primitive tasks \(i\.e\., executable actions\) and additional abstract tasks that must themselves be recursively refined\. The objective of an HTN planner is to iteratively decompose an initial abstract task into a valid plan \(i\.e\., an executable sequence of primitive tasks\)\. In this paper, we focus our investigation on Totally\-Ordered HTN \(TOHTN\) planning, a highly popular subclass of HTN problems where the decomposition methods specify a totally\-ordered list of primitive actions and abstract tasks to be executed in order to achieve an abstract task\.

While HTN planning is a central topic in automated planning and has been included in recent editions of the International Planning Competition \(IPC\)\([Behnke et al\. 2019](https://arxiv.org/html/2609.03938#bib.bib2);[Taitler et al\. 2024](https://arxiv.org/html/2609.03938#bib.bib17)\), it still suffers from important modeling limitations compared to classical planning formalisms\. In particular, numerical and temporal features \(such as resource management, costs, and durations\) introduced in classical planning with PDDL2\.1\([Fox and Long 2003](https://arxiv.org/html/2609.03938#bib.bib8)\)are absent from most HTN planners\. Although some work has investigated the integration of temporal aspects into HTN planning\([Pellier et al\. 2022](https://arxiv.org/html/2609.03938#bib.bib12)\), the formalization of temporal HTN remains an active research topic, and current proposals have not yet reached broad adoption\. In contrast, numerical reasoning \(e\.g\., through numerical constraints over the preconditions and effects of primitive tasks\) can be naturally incorporated, but has received little attention so far\. These features are essential in many real\-world applications, including logistics, robotics, and scheduling, where reasoning about quantities is required\. To the best of our knowledge, only Siadex\([Castillo et al\. 2006](https://arxiv.org/html/2609.03938#bib.bib5)\)and Aries\([Bit\-Monnot 2023](https://arxiv.org/html/2609.03938#bib.bib4)\)support numerical reasoning in HTN planning\. This limitation restricts the applicability of HTN planning to realistic domains\.

In this paper, we propose to extend SAT\-based TOHTN planning to handle numerical constraints by leveraging Satisfiability Modulo Theories \(SMT\)\. SAT\-based approaches have shown strong performance in recent years in TOHTN planning due to both the efficiency of modern solvers and improved encodings and search strategies\([Schreiber et al\. 2019](https://arxiv.org/html/2609.03938#bib.bib16);[Behnke, Höller, and Biundo 2018](https://arxiv.org/html/2609.03938#bib.bib3);[Schreiber 2021](https://arxiv.org/html/2609.03938#bib.bib15);[Behnke 2021](https://arxiv.org/html/2609.03938#bib.bib1);[Quenard, Pellier, and Fiorino 2024](https://arxiv.org/html/2609.03938#bib.bib13);[Quenard, Pellier, and Fiorino 2025](https://arxiv.org/html/2609.03938#bib.bib14)\), but they are inherently limited to propositional representations\. In contrast to heuristic\-search\-based approaches, which typically require substantial adaptations to handle numerical reasoning, SAT\-based methods can be more naturally extended by lifting the encoding to SMT, without fundamentally modifying the search procedure\. By moving to SMT, we enable reasoning over numerical variables while preserving the benefits of logical encodings\. In this paper, we introduce a new encoding that extends SAT\-based TOHTN planning to handle numerical variables and constraints using an SMT solver\. Additionally we design and provide seven numerical TOHTN benchmarks to evaluate these approaches\. We experimentally show that our SMT\-based encoding enables solving numerical TOHTN problems more efficiently than existing numerical HTN planners\.

This paper is organized as follows: first, we introduce the concept of numerical TOHTN planning\. Next, we describe the basic incremental encoding used by current SAT\-based TOHTN planners to find a solution\. Then, we explain how this encoding can be modified to support numerical constraints\. Finally, we compare this approach with other numerical HTN planners\.

## Numerical TOHTN Planning Problem

We present a formalization of numerical TOHTN planning, building on\([Behnke, Höller, and Biundo 2018](https://arxiv.org/html/2609.03938#bib.bib3);[Behnke 2021](https://arxiv.org/html/2609.03938#bib.bib1);[Quenard, Pellier, and Fiorino 2024](https://arxiv.org/html/2609.03938#bib.bib13)\)and following the treatment of numeric fluents introduced in PDDL2\.1 and discussed for HDDL 2\.1\([Pellier et al\. 2022](https://arxiv.org/html/2609.03938#bib.bib12)\)\.

### Tasks, Actions, Methods, Numeric Fluents, and Task Networks

Tasks are central to HTN planning\. A task is defined by a name and parameters\. Tasks are eitherprimitiveorabstract: primitive tasks directly affect the state of the world, while abstract tasks do not; instead, they must be decomposed into primitive tasks usingmethodsbefore they can be executed\.

We assume a finite setLLof propositions and a finite setFFof numeric fluents\. Anumeric expressionoverFFis built from constants and fluents inFFusing the arithmetic operators\+,−,×,/\+,\-,\\times,/\. Anumeric constraintis an expression of the formf⋈ξf\\bowtie\\xi, wheref∈Ff\\in Fis a numeric fluent,ξ\\xiis a numeric expression, and⋈∈\{<,≤,=,≥,\>\}\\bowtie\\in\\\{<,\\leq,=,\\geq,\>\\\}\.

A primitive taskaais analogous to an action in classical planning and is defined by a tuple\(name​\(a\),precond​\(a\),effect​\(a\)\)\(\\text\{\\it name\}\(a\),\\text\{\\it precond\}\(a\),\\text\{\\it effect\}\(a\)\)\. Its preconditionsprecond​\(a\)=\(precondL​\(a\),precondN​\(a\)\)\\text\{\\it precond\}\(a\)=\(\\text\{\\it precond\}\_\{L\}\(a\),\\text\{\\it precond\}\_\{N\}\(a\)\)consist of a set of propositional preconditionsprecondL​\(a\)\\text\{\\it precond\}\_\{L\}\(a\)and a set of numeric constraintsprecondN​\(a\)\\text\{\\it precond\}\_\{N\}\(a\)\. Its effectseffect​\(a\)=\(effect\+​\(a\),effect−​\(a\),effectN​\(a\)\)\\text\{\\it effect\}\(a\)=\(\\text\{\\it effect\}^\{\+\}\(a\),\\text\{\\it effect\}^\{\-\}\(a\),\\text\{\\it effect\}\_\{N\}\(a\)\)consist of add and delete effects over propositions and a set of numeric effectseffectN​\(a\)\\text\{\\it effect\}\_\{N\}\(a\)\. In this work, we restrict numeric effects to assignment effects of the formf:=ξf:=\\xi, wheref∈Ff\\in Fandξ\\xiis a numeric expression overFF\.

A statessis defined as a pair\(l,v\)\(l,v\)wherel⊆Ll\\subseteq Lis the set of propositions true in the state, andv:F→ℝv:F\\rightarrow\\mathbb\{R\}is a valuation function assigning a real value to each numeric fluent\. A taskaais executable ins=\(l,v\)s=\(l,v\)iffprecondL​\(a\)⊆l\\text\{\\it precond\}\_\{L\}\(a\)\\subseteq landv⊧precondN​\(a\)v\\models\\text\{\\it precond\}\_\{N\}\(a\), i\.e\., all numeric constraints inprecondN​\(a\)\\text\{\\it precond\}\_\{N\}\(a\)are satisfied undervv\. If a taskaais executable in a states=\(l,v\)s=\(l,v\), applying its effects yields a new states′=\(l′,v′\)s^\{\\prime\}=\(l^\{\\prime\},v^\{\\prime\}\), wherel′=\(l∖effect−​\(a\)\)∪effect\+​\(a\)l^\{\\prime\}=\(l\\setminus\\text\{\\it effect\}^\{\-\}\(a\)\)\\cup\\text\{\\it effect\}^\{\+\}\(a\)andv′v^\{\\prime\}is obtained by applyingeffectN​\(a\)\\text\{\\it effect\}\_\{N\}\(a\)tovv\.

A methodm=\(name​\(m\),c,wm\)m=\(\\text\{\\it name\}\(m\),c,w\_\{m\}\)indicates how an abstract taskcccan be refined into a task networkwmw\_\{m\}, called the subtasks ofmm\. For notation purposes, we defineM⁡\(c\)=\{m=\(name​\(m\),c,wm\)∣m∈M\}M\(c\)=\\\{m=\(\\text\{\\it name\}\(m\),c,w\_\{m\}\)\\mid m\\in M\\\}as the set of all methods that can be applied to decompose the abstract taskcc\.

### Planning Problem and Solution

###### Definition 1\(TOHTN Planning Problem\)

A numerical TOHTN planning problemPPis a tuple\(L,F,C,A,M,cI,sI,g\)\(L,F,C,A,M,c\_\{I\},s\_\{I\},g\)where:LLis a finite set of propositions;FFis a finite set of numeric fluents;CCis a finite set of abstract tasks;AAis a finite set of primitive tasks;MMis a finite set of decomposition methods;cI∈Cc\_\{I\}\\in Cis the initial abstract task to be decomposed;sI=\(lI,vI\)∈Ss\_\{I\}=\(l\_\{I\},v\_\{I\}\)\\in Sis the initial state; andg=\(gL,gN\)g=\(g\_\{L\},g\_\{N\}\)is the goal condition, wheregL⊆Lg\_\{L\}\\subseteq Lis a set of propositions andgNg\_\{N\}is a set of numeric constraints\.

###### Definition 2\(TOHTN Planning Problem Solution\)

A solution to a numerical TOHTN planning problemPPis a primitive task networkπ∈A∗\\pi\\in A^\{\*\}such that:

1. 1\.π\\piis obtained by refiningcIc\_\{I\}using methods,
2. 2\.π\\piis executable insIs\_\{I\},
3. 3\.π\\pireaches the goalggafter execution\.

## SAT\-based Search in TOHTN

HTN planning can be naturally represented as an AND/OR tree\([Ghallab, Nau, and Traverso 2004](https://arxiv.org/html/2609.03938#bib.bib9)\), where the root contains the initial abstract task\. This tree represents a finite fragment of the potentially infinite decompositions of the initial abstract task, and is incrementally expanded during search\. OR nodes correspond to abstract tasks with multiple possible decompositions \(methods\), while AND nodes represent methods whose subtasks must all be achieved\. A valid plan is obtained by selecting exactly one child for each OR node and all children for each AND node, such that the leaves form a sequence of primitive actions achieving the goal\. An example of such AND/OR tree is given in the left side of Figure[1](https://arxiv.org/html/2609.03938#Sx3.F1)\. This tree is not fully developed here, since the abstract taskT8T\_\{8\}is undeveloped\.

In SAT\-based HTN planning, the AND/OR tree is encoded into a SAT formula that is satisfiable iff a solution exists within it, with the satisfying assignment yielding the plan\. However, the AND/OR tree alone is insufficient for current encodings\. Indeed, clauses must capture action transitions, ensuring preconditions hold at execution time and effects are applied\. All current SAT\-based HTN planners address this by assigning each task a discrete time step indicating when it may execute; something the AND/OR tree’s structural representation does not provide\.

That is why all current HTN\-SAT planners rely on a structure introduced independently inTreeRexandtotSAT\([Schreiber et al\. 2019](https://arxiv.org/html/2609.03938#bib.bib16);[Behnke, Höller, and Biundo 2018](https://arxiv.org/html/2609.03938#bib.bib3)\), which is equivalent to the AND/OR tree while making execution time steps explicit\. We call this structure a*Compact Path Decomposition Tree*\(cPDT\); its nodes may contain multiple tasks and are organized as follows:

- •The root node contains only the initial abstract taskcIc\_\{I\}\.
- •To expand a nodePP, its children are built as follows: - –For each abstract taskccinPPand each methodmim\_\{i\}decomposingccinto subtasks⟨t1,…,tn⟩\\langle t\_\{1\},\\ldots,t\_\{n\}\\rangle, thekk\-th child ofPPcontains tasktkt\_\{k\}\. - –For each primitive taskaainPP, the first child ofPPcontainsaa\.

The cPDT guarantees that for any taskttat leaflil\_\{i\}, all tasks that must precedettappear at leavesljl\_\{j\}withj<ij<i, and all that must follow appear atlrl\_\{r\}withr\>ir\>i\. Consequently, a left\-to\-right scan of the leaves reveals all possible plans encoded in the cPDT\. The cPDT corresponding to the AND/OR tree of Figure[1](https://arxiv.org/html/2609.03938#Sx3.F1)is shown on its right side\.

![Refer to caption](https://arxiv.org/html/2609.03938v1/test.png)Figure 1:On the left, a simple decomposition schema in the form of an AND/OR tree, whereTiT\_\{i\}denotes abstract taskii,MiM\_\{i\}denotes methodiiandAiA\_\{i\}denotes actionii\. On the right, we represent the corresponding cPDT\. An identical potential solution for both structures is highlighted in blue\.We now present an incremental encoding, capturing the core ideas shared by current HTN\-SAT encodings\([Schreiber et al\. 2019](https://arxiv.org/html/2609.03938#bib.bib16);[Behnke, Höller, and Biundo 2018](https://arxiv.org/html/2609.03938#bib.bib3);[Schreiber 2021](https://arxiv.org/html/2609.03938#bib.bib15)\), that determines whether a solution exists in a given cPDT\. This encoding serves as the basis for the numerical extension introduced next\. For each cPDT nodePP, we use Boolean variablesPtP\_\{t\}indicating that taskttis active atPP, variablesPpP\_\{p\}indicating that propositionp∈Lp\\in Lholds atPP, and an auxiliary variableP𝑝𝑟𝑖𝑚P\_\{\\mathit\{prim\}\}indicating that a primitive task is active inPP\. Whenttis a primitive task, we write it asaa; whenttis an abstract task, we write it ascc\. For any leafPP, we denote byP\+=successor​\(P\)P^\{\+\}=\\text\{\\it successor\}\(P\)the leaf executed immediately afterPPin the left\-to\-right order induced by the decomposition hierarchy\. To handle the goal state, we introduce a special*virtual*nodeGG, representing the goal\. Thus, for any nodePPthat has no successor, we defineP\+=GP^\{\+\}=G\. As shown in Figure[1](https://arxiv.org/html/2609.03938#Sx3.F1), there may exist solutions in which no task is active at a given position\. To handle this case, we introduce a special actionε\\varepsilonsuch thatprecond​\(ε\)=effect​\(ε\)=∅\\text\{\\it precond\}\(\\varepsilon\)=\\text\{\\it effect\}\(\\varepsilon\)=\\emptyset\. This action is treated like a normal action in the encoding, but it is ignored in the final plan\. We writePεP\_\{\\varepsilon\}to denote that no task is active at nodePP\.

#### Initial task, initial state, and goal\.

At the root nodeRR, the initial task and initial state must hold, and the goal must hold atGG:

RcI\\displaystyle R\_\{c\_\{I\}\}∀p∈sI:Rp∀p∈L∖sI:¬Rp\\displaystyle\\forall p\\in s\_\{I\}:\\ R\_\{p\}\\qquad\\forall p\\in L\\setminus s\_\{I\}:\\ \\neg R\_\{p\}∀p∈g:Gp\\displaystyle\\forall p\\in g:\\ G\_\{p\}

#### Leaf constraints\.

For every leaf nodePP, exactly one task is active atPP:

⋁t∈T​a​s​k​s​\(P\)Pt\\displaystyle\\bigvee\_\{t\\in Tasks\(P\)\}P\_\{t\}⋀t,t′∈T​a​s​k​s​\(P\)t≠t′¬\(Pt∧Pt′\)\\displaystyle\\bigwedge\_\{\\begin\{subarray\}\{c\}t,t^\{\\prime\}\\in Tasks\(P\)\\\\ t\\neq t^\{\\prime\}\\end\{subarray\}\}\\neg\(P\_\{t\}\\wedge P\_\{t^\{\\prime\}\}\)If a primitive taskaais active inPP, then its preconditions must hold atPPand its effects atP\+P^\{\+\}:

∀a∈T​a​s​k​s​\(P\)∩A:\\displaystyle\\forall a\\in Tasks\(P\)\\cap A:\\quadPa⇒⋀p∈precond​\(a\)Pp\\displaystyle P\_\{a\}\\Rightarrow\\bigwedge\_\{p\\in\\text\{\\it precond\}\(a\)\}P\_\{p\}∀a∈T​a​s​k​s​\(P\)∩A:\\displaystyle\\forall a\\in Tasks\(P\)\\cap A:\\quadPa⇒⋀p∈effect\+​\(a\)Pp\+\\displaystyle P\_\{a\}\\Rightarrow\\bigwedge\_\{p\\in\\text\{\\it effect\}^\{\+\}\(a\)\}P^\{\+\}\_\{p\}∀a∈T​a​s​k​s​\(P\)∩A:\\displaystyle\\forall a\\in Tasks\(P\)\\cap A:\\quadPa⇒⋀p∈effect−​\(a\)¬Pp\+\\displaystyle P\_\{a\}\\Rightarrow\\bigwedge\_\{p\\in\\text\{\\it effect\}^\{\-\}\(a\)\}\\neg P^\{\+\}\_\{p\}Frame axioms ensure that if a fact changes value between a node and its successor, it must be explained by a specific action that can change this fact or an abstract task:

∀p∈L:¬Pp∧Pp\+⇒\(¬P𝑝𝑟𝑖𝑚∨⋁a∈T​a​s​k​s​\(P\)∩Ap∈effect\+​\(a\)Pa\)\\displaystyle\\forall p\\in L:\\quad\\neg P\_\{p\}\\wedge P^\{\+\}\_\{p\}\\Rightarrow\\left\(\\neg P\_\{\\mathit\{prim\}\}\\vee\\bigvee\_\{\\begin\{subarray\}\{c\}a\\in Tasks\(P\)\\cap A\\\\ p\\in\\text\{\\it effect\}^\{\+\}\(a\)\\end\{subarray\}\}P\_\{a\}\\right\)∀p∈L:Pp∧¬Pp\+⇒\(¬P𝑝𝑟𝑖𝑚∨⋁a∈T​a​s​k​s​\(P\)∩Ap∈effect−​\(a\)Pa\)\\displaystyle\\forall p\\in L:\\quad P\_\{p\}\\wedge\\neg P^\{\+\}\_\{p\}\\Rightarrow\\left\(\\neg P\_\{\\mathit\{prim\}\}\\vee\\bigvee\_\{\\begin\{subarray\}\{c\}a\\in Tasks\(P\)\\cap A\\\\ p\\in\\text\{\\it effect\}^\{\-\}\(a\)\\end\{subarray\}\}P\_\{a\}\\right\)Finally, if an action is chosen on this position, this node is primitive:

∀a∈T​a​s​k​s​\(P\)∩A:Pa⇒P𝑝𝑟𝑖𝑚\\displaystyle\\forall a\\in Tasks\(P\)\\cap A:\\quad P\_\{a\}\\Rightarrow P\_\{\\mathit\{prim\}\}∀c∈T​a​s​k​s​\(P\)∩C:Pc⇒¬P𝑝𝑟𝑖𝑚\\displaystyle\\forall c\\in Tasks\(P\)\\cap C:\\quad P\_\{c\}\\Rightarrow\\neg P\_\{\\mathit\{prim\}\}

#### Hierarchical constraints\.

LetPPbe an expanded node with children⟨P1,…,Pk⟩\\langle P^\{1\},\\dots,P^\{k\}\\rangle\. Facts hold inPPiff they hold in its first child:

∀p∈L:Pp⇔Pp1\\forall p\\in L:\\quad P\_\{p\}\\Leftrightarrow P^\{1\}\_\{p\}If an abstract taskccis selected atPP, then exactly one applicable method must be chosen to decompose this task, its subtasks must be assigned to the children in order, and all remaining children must receiveε\\varepsilon:

∀c∈T​a​s​k​s​\(P\)∩C:\\displaystyle\\forall c\\in Tasks\(P\)\\cap C:Pc⇒⋁m∈M⁡\(c\)\(CLOSE\\displaystyle P\_\{c\}\\Rightarrow\\bigvee\_\{m\\in M\(c\)\}\\Bigg\(⋀i=1\|s​u​b​t​a​s​k​s​\(m\)\|Ps​u​b​t​a​s​k​s​\(m\)​\[i\]i\\displaystyle\\bigwedge\_\{i=1\}^\{\|subtasks\(m\)\|\}P^\{i\}\_\{subtasks\(m\)\[i\]\}∧⋀i=\|s​u​b​t​a​s​k​s​\(m\)\|\+1kPiε\)\\displaystyle\\wedge\\bigwedge\_\{i=\|subtasks\(m\)\|\+1\}^\{k\}P^\{i\}\_\{\\varepsilon\}\\Bigg\)If a primitive taskaais selected atPP\(includingε\\varepsilon\), it is propagated to the first child and remaining children receiveε\\varepsilon:

∀a∈T​a​s​k​s​\(P\)∩A:Pa⇒\(Pa1∧⋀i=2kPεi\)\\forall a\\in Tasks\(P\)\\cap A:\\quad P\_\{a\}\\Rightarrow\\left\(P^\{1\}\_\{a\}\\wedge\\bigwedge\_\{i=2\}^\{k\}P^\{i\}\_\{\\varepsilon\}\\right\)

#### Primitivity of the leaves\.

Finally, in order to obtain a solution, all leaves must contain primitive actions\.

⋀P∈l​e​a​v​e​s​\(c​P​D​T\)P𝑝𝑟𝑖𝑚\\bigwedge\_\{P\\in leaves\(cPDT\)\}P\_\{\\mathit\{prim\}\}
The clauses ensuring the initial task, initial state, and goal are generated only during the first encoding of the cPDT, whereas the clause ensuring the primitivity of the leaves is provided only asassumptions\(temporary hypotheses active during a single SAT call\)\. All other clauses remain valid after extending the cPDT\. When the cPDT is expanded, hierarchical constraints are generated for the newly expanded nodes, and leaf constraints are generated for the new leaf positions \(i\.e\., the children of the expanded nodes\)\.

### SMT Extension for Numerical TOHTN

To extend the previous SAT encoding to numerical TOHTN, we introduce for each nodePPand each numeric fluentf∈Ff\\in Fa numeric variablePfP\_\{f\}denoting the value offfatPP\. For any numeric expression or constraintξ\\xi, we write⟦ξ⟧P\\llbracket\\xi\\rrbracket\_\{P\}for the arithmetic expression or constraint obtained by replacing each fluentffoccurring inξ\\xiby the numerical variablePfP\_\{f\}\.

#### Initial numeric state and numeric goal\.

The initial valuation of the numeric fluents is encoded at the root node:

∀f∈F:Rf=vI​\(f\)\\forall f\\in F:\\quad R\_\{f\}=v\_\{I\}\(f\)Each numeric goal constraint must hold at the goal nodeGG:

∀ξ∈gN:⟦ξ⟧G\\forall\\xi\\in g\_\{N\}:\\quad\\llbracket\\xi\\rrbracket\_\{G\}

#### Numeric leaf constraints\.

If a primitive taskaais active at leaf nodePP, then its numeric preconditions must hold atPP:

∀a∈T​a​s​k​s​\(P\)∩A,∀ξ∈precondN​\(a\):Pa⇒⟦ξ⟧P\\forall a\\in Tasks\(P\)\\cap A,\\ \\forall\\xi\\in\\text\{\\it precond\}\_\{N\}\(a\):\\quad P\_\{a\}\\Rightarrow\\llbracket\\xi\\rrbracket\_\{P\}Ifaais active atPP, then each numeric effect of the formf=ξf=\\xidetermines the value offfatP\+P^\{\+\}:

∀a∈T​a​s​k​s​\(P\)∩A,∀\(f=ξ\)∈effectN​\(a\):\\forall a\\in Tasks\(P\)\\cap A,\\ \\forall\(f=\\xi\)\\in\\text\{\\it effect\}\_\{N\}\(a\):Pa⇒\(Pf\+=⟦ξ⟧P\)P\_\{a\}\\Rightarrow\(P^\{\+\}\_\{f\}=\\llbracket\\xi\\rrbracket\_\{P\}\)

#### Numeric frame axioms\.

For each leaf nodePPand each fluentf∈Ff\\in F, the value offfcan change betweenPPandP\+P^\{\+\}only if the selected task is abstract or a primitive action that can modifyff:

\(Pf≠Pf\+\)⇒\(¬P𝑝𝑟𝑖𝑚∨⋁a∈T​a​s​k​s​\(P\)∩Af∈effectN​\(a\)Pa\)\(P\_\{f\}\\neq P^\{\+\}\_\{f\}\)\\Rightarrow\\left\(\\neg P\_\{\\mathit\{prim\}\}\\;\\vee\\;\\bigvee\_\{\\begin\{subarray\}\{c\}a\\in Tasks\(P\)\\cap A\\\\ f\\in\\text\{\\it effect\}\_\{N\}\(a\)\\end\{subarray\}\}P\_\{a\}\\right\)

#### Numeric hierarchical constraints\.

As in the propositional case, numeric fluent values are constrained to be equal between a nodePPand its first childP1P^\{1\}:

∀f∈F:Pf=Pf1\\forall f\\in F:\\quad P\_\{f\}=P^\{1\}\_\{f\}
All Boolean clauses from the SAT encoding remain unchanged\. The numeric clauses described above are generated following the same incremental scheme: the initial numeric state and numeric goal clauses are generated once at the first encoding, while the numeric precondition, effect, and frame axiom clauses are generated for each new leaf node as the cPDT is extended and numerical hierarchical constraints are generated for the newly expanded nodes\.

## Evaluation

We compare our approach with the two numerical HTN planners available to us\. The evaluation involves three planners: SibylSmt, our planner using the encoding described above with the Z3 SMT solver\([De Moura and Bjørner 2008](https://arxiv.org/html/2609.03938#bib.bib6)\)and a BFS exploration \(i\.e\., expanding all nodes of the cPDT if no solution is found\)111https://github\.com/gaspard\-quenard/sibylsat; Siadex\([Castillo et al\. 2006](https://arxiv.org/html/2609.03938#bib.bib5)\), an HTN planner derived from SHOP\([Nau et al\. 1999](https://arxiv.org/html/2609.03938#bib.bib10);[Nau et al\. 2003](https://arxiv.org/html/2609.03938#bib.bib11)\)with constraint\-based reasoning; and Aries\([Bit\-Monnot 2023](https://arxiv.org/html/2609.03938#bib.bib4)\), a hybrid CP/SAT planner\. Experiments were run on an Intel Core i7\-12700H with 32GB RAM, with a 10\-minute time limit per instance\.

To the best of our knowledge, no standard benchmark suite exists for numerical HTN planning\. We therefore introduce seven numerical HTN benchmark families, each with an instance generator222https://github\.com/gaspard\-quenard/HTN\-Numerical\-Benchmarks\. For example,Transport\-Fuelmodels fuel\-limited delivery with possible refueling, whileTransvasementcaptures water\-jug\-style transfers \(reaching a target quantity in a specific container by pouring between containers of different capacities\)\.

Table 1:Performance of each planner on the numerical benchmark suite\. Each cell reports the agile score per domain\. Total coverage and agile score are shown in the last two rows\. Agile score is computed asA​g​i​l​e​\_​s​c​o​r​e=min⁡\(1,1−log⁡\(t\)log⁡\(T\)\)Agile\\\_score=\\min\\left\(1,1\-\\frac\{\\log\(t\)\}\{\\log\(T\)\}\\right\)if a plan is found, and00otherwise, whereTTis the time limit andttthe solving time \(in seconds\)\.Results are shown in Table[1](https://arxiv.org/html/2609.03938#Sx4.T1)\. Our approach achieves higher coverage and agile scores \(reflecting how quickly a planner finds a solution\) than the other planners on most benchmarks, suggesting that it is a promising direction for numerical HTN problems\. In particular, it appears more robust, being able to solve multiple instances across all benchmark families, while the other planners fail on some domains\. Siadex notably struggles on recursive domains with strong combinatorial branching, where the choice of decomposition methods is not easily guided by the current state\. Finally, none of the planners saturate all the benchmarks, leaving significant room for improvement and the development of more powerful approaches\.

## Conclusion

Numerical reasoning is essential in many planning applications, yet remains largely underexplored in HTN planning\. We introduced a benchmark suite for numerical TOHTN and a simple SMT\-based extension of HTN\-SAT encodings to handle numeric fluents\. This provides a baseline for future work and enables empirical comparison on shared instances\. We hope this work encourages further research on expressive HTN models and stronger planners and benchmarks for numerical hierarchical planning\.

## References

- Behnke \(2021\)Behnke, G\. 2021\.Block compression and invariant pruning for SAT\-based totally\-ordered HTN planning\.In*Proceedings of the International Conference on Automated Planning and Scheduling*, volume 31, 25–35\.
- Behnke et al\. \(2019\)Behnke, G\.; Höller, D\.; Bercher, P\.; Biundo, S\.; Pellier, D\.; Fiorino, H\.; and Alford, R\. 2019\.Hierarchical planning in the IPC\.In*Workshop on HTN Planning \(ICAPS\)*\.
- Behnke, Höller, and Biundo \(2018\)Behnke, G\.; Höller, D\.; and Biundo, S\. 2018\.totSAT\-Totally\-ordered hierarchical planning through SAT\.In*Proceedings of the AAAI Conference on Artificial Intelligence*, volume 32\.
- Bit\-Monnot \(2023\)Bit\-Monnot, A\. 2023\.Experimenting with Lifted Plan\-Space Planning as Scheduling: Aries in the 2023 IPC\.In*2023 International Planning Competition at the 33rd International Conference on Automated Planning and Scheduling*\.
- Castillo et al\. \(2006\)Castillo, L\. A\.; Fernández\-Olivares, J\.; Garcia\-Perez, O\.; and Palao, F\. 2006\.Efficiently Handling Temporal Knowledge in an HTN Planner\.In*ICAPS*, 63–72\.
- De Moura and Bjørner \(2008\)De Moura, L\.; and Bjørner, N\. 2008\.Z3: An efficient SMT solver\.In*International conference on Tools and Algorithms for the Construction and Analysis of Systems*, 337–340\. Springer\.
- Erol, Hendler, and Nau \(1994\)Erol, K\.; Hendler, J\. A\.; and Nau, D\. S\. 1994\.UMCP: A Sound and Complete Procedure for Hierarchical Task\-network Planning\.In*Aips*, volume 94, 249–254\.
- Fox and Long \(2003\)Fox, M\.; and Long, D\. 2003\.PDDL2\. 1: An extension to PDDL for expressing temporal planning domains\.*Journal of artificial intelligence research*, 20: 61–124\.
- Ghallab, Nau, and Traverso \(2004\)Ghallab, M\.; Nau, D\.; and Traverso, P\. 2004\.*Automated Planning: theory and practice*\.Elsevier\.
- Nau et al\. \(1999\)Nau, D\.; Cao, Y\.; Lotem, A\.; and Munoz\-Avila, H\. 1999\.SHOP: Simple hierarchical ordered planner\.In*Proceedings of the 16th international joint conference on Artificial intelligence\-Volume 2*, 968–973\.
- Nau et al\. \(2003\)Nau, D\. S\.; Au, T\.\-C\.; Ilghami, O\.; Kuter, U\.; Murdock, J\. W\.; Wu, D\.; and Yaman, F\. 2003\.SHOP2: An HTN planning system\.*Journal of artificial intelligence research*, 20: 379–404\.
- Pellier et al\. \(2022\)Pellier, D\.; Fiorino, H\.; Grand, M\.; Albore, A\.; and Bailon\-Ruiz, R\. 2022\.HDDL 2\.1: Towards Defining an HTN Formalism with Time\.*arXiv preprint arXiv:2206\.01822*\.
- Quenard, Pellier, and Fiorino \(2024\)Quenard, G\.; Pellier, D\.; and Fiorino, H\. 2024\.SibylSat: Using SAT as an Oracle to Perform a Greedy Search on TOHTN Planning\.In*27th European Conference on Artificial Intelligence*, volume 392, 4157–4164\.
- Quenard, Pellier, and Fiorino \(2025\)Quenard, G\.; Pellier, D\.; and Fiorino, H\. 2025\.SibylSatOpt: a MaxSAT\-based Greedy Optimal Search for TOHTN Planning\.In*Proceedings of the International Conference on Automated Planning and Scheduling*, volume 35, 236–244\.
- Schreiber \(2021\)Schreiber, D\. 2021\.Lilotane: A lifted SAT\-based approach to hierarchical planning\.*Journal of artificial intelligence research*, 70: 1117–1181\.
- Schreiber et al\. \(2019\)Schreiber, D\.; Pellier, D\.; Fiorino, H\.; et al\. 2019\.Tree\-REX: SAT\-based tree exploration for efficient and high\-quality HTN planning\.In*Proceedings of the International Conference on Automated Planning and Scheduling*, volume 29, 382–390\.
- Taitler et al\. \(2024\)Taitler, A\.; Alford, R\.; Espasa, J\.; Behnke, G\.; Fišer, D\.; Gimelfarb, M\.; Pommerening, F\.; Sanner, S\.; Scala, E\.; Schreiber, D\.; et al\. 2024\.The 2023 international planning competition\.