面向数值全序HTN规划的SMT-based HTN-SAT编码

# 基于SMT的HTN-SAT编码实现数值化TOHTN规划
来源：https://arxiv.org/html/2609.03938
###### 摘要
尽管层次任务网络（HTN）规划近年来受到广泛关注，但其对数值推理的支持仍然非常有限。本文研究了数值全序HTN（TOHTN）规划问题，展示了如何利用标准的基于SAT的编码通过SMT自然扩展以处理数值流（numeric fluents）。此外，我们引入了一套数值TOHTN规划基准测试，为该领域的评估提供了首个公共基础。实验结果表明，这种简单的编码方式已能构成一个具有竞争力的基准方法。本工作为更富表现力的HTN规划方法奠定了基础。
1 格勒诺布尔大学，法国 {takudzwa.togarepi, gaspard.quenard, damien.pellier, humbert.fiorino}@univ-grenoble-alpes.fr

## 引言
层次任务网络（HTN）规划（Erol, Hendler, and Nau 1994 (https://arxiv.org/html/2609.03938#bib.bib7)）是一种利用领域特定知识将复杂任务分解为更简单子任务的规划范式。与经典规划不同，HTN引入了无法直接执行的抽象任务（abstract tasks），以及描述如何将这些任务精炼为包含原始任务（即，可执行动作）和必须自身被递归精炼的其他抽象任务的部分有序子任务集的方法（methods）。HTN规划器的目标是将初始抽象任务迭代分解为一个有效计划（即，一个可执行的原始任务序列）。

本文聚焦于全序HTN（TOHTN）规划的探讨，这是HTN问题中一个非常流行的子类，其中的分解方法指定了为实现抽象任务而按顺序执行的原始动作和抽象任务的全序列表。

尽管HTN规划是自动规划的核心主题，并已被纳入近年的国际规划竞赛（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)），但与经典规划形式化方法相比，它仍存在重要的建模局限性。特别是，经典规划通过PDDL2.1（Fox and Long 2003 (https://arxiv.org/html/2609.03938#bib.bib8)）引入的数值和时间特性（如资源管理、成本和持续时间）在大多数HTN规划器中是缺失的。尽管一些工作研究了将时间方面集成到HTN规划中（Pellier et al. 2022 (https://arxiv.org/html/2609.03938#bib.bib12)），但时间HTN的形式化仍然是一个活跃的研究课题，当前的提案尚未获得广泛采用。相比之下，数值推理（例如，通过对原始任务的前置条件和效果施加数值约束）可以自然地被纳入，但迄今为止受到的关注很少。

这些特性在许多现实世界应用中至关重要，包括物流、机器人技术和调度，这些应用需要进行数量推理。据我们所知，只有Siadex（Castillo et al. 2006 (https://arxiv.org/html/2609.03938#bib.bib5)）和Aries（Bit-Monnot 2023 (https://arxiv.org/html/2609.03938#bib.bib4)）支持HTN规划中的数值推理。这种限制制约了HTN规划在现实领域中的适用性。

在本文中，我们提出利用可满足性模理论（SMT）扩展基于SAT的TOHTN规划以处理数值约束。基于SAT的方法近年来在TOHTN规划中展现出强大的性能，这得益于现代求解器的高效性以及改进的编码和搜索策略（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)），但它们本质上局限于命题表示。与基于启发式搜索的方法（通常需要大量适配以处理数值推理）相比，基于SAT的方法可以通过将编码提升到SMT来更自然地扩展，而无需从根本上修改搜索过程。通过转向SMT，我们在保持逻辑编码优势的同时，实现了对数值变量的推理。

本文提出了一种新的编码，将基于SAT的TOHTN规划扩展到使用SMT求解器处理数值变量和约束。此外，我们设计并提供了七个数值TOHTN基准测试来评估这些方法。实验表明，我们的基于SMT的编码能比现有的数值HTN规划器更高效地求解数值TOHTN问题。

本文结构如下：首先，介绍数值TOHTN规划的概念。其次，描述当前基于SAT的TOHTN规划器用于寻找解决方案的基本增量编码。然后，解释如何修改该编码以支持数值约束。最后，将该方法与其他数值HTN规划器进行比较。

## 数值TOHTN规划问题
我们呈现数值TOHTN规划的形式化，构建于（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)）之上，并遵循PDDL2.1中引入并在HDDL 2.1中讨论的数值流处理（Pellier et al. 2022 (https://arxiv.org/html/2609.03938#bib.bib12)）。

### 任务、动作、方法、数值流和任务网络
任务是HTN规划的核心。任务由名称和参数定义。任务分为原始任务（primitive）和抽象任务（abstract）：原始任务直接影响世界状态，而抽象任务不直接影响；相反，它们必须使用方法分解为原始任务后才能被执行。

我们假设一个有限的命题集L和一个有限的数值流集F。F上的数值表达式由常量和F中的流使用算术运算符+、-、×、/构建。数值约束是形如fBowtieξ的表达式，其中f∈F是一个数值流，ξ是一个数值表达式，Bowtie∈{<,≤,=,≥,>}。

原始任务a类似于经典规划中的动作，由一个元组(name(a), precond(a), effect(a))定义。其前置条件precond(a)=(precond_L(a), precond_N(a))由一组命题前置条件precond_L(a)和一组数值约束precond_N(a)组成。其效果effect(a)=(effect^+(a), effect^-(a), effect_N(a))由命题上的添加效果和删除效果以及一组数值效果effect_N(a)组成。在这项工作中，我们将数值效果限制为形如f:=ξ的赋值效果，其中f∈F，ξ是F上的数值表达式。

状态s被定义为一对(l,v)，其中l⊆L是在该状态下为真的命题集，v:F→ℝ是一个赋值函数，为每个数值流分配一个实数值。任务a在状态s=(l,v)下是可执行的，当且仅当precond_L(a)⊆l且v⊨precond_N(a)，即在v下precond_N(a)中的所有数值约束都得到满足。如果任务a在状态s=(l,v)下可执行，则应用其效果会产生一个新状态s'=(l',v')，其中l'=(l∖effect^-(a))∪effect^+(a)，v'是通过对v应用effect_N(a)获得的。

方法m=(name(m), c, w_m)指示了如何将一个抽象任务c精炼为一个任务网络w_m，称为m的子任务。为方便表示，我们定义M(c)={m=(name(m), c, w_m) | m∈M}为所有可以应用于分解抽象任务c的方法的集合。

### 规划问题与解
###### 定义1（TOHTN规划问题）
一个数值TOHTN规划问题P是一个元组(L, F, C, A, M, c_I, s_I, g)，其中：L是有限命题集；F是有限数值流集；C是有限抽象任务集；A是有限原始任务集；M是有限分解方法集；c_I∈C是待分解的初始抽象任务；s_I=(l_I, v_I)∈S是初始状态；g=(g_L, g_N)是目标条件，其中g_L⊆L是一组命题，g_N是一组数值约束。

###### 定义2（TOHTN规划问题解）
数值TOHTN规划问题P的解是一个原始任务网络π∈A*，使得：
1. π是通过使用方法精炼c_I得到的，
2. π在s_I下是可执行的，
3. π在执行后达到目标g。

## 基于SAT的TOHTN搜索
HTN规划可以自然地表示为一个AND/OR树（Ghallab, Nau, and Traverso 2004 (https://arxiv.org/html/2609.03938#bib.bib9)），其中根节点包含初始抽象任务。该树表示初始抽象任务潜在无限分解的一个有限片段，并在搜索过程中逐步扩展。OR节点对应于具有多种可能分解（方法）的抽象任务，而AND节点代表其子任务都必须被实现的方法。通过为每个OR节点选择一个子节点，为每个AND节点选择所有子节点，可以获得一个有效计划，使得叶子节点构成一个实现目标的原始动作序列。图1左侧给出了这样一个AND/OR树的示例（https://arxiv.org/html/2609.03938#Sx3.F1）。该树在此并未完全展开，因为抽象任务T_8未展开。

在基于SAT的HTN规划中，AND/OR树被编码为一个SAT公式，当且仅当其中存在解时该公式是可满足的，且满足赋值对应于计划。然而，仅靠AND/OR树对于当前的编码是不够的。实际上，子句必须捕获动作转换，确保在执行时前置条件成立并且效果得以应用。所有当前的基于SAT的HTN规划器都通过为每个任务分配一个离散的时间步来表示其可能的执行时间来解决这个问题；而这正是AND/OR树的结构表示所提供的。这就是为什么所有当前的HTN-SAT规划器都依赖于在TreeRex和totSAT中独立引入的一种结构（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)），该结构等价于AND/OR树，同时使执行时间步显式化。我们将此结构称为*紧致路径分解树*（cPDT）；其节点可以包含多个任务，并组织如下：
- •根节点仅包含初始抽象任务c_I。
- •要扩展一个节点P，其子节点构建如下：
  - –对于P中的每个抽象任务c和每个将c分解为子任务⟨t_1,...,t_n⟩的方法m_i，P的第k个子节点包含任务t_k。
  - –对于P中的每个原始任务a，P的第一个子节点包含a。

cPDT保证了对于叶子节点l_i处的任何任务t，所有必须在t之前执行的任务都出现在叶子节点l_j处，其中j < i。因此，从左到右扫描叶子节点可以揭示cPDT中编码的所有可能计划。图1左侧AND/OR树对应的cPDT显示在其右侧。参见说明图1：左侧是简单的分解图式，形式为AND/OR树，其中T_i表示抽象任务i，M_i表示方法i，A_i表示动作i。右侧我们表示对应的cPDT。一个潜在的相同解在两者中都用蓝色高亮显示。

我们现在介绍一个增量编码，它捕获了当前HTN-SAT编码（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)）共享的核心思想，用于确定在给定的cPDT中是否存在解。这个编码是接下来介绍的数值扩展的基础。

