多值动作语言与并发约束程序的研究与应用

# 多值动作语言与并发约束程序的研究与应用 ## 一、BF D MV 语言的扩展与特性 ### 1.1 具体扩展 BF D MV 语言使用 SICStus Prolog 实现，是布尔情况编码的直接推广。为便于编码常见问题特征，还引入了一些额外的语法扩展。 #### 1.1.1 成本信息添加 可以添加每个动作、流和计划全局成本的信息，具体规则如下： - `action cost(action,VAL)`：若未提供信息，默认成本为 1。 - `state cost(FE)`：若未提供信息，默认成本为 1，其中 FE 是基于当前流构建的流表达式。 - `plan cost(plan op n)`：添加动作序列允许的全局成本信息。 - `goal cost(goal op NUM)`：添加状态序列允许的全局成本约束。 - `minimize action`：将搜索约束到全局动作成本最小的计划。 - `minimize state`：强制搜索目标状态成本最小的计划。 这些基于成本的约束的实现依赖于 SICStus 标记谓词提供的优化特性，标记阶段通过施加要优化的目标函数来引导。 #### 1.1.2 绝对时间约束定义 该语言允许定义绝对时间约束，即涉及轨迹中特定时间实例的约束。定义定时流为 `FLUENT @ TIME` 对，用于构建定时流表达式（TE）和定时原始约束（TC）。例如： - `contains(5) @ 2 leq contains(5) @ 4`：表示在时间 2 时，桶 5 中的水量最多与时间 4 时相同。 - `contains(12) @ 2 eq 3`：表示在时间 3 时，桶 12 中有 3 升水。 这些构造可用于以下表达式： - `cross constraint(TC)`：强制定时约束 TC 成立。 - `holds(FC,StateNumber)`：是上述约束的简化，表明原始流约束 FC 在所需的状态编号（初始状态编号为 0）成立，是 `initially` 原语的推广，可利用点信息驱动计划搜索。 - `always(FC)`：表示流约束 FC 在所有状态中都成立，必须使用当前流以避免负引用。 ### 1.2 扩展的 BF D MV 语言：展望未来 提议扩展 BF D MV 语言，以允许对轨迹的未来步骤进行推理的约束。 #### 1.2.1 语法 将之前的语法推广，注释流的形式为 `f a`，其中 `f ∈ Z`。构建流公式和流约束现在意味着能够展望计算的未来步骤。此外，引入了另一个流约束 `incr(f a, n)`，其中 `f a` 是注释流，`n` 是数字，该约束提供了加法流的简化视图。 #### 1.2.2 语义 语义的定义成为“验证”状态序列以验证其是否适合作为轨迹的过程。给定流公式/约束 `ϕ` 和时间步 `i`，定义 `Absolute(ϕ, i)` 如下： - 若 `ϕ ≡ n`，则 `Absolute(ϕ, i) = n`。 - 若 `ϕ ≡ f a`，则 `Absolute(ϕ, i) = f i+a`。 - 若 `ϕ ≡ ϕ1 ⊕ ϕ2`，则 `Absolute(ϕ, i) = Absolute(ϕ1, i) ⊕ Absolute(ϕ2, i)`。 - 若 `ϕ ≡ abs(ϕ1)`，则 `Absolute(ϕ, i) = abs(Absolute(ϕ1, i))`。 - 若 `ϕ ≡ rei(ϕ1)`，则 `Absolute(ϕ, i) = rei(Absolute(ϕ1, i))`。 - 若 `ϕ ≡ ϕ1 op ϕ2`，则 `Absolute(ϕ, i) = Absolute(ϕ1, i) op Absolute(ϕ2, i)`。 - 若 `ϕ ≡ incr(ϕ1, n)`，则 `Absolute(ϕ, i) = incr(Absolute(ϕ1, i), n)`。 对于状态序列 `¯ν = ⟨ν0, ..., νn⟩` 和动作序列 `¯a = ⟨a0, ..., an−1⟩`，定义 `Global(¯a, ¯ν)` 为： \[Global(¯a, ¯ν) = \sum_{i = 0}^{n - 1} Absolute(Eff(ai, ¯ν, i), i + 1)\] 状态序列 `¯ν` 是轨迹的条件如下： - 对于动作理论中形式为 `initial(C)` 的每个公理，有 `¯ν |=0 C`。 - 对于动作理论中形式为 `goal(C)` 的每个公理，有 `¯ν |=|¯ν|−1 C`。 - 存在动作序列 `¯a = ⟨a0, a1, ..., an−1⟩`，具有以下属性：对于每个 `0 ≤ i < n`，`ai` 在 `¯ν` 的第 `i` 步是可执行的，且 `νi+1 = σ∪(νi ∩ νi+1)`，其中 `σ` 是 `Red(Global(¯a, ¯ν), ¯ν, i+1)∧Clo(¯ν, i+1)` 的解。 特别地，若 `Incr(C, i) = {n | incr(f i, n) ∈ C}` 是注释流 `f i` 的所有 `incr` 约束，则对于状态序列 `¯ν`，`θ` 是其解的条件是 `νi(f) = νi−1(f) + ∑_{n∈Incr(C,i)} n`。 ## 二、实验分析 ### 2.1 三桶问题 对三桶问题的不同编码进行了实验。有三个容量分别为 `N`（偶数）、`N/2 + 1` 和 `N/2 - 1` 的桶，初始时最大的桶装满酒，另外两个为空，目标是使两个较大的桶中的酒量相同，唯一允许的动作是将酒从一个桶倒入另一个桶，直到后者满或前者空。 以下是不同实例的实验结果： | 桶容量 | 长度 | 答案 | B（lparse） | B（Smodels） | B（Cmodels） | CLP(FD) | BF D MV（无约束） | BF D MV（计划成本约束） | | ---- | ---- | ---- | ---- | ---- | ---- | ---- | ---- | ---- | | 8 - 5 - 3 | 6 | N | 8.95 | 0.10 | 0.85 | 0.16 + 0.36 | 0.02 + 0.11 | (70) 0.01 + 0.10 | | 8 - 5 - 3 | 7 | Y | 8.94 | 0.28 | 1.34 | 0.19 + 0.47 | 0.02 + 0.13 | (70) 0.03 + 0.13 | | 8 - 5 - 3 | 8 | Y | 9.16 | 0.39 | 2.07 | 0.18 + 2.66 | 0.03 + 0.85 | (70) 0.01 + 0.79 | | 8 - 5 - 3 | 9 | Y | 9.22 | 0.39 | 8.11 | 0.22 + 1.05 | 0.02 + 0.28 | (70) 0.05 + 0.28 | | 12 - 7 - 5 | 10 | N | 35.63 | 18.31 | 325.28 | 0.45 + 26.86 | 0.05 + 7.79 | (90) 0.03 + 6.78 | | 12 - 7 - 5 | 11 | Y | 35.70 | 45.91 | 781.28 | 0.52 + 28.87 | 0.05 + 9.46 | (90) 0.04 + 5.03 | | 12 - 7 - 5 | 12 | Y | 35.58 | 81.12 | 4692.08 | 0.58 + 203.34 | 0.06 + 57.42 | (100) 0.04 + 35.31 | | 12 - 7 - 5 | 13 | Y | 35.67 | 18.87 | 1581.49 | 0.66 + 66.52 | 0.06 + 25.65 | (100) 0.03 + 23.26 | | 16 - 9 - 7 | 14 | N | 114.16 | 2018.65 | – | 1.28 + 2560.90 | 0.07 + 564.68 | (170) 0.07 + 518.78 | | 16 - 9 - 7 | 15 | Y | 113.53 | 2493.61 | – | 1.29 + 2833.97 | 0.07 + 688.84 | (170) 0.07 + 520.14 | | 16 - 9 - 7 | 16 | Y | 115.36 | 6801.36 | – | 1.37 + 17765.62 | 0.06 + 4282.86 | (170) 0.04 + 1904.17 | | 16 - 9 - 7 | 17 | Y | 114.04 | 2294.15 | – | 1.55 + 6289.06 | 0.06