Towards Numerical TOHTN Planning with SMT-based HTN-SAT Encoding
Gaspard Quenard, Takudzwa Togarepi, Damien Pellier, Humbert Fiorino
cs.AI
Quick verdict
将基于 SAT 的 TOHTN 规划通过 SMT (Z3) 扩展至数值领域，并增加了一个 7 领域的基准测试；91/140 对比 48/42 的覆盖率支持了该基准声明的有效性，但相关分析略显薄弱。
Summary
本文旨在解决 HTN 规划中数值推理几乎缺失的问题，据作者称，此前仅有 Siadex (2006) 和 Aries (2023) 能够处理数值流（numeric fluents）。基于 TreeRex 和 totSAT 等 SAT-based TOHTN 规划器所使用的紧凑路径分解树（cPDT），作者为每个节点和流引入了一个数值变量，并在现有的增量 SAT 编码之上叠加了四个数值约束子句族：初始状态和目标、叶子处的数值前提条件和赋值效果、数值框架公理以及节点到首个子节点的相等关系；布尔子句保持不变。生成的规划器 SibylSmt 将 Z3 SMT 求解器与 cPDT 的广度优先扩展相结合。他们还发布了七个数值 TOHTN 基准测试族及其实例生成器（共 140 个实例），这是首个共同的评估基础。在 10 分钟限制内，SibylSmt 求解了 91/140 个实例，而 Aries 为 48 个，Siadex 为 42 个，并取得了最好的总敏捷得分（66.82，而前两者分别为 31.72 和 40.54）；它是唯一在每个族中都能求解实例的规划器，尽管 Siadex 在 Alchemy 和 Minecraft 上速度更快。局限性：缺乏可靠性/完备性论证，未分析理论选择或 SMT 开销，对实例大小的表征不足，且缺乏针对各领域的覆盖率报告。
Review complete
Assessment at a glance
4
risk flags identified
● high 0
● medium 2
● low 2
4 strengths · 4 weaknesses · 5 author questions
AI text signal = Binoculars zero-shot detector score over 20 sampled passages (Fast-DetectGPT co-reported) — absence does not prove human authorship, and a flag does not imply misconduct.
Levels reflect verification complexity — not a quality score. Evolve never rates your paper.
Key claims under review
- Standard incremental SAT-based TOHTN encodings can be naturally extended to SMT by adding one numeric variable per node and fluent, with numeric effects restricted to assignments.
- On the new suite, SibylSmt (Z3 + BFS cPDT expansion) achieves higher coverage (91/140 vs 48 for Aries and 42 for Siadex) and the best total agile score (66.82 vs 31.72 and 40.54).
- The seven-family benchmark suite with public instance generators is the first common evaluation basis for numerical TOHTN planning.
- This simple encoding already constitutes a competitive baseline that opens the way to more expressive HTN planning approaches.
Strengths
Real, well-motivated gap
The paper correctly identifies that numeric fluents (PDDL2.1-era features) are absent from essentially all HTN planners; the Introduction names only Siadex (ICAPS 2006) and Aries (IPC 2023) as numerically capable, making the target area genuinely underexplored.
Clean, conservative encoding design
The SMT extension (Numeric leaf constraints, frame axioms, hierarchical equalities sections) layers four clause families onto the established cPDT/incremental-SAT scheme without touching Boolean clauses; restricting numeric effects to assignments (f := ξ) keeps expressions within decidable arithmetic.
First common benchmark suite with public generators
Transparent result reporting
Weaknesses
No formal guarantees for the core artifact
Thin evaluation reporting
No ablation or propositional reference point
Narrow baseline set
Full Review Report
$1.99 · one-timeUnlock the complete preliminary analysis Evolve produced for this paper.
Report preview
Scope & Claims
The paper targets a real gap: while classical planning gained numeric fluents with PDDL2.1, HTN planning has stayed almost entirely propositional — the Introduction names only Siadex (Castillo et al., ICAPS 2006) and Aries (Bit-Monnot, IPC 2023) as numerically capable HTN planners. Two contributions are claimed: (1) an SMT lifting of the incremental SAT encodings used by TreeRex/totSAT-lineage TOHTN planners; (2) the first shared benchmark suite for numerical TOHTN planning (seven families × 20 instances = 140, with public generators). Headline claims: the extension is natural; SibylSmt (Z3 plus BFS over cPDT expansions) outperforms Siadex and Aries; the encoding is a competitive baseline. Scope is deliberately modest: totally-ordered HTN only, numeric effects restricted to assignments (f := ξ), no optimality, no temporal reasoning.
The remaining sections cover Methodology Assessment, Statistical Evidence, Results & Reproducibility, Limitations & Risks, and Verdict & Recommendations.
- All 4 strengths & 4 weaknesses, analyzed in detail
- 4 risk flags with severity, section & reviewer questions
- Methods & statistical evidence assessment
- 5 questions a peer reviewer would ask
- Full six-dimension evaluation report & recommendations
One-time purchase · this paper only
One-time purchase, this paper only. AI-generated preliminary analysis — not peer review.
Frequently asked questions
What problem does this paper solve?
It addresses the lack of numerical reasoning in HTN (Hierarchical Task Network) planning. Classical planning gained numeric fluents, resources, and arithmetic preconditions with PDDL2.1, but most HTN planners remain purely propositional; the authors state that only Siadex (2006) and Aries (2023) support numerics in HTN planning.
How well does the proposed SibylSmt planner perform?
On the authors' new suite of seven numerical TOHTN benchmark families (140 instances, 10-minute limit per instance), SibylSmt solves 91 instances versus 48 for Aries and 42 for Siadex, and posts the best total agile score (66.82 against 31.72 and 40.54). It is the only planner solving instances in every family, though Siadex is faster on the Alchemy and Minecraft families.
Are the code and benchmarks publicly available?
Yes. The paper links a GitHub repository for the planner (github.com/gaspard-quenard/sibylsat) and a second repository with instance generators for the seven benchmark families (github.com/gaspard-quenard/HTN-Numerical-Benchmarks).
What is the agile score used in the evaluation?
A speed measure: for a solved instance it equals min(1, 1 − log(t)/log(T)), where t is the solving time and T is the 600-second limit (so it is 1 for instant solves, 0 at the timeout); unsolved instances score 0. Per-domain values in Table 1 sum this over the 20 instances of each family, so the theoretical maximum is 140 across the suite.
About this review
This is an AI-generated preliminary review by Evolve.Pub, produced from the openly available text of the paper. It is not peer review and does not represent the authors' views. The canonical record of the paper is at the publisher link above.
- Table 1's header row and the leading per-row values (20 per domain, 140 in the totals) were garbled by PDF extraction; the three planner columns were disambiguated by arithmetic consistency, since the per-domain agile scores sum exactly to the reported totals 66.82/31.72/40.54.
- The extracted byline lists Togarepi first while the provided metadata lists Quenard first; author ordering differs between the two sources (same four authors and affiliation).
Go deeper on this paper
Wrote a paper? Stress-test it before reviewers do.
Upload your manuscript for the same structured scrutiny — reasoning, statistics, evidence, figures, and reproducibility.