HTN（层次任务网络）规划近年来受到广泛关注，但对数值推理的支持仍然不足。本文聚焦于全序数值 HTN（TOHTN）规划，提出在传统基于 SAT 的编码上自然地加入 SMT 技术，以处理数值流变量（numeric fluents）。具体做法是将每个数值流的取值约束表示为 SMT 公式，例如前置条件可以写成 $x \ge 5$，效果函数则用等式或不等式约束描述。这样，原本只能处理布尔变量的 SAT 编码被扩展为混合布尔‑数值的 SAT‑SMT 形式，保持了编码的简洁性同时获得了数值推理能力。
为了促进该方向的实验研究，本文还构建了一套数值 TOHTN 基准测试集，涵盖了不同规模和数值复杂度的任务网络，为后续算法提供统一的评估平台。实验在该基准上对比了纯 SAT 编码、本文的 SAT‑SMT 编码以及若干现有数值规划方法。结果显示，仅凭上述简易的 SMT 扩展即可形成一个具有竞争力的基线，尤其在包含大量数值约束的实例中表现突出。
本文的工作为数值 HTN 规划打开了新的可能性，后续可以在此基础上引入更复杂的数值约束、优化目标或学习驱动的任务分解策略，以提升规划的表达力和求解效率。
点评