对于cPDT的每个节点P，我们使用布尔变量P_t表示任务t在P处是活跃的，变量P_p表示命题p∈L在P处成立，以及辅助变量P_prim表示在P处有一个原始任务是活跃的。当t是原始任务时，我们记为a；当t是抽象任务时，我们记为c。对于任何叶子节点P，我们用P^+=successor(P)表示在分解层次结构诱导的从左到右顺序中紧随P之后执行的叶子节点。为了处理目标状态，我们引入了一个特殊的*虚拟*节点G，表示目标。因此，对于任何没有后继的节点P，我们定义P^+=G。如图1所示（https://arxiv.org/html/2609.03938#Sx3.F1），可能存在某些解在给定位置没有活跃任务。为了处理这种情况，我们引入一个特殊动作ε，使得precond(ε)=effect(ε)=∅。该动作在编码中被视为普通动作，但在最终计划中被忽略。我们用P_ε表示节点P处没有活跃任务。

#### 初始任务、初始状态和目标。
在根节点R处，初始任务和初始状态必须成立，且在G处目标必须成立：
R_{c_I}
∀p∈s_I: R_p
∀p∈L∖s_I: ¬R_p
∀p∈g: G_p

#### 叶子节点约束。
对于每个叶子节点P，恰好有一个任务在P处是活跃的：
⋁_{t∈Tasks(P)} P_t
⋀_{t,t'∈Tasks(P), t≠t'} ¬(P_t ∧ P_{t'})

如果原始任务a在P处是活跃的，那么其前置条件必须在P处成立，且其效果在P^+处成立：
∀a∈Tasks(P)∩A: P_a ⇒ ⋀_{p∈precond(a)} P_p
∀a∈Tasks(P)∩A: P_a ⇒ ⋀_{p∈effect^+(a)} P^+_p
∀a∈Tasks(P)∩A: P_a ⇒ ⋀_{p∈effect^-(a)} ¬P^+_p