Page 18 - 《软件学报》2026年第1期

陈蔚骏 等: 向量加法系统可达性问题复杂性下界研究综述 15

m 即可, 其代价是需要引入一个辅助计数器记录剩余可用测零次数. 但即便是在最新的工作里, 常数
零次数恰好是
个计数器的代价也并不算高.
至此, 我们得到了一套相当完善的测零方法. 归约中的关键步骤仅剩以下两步.
1) 构造一对计数器 x、x, 使其总和等于某给定函数 f (n).
2) 对任意 m ∈ N 和给定的 f (n), 构造一对值分别等于 m、2mf (n) 的计数器.
事实上, 后续所有工作中几乎都涉及了此测零方法和上述步骤的变体. 在接下来的几节, 我们将会看到此方法
的具体应用以及研究者是如何通过不断改进这一技巧得到更好的下界的.
3.2 下界证明框架
Czerwiński 等人 [35] 形式化了第 3.1.2 节中的想法, 他们将实现步骤 1) 的程序模块称作放大器 (amplifier); 放大
x = f(n) 和步骤 m、2mf(n) 的计数器共同称为乘法三元组 (multiplication triple).
器构造出的计数器 2) 中值分别为
后续工作 [14,15,35−38] 均沿用了相同的思路, 但不同研究者的定义方式不同, 这对该方法未来的改进与推广十分不利.
我们将在第 3.2.1 节中严格给出三元组和放大器的一般定义, 随后在第 3.2.2 节介绍了基于二者的通用模拟测零技
巧与下界证明框架, 并在后文中以此框架统一地梳理近些年的进展.
3.2.1 乘法三元组与放大器
本节给出乘法三元组和放大器的定义, 相关文献中具体使用的不同定义均与此等价. 乘法三元组可以推广到
更一般的情形: 任给一个三元不变量 inv, 我们均可按照如下方式定义一个 inv-三元组.
3
定义 3. 给定函数 inv : N → N, 一个 inv-三元组形如 τ = (a,b,c,A,B,X), 其中, A,B ∈ N X 是计数器的有限集;
;
a,b,c ∈ X 是 3 个计数器, 它们满足 a = A, b = B, inv(A,B,c) = 0 且对任意 x ∈ X\{a,b,c} 都有 x = 0.
直观上, A 代表 τ 允许的测零次数的 2 倍, 需为偶数; B 代表待测零计数器值应当满足的上界, 通常是某个增长
超过指数量级的函数; c 用于在每次模拟中记录下待测零计数器的信息, 故应和 a、b 保持某些不变量关系 inv. 若
inv 定义为 inv(A,B,C) = C − AB, 对应的 inv-三元组即乘法三元组, 本节仅讨论乘法三元组.
考虑某个使用计数器 X = {x 1 ,..., x k } 的程序 P, 由于乘法三元组确定了 X 中所有计数器的值, 后文有时直接用
τ = (a,b,c,A,B,X) 来指定初始或终止格局. 此外, 若某次完全执行后对任意计数器 x ∈ Z ⊆ X 都有 x = 0, 则此次执
行称为 Z-执行. 若某次 Z-执行初始格局为 α, 终止格局为 β, 则称 P 可以从 α 出发 Z-计算出 β.
定义 4. 给定 f (n) ⩾ n, 一个 f(n)-放大器是一个 5-元组 Ampl = (P,X,(a ,b ,c ),(a,b,c),Z).
′
′
′
′
′
● P 是一段计数器程序, 它使用的所有计数器集合为有限集 X ⊇ Z ∪{a,b,c}∪{a ,b ,c }.
′
● a,b,c,a ,b ,c ∈ X 是计数器; a 、b 、c 称为放大器的输入; a、b、c 称为放大器的输出; Z , ∅ 是一组控制计
′
′
′
′
′
′
数器.
′
′
′
● 若存在 A s ,B ∈ N, 使得 (a ,b ,c ,A s ,B,X) 构成一个乘法三元组, 则任意 Z-执行后存在 A t ∈ N 使得 (a,b,c,
A t , f(B),X) 构成一个乘法三元组.
′
′
′
● 对任何 A,B ∈ N, 存在 A s ∈ N, 使得: 若 τ s = (a ,b ,c ,A s ,B,X) 构成一个乘法三元组, 则从该格局出发可以
Z-计算得到某个 τ t = (a,b,c,A t , f (B),X) 使得 A t ⩾ A.
Z 可弥补 Lipton Z 中计数器的取值是否为 0 来“控制”程序终止
引入控制计数器集合 方法的局限: 将通过判定
′
′
′
′
于某个希望的格局. 为此 Z , ∅ 是必须的. 注意, {a,b,c}、{a ,b ,c }、Z 不必互斥, 一般而言至少有 c ∈ Z. 事实上这
3 组计数器的复用程度往往对 d-VASS 复杂性下界有显著影响.
3.2.2 通用模拟测零技术
第 1.4.1 节定义了计数器机器 f(n)-有界可达性问题, 基于乘法三元组和放大器, 我们有如下引理.
引理 10. 给定 f (n), 若存在一族 f(n)-放大器 Ampl n = (P n ,X n ,(a ,b ,c ),(a,b,c),Z n ) 使得其中程序 P n 长度为
′
′
′
poly(n), 则有如下结论.
1) CM f(n)-bounded reachability ⩽ p VASS reachability.
2) 当 |X n | 是个与 n 无关的常数 d 时, CM f(n)-bounded reachability ⩽ p (d + 3)-VASS reachability.