Source-linked AI summary
Towards Numerical TOHTN Planning with SMT-based HTN-SAT Encoding
Gaspard Quenard, Takudzwa Togarepi, Damien Pellier, Humbert Fiorino
TL;DR
HTN planning has limited support for numerical reasoning, motivating numerical TOHTN planning with richer state constraints. The paper extends SAT-based TOHTN encodings with SMT, introduces seven benchmark families, and reports a competitive baseline that solves instances across all families while outperforming other planners on most benchmarks.
Problem
Numerical reasoning is largely underexplored in HTN planning, limiting support for quantity-dependent applications such as logistics, robotics, and scheduling.
Method
The paper extends SAT-based TOHTN encodings with SMT to handle numeric fluents and constraints and introduces seven numerical TOHTN benchmark families.
Results
The SMT-based approach achieves higher coverage and agile scores than other planners on most benchmarks and solves instances across all benchmark families.
Takeaways & Limitations
The encoding provides a competitive baseline and a shared empirical basis for future research on more expressive numerical HTN planning.
Abstract
from arXiv · showhide
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.
Introduction
HTN planning decomposes abstract tasks into executable primitive actions, but numerical reasoning remains under-supported despite its relevance to realistic domains. This paper extends SAT-based TOHTN planning with SMT and introduces numerical benchmarks for evaluation.
- HTN and TOHTN planning: HTN planning recursively decomposes abstract tasks into ordered primitive actions using domain-specific methods.TOHTN methods specify a totally ordered list of primitive and abstract tasks.
- Modeling gap: Numerical and temporal features common in classical planning remain absent from most HTN planners.The passage identifies numerical constraints, resource management, costs, and durations as under-supported features.
- Modeling gap: Numerical reasoning has received little HTN research attention, although quantities matter in logistics, robotics, and scheduling.Only Siadex and Aries are identified as supporting numerical reasoning in HTN planning.
- Paper contributions: The paper extends SAT-based TOHTN planning with SMT to represent numerical variables and constraints while preserving logical encodings.The approach lifts the encoding rather than fundamentally modifying the search procedure.
- Paper contributions: The authors introduce seven numerical TOHTN benchmarks and compare the approach with other numerical HTN planners.The introduction describes the benchmarks as an evaluation basis for the proposed approach.
Numerical TOHTN Planning Problem
Numerical TOHTN planning combines hierarchical task decomposition with propositional and numeric state reasoning. The formalization specifies numeric fluents, constraints, primitive-task effects, decomposition methods, and solution conditions.
- Numeric fluents and constraints: Numeric constraints compare a fluent with an arithmetic expression using <, ≤, =, ≥, or >.Numeric expressions are built from constants and fluents using addition, subtraction, multiplication, and division.
- Tasks and actions: Primitive tasks have propositional and numeric preconditions plus add, delete, and assignment effects.Numeric effects are restricted to assignments of the form f := ξ.
- Execution semantics: A task is executable when its propositional and numeric preconditions hold, and applying it updates both propositions and numeric fluents.The resulting state is obtained by applying the task's effects to the current state.
- Hierarchical decomposition: Methods refine abstract tasks into task networks, while primitive tasks directly affect the world and abstract tasks require decomposition.This establishes the hierarchical structure underlying numerical TOHTN plans.
- Problem definition: A numerical TOHTN problem contains propositions, numeric fluents, abstract and primitive tasks, methods, an initial task, an initial state, and a goal.The goal includes both propositional conditions and numeric constraints.
- Solution definition: A solution is a primitive task network that is executable in the initial state and reaches the goal after execution.The solution definition characterizes the required executable plan outcome.
SAT-based Search in TOHTN
SAT-based TOHTN planning encodes hierarchical decompositions in a cPDT that makes execution order explicit, then extends the encoding with SMT variables and constraints for numeric fluents.
- Hierarchical decomposition: HTN decompositions form an AND/OR tree where OR nodes select one method and AND nodes require all subtasks.A valid plan selects one child at each OR node and all children at each AND node, with primitive leaves forming the plan.
- Compact Path Decomposition Tree: The cPDT is equivalent to the AND/OR tree while making execution time steps explicit for SAT-based encodings.Its leaves preserve task precedence, so scanning them left to right reveals possible plans.
- Boolean encoding: Each cPDT node uses Boolean variables for active tasks and propositions, plus a primitive-task indicator, while a virtual goal node terminates the sequence.The special action ε represents positions where no task is active.
- Boolean encoding: The encoding constrains initial and goal states, leaf actions, preconditions, effects, frame axioms, and hierarchical propagation.Hierarchical constraints assign methods and subtasks to ordered children, while leaf constraints ensure executable actions are selected.
- SMT extension: Numeric TOHTN extends the SAT encoding with one numeric variable per fluent and SMT constraints for initial values, goals, preconditions, effects, frames, and hierarchy.Numeric hierarchical constraints preserve fluent values between a node and its first child, and all Boolean clauses remain unchanged.
- SMT extension: The numerical clauses follow the same incremental scheme as the cPDT expands, generating constraints for new leaves and newly expanded nodes.Initial numeric-state and goal clauses are generated once, while precondition, effect, frame, and hierarchical clauses are added incrementally.
Evaluation
The evaluation compares three numerical HTN planners on seven generated benchmark families under a ten-minute per-instance limit. The SMT-based planner achieves higher coverage and agile scores on most benchmarks, while no planner solves all instances.
- Experimental setup: The evaluation compares SibylSmt, Siadex, and Aries on numerical HTN planning.SibylSmt uses the proposed encoding with Z3 SMT solving and breadth-first cPDT exploration when no solution is found.
- Experimental setup: Experiments use an Intel Core i7-12700H, 32GB RAM, and a 10-minute time limit per instance.The study introduces seven numerical HTN benchmark families, each with an instance generator.
- Benchmark suite: Seven benchmark families provide shared generated instances for evaluating numerical HTN planners.TRANSPORT-FUEL models fuel-limited delivery with refueling, while TRANSVASEMENT models quantity transfer between containers of different capacities.
- Results: The proposed approach achieves higher coverage and agile scores than the other planners on most benchmarks.It solves instances across all benchmark families, whereas the other planners fail on some domains.
- Results: None of the planners saturate all benchmarks, leaving room for stronger numerical HTN planners and benchmarks.Siadex particularly struggles on recursive domains with strong combinatorial branching.
Conclusion
The paper introduces a benchmark suite and an SMT-based extension of HTN-SAT encodings for numerical TOHTN planning. It positions this approach as a baseline for shared evaluation and future work on more expressive hierarchical planning.
- Contributions: The paper introduces a numerical TOHTN benchmark suite and a simple SMT-based extension of HTN-SAT encodings for numeric fluents.The benchmark suite provides shared instances for empirical comparison.
- Implications: The work provides a baseline for future research on more expressive HTN models and stronger planners and benchmarks.The stated scope is numerical hierarchical planning.