arXiv论文：用SMT扩展SAT编码，为数值TOHTN规划提供首个基准套件
法国团队提出数值全序HTN规划的SMT编码方案，并发布评测基准，实验显示该简单编码已具备竞争力。
AI解读：这篇论文要解决的是HTN规划中数值推理支持薄弱的问题。HTN（层次任务网络）规划常用于机器人、制造等需要任务分解的领域，但传统编码大多只能处理符号状态，遇到燃料、能量、距离这类连续数值就难以扩展。作者把经典SAT编码升级为SMT（可满足性模理论），让规划器能直接处理数值流（numeric fluents），相当于给原有方法加上了算术推理能力。更重要的是，他们同时公开了一套面向数值TOHTN规划的基准套件，此前这一领域缺少统一的评测基础。实验表明，这种简单编码已构成一个有竞争力的基线，意味着后续研究者不必从零起步，可以直接用它做对比。对从事AI规划的研究者来说，这意味着可以尝试把现有HTN求解器推向更多带资源约束的现实场景；对工程人员而言，该编码思路也可能降低在项目里落地数值HTN规划的门槛。论文发表于ICAPS的HPlan 2026研讨会，提供的基准和编码目前是学术成果，尚未以开源工具形式发布，实际易用性还需进一步检验。
一篇题为《Towards Numerical TOHTN Planning with SMT-based HTN-SAT Encoding》的arXiv论文（编号2609.03938）研究了数值全序HTN（TOHTN）规划问题，提出将标准SAT编码自然扩展为SMT以处理数值流，并发布了面向该场景的基准套件。实验显示，这一简单编码已具备竞争力。
方法与结果
论文指出，尽管HTN规划近年受到较多关注，但对数值推理的支持仍然非常有限。作者针对数值TOHTN规划，展示了如何将基于SAT的标准编码扩展为SMT编码，从而处理数值流。
研究还引入了一个数值TOHTN规划的基准套件，为该设定下的评测提供了首个共同基础。实验结果表明，这种简单编码已经构成一个有竞争力的基线。论文认为，这项工作为更富有表现力的HTN规划方法开辟了道路。
- 论文发表于第9届ICAPS分层规划研讨会（HPlan 2026）论文集，页码为32-36。
- 作者包括Gaspard Quenard、Takudzwa Togarepi、Damien Pellier和Humbert Fiorino。
- 提交历史显示论文于2026年9月3日提交至arXiv。