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

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

定理 4 [33] . 对于任意的 d ⩾ 3, d-VASS 可达性问题在 F d 中.
此结论对复杂性上界的刻画十分优美, 但遗憾的是目前没有相匹配的下界. 事实上, 理论计算机科学界对
VASS 可达性问题的复杂性下界的研究由来已久. 一方面, 早在 1976 年该问题可判定性尚且未知时, Lipton [34] 就给
出了 EXPSPACE-难的下界归约. 但由于问题复杂, 下界研究随后沉寂了 40 余年. 新的突破始于 2020 年, Czerwiński
等人 [35] 借鉴 Lipton 的证明方法开创了一套普适性强的归约流程, 并给出了首个非初等的 Tower-难下界. 该工作
发表于 Journal of the ACM. 接着在 2021 年, Czerwiński 等人 [14] 和 Leroux [15] 通过巧妙地改进流程细节, 为一般
VASS 可达性问题提供了匹配的 Ackermann 下界, 一个开放多年的复杂性问题至此得到解决. 另一方面, d-VASS
可达性问题的参数化下界更具挑战性. 经过研究者 [36−38] 的不断努力, 目前最先进的结果如下.
定理 5 [36] . 对于任意的 d ⩾ 3, (2d + 3)-VASS 可达性问题是 F d -难的.
除了结论之外, 改进过程本身亦有重要的参考价值, 接下来我们将总结自 1976 年以来人们为解决下界问题所
提出的研究方法, 指出不同方法的使用范围和局限性, 以期对未来的相关工作有所启发.
3.1 Lipton 证明技术
Lipton 给出了 VASS 可达性问题的第 1 个非平凡复杂性下界——EXPSPACE-难. 其原方法是基于并行程序
(parallel program) 进行的, 文献 [16] 中对此有详尽的描述, 在此不再赘述. 在第 3.1.1 节中, 我们将基于更为现代的
计数器程序方法给出一个全新的证明, 并在第 3.1.2 节分析 Lipton 方法的局限性及其对后续研究工作的启发.
3.1.1 EXPSPACE-难归约
2 n
本节介绍 Lipton 的证明思路. 首先, 我们需要选择合适的问题用于归约. 引理 2 表明 2 - 有界计数器机器可达
性问题是 EXPSPACE-难的, 本节正是从此问题出发进行归约. 给定一个 2 -BCM M, 我们接着将其归约到一个计
2 n

数器程序 P. 由于计数器机器和计数器程序唯一的区别在于前者可以测零, 但后者不具备此能力, 故归约的关键在
M 中的每一次测零? 事实上, 后续每一次下界提高的背后都蕴含着模拟测零技术的
于: 如何使用一个程序模拟
改进.
在第 2.2.3.1 节我们曾提到一种简单的测零技术: 当已知计数器 x 满足 0 ⩽ x ⩽ b 时, 只需执行“x+= b; x−= b;”

程序. 若该语句顺利执行, 定有 x ⩽ 0, 从而 x = 0. 当上界 b 充分小 (关于输入规模成指数量级) 时, 可以高效构造出
2 n
2 0
2 1
2 2 n 2 , 2 ,..., 2 .
这条语句. 但显然 不符合此情形. 最终, Lipton 巧妙地通过递归构造出了上界序列
2 i
定义 A i = 2 , 构造过程中为了保证某个计数器 x i 是 A i -有界的, 只需定义辅助计数器 x i 使得 x i + x i = A i 即可.
,
2
,
假设已有 x i + x i = A i y i +y i = A i s i+1 + s i+1 = A i+1 , 需要对 s i+1 测零, 又观察到有 A i+1 = A . 为了实现 s i+1 += A i+1 的效
i
x i , y i 构造图 6
果只需用 中程序 P i 所示的双层循环.

loop
i x +=1, i x -=1;
loop loop loop
i x +=1, i x -=1; i y +=1, i y -=1,
loop i y -=1, i y +=1, i s + 1 +=1, i s + 1 -=1;
i s +=1,
i y +=1, i y -=1, �lagy i + = 1; i s -=1; reset ( y ) ;
i
i r + 1 +=1, i r + 1 -=1; goto zt i ; reset ( x ) ; goto end;
i
zero-test ( y ); zt i : zero-test ( s ) ;
i ry i : skip; i
zero-test ( x ); do �lagy i -=1, goto ry i ;
i
or �lagx i -=1, goto rx i ;
end: halt ;
reset zero-test (S i+1 )
P i
图 6 Lipton 的模拟测零技术

在初始 x i = y i = s i+1 = 0 的情形下, 此段程序可以执行完全, 最终 x i = y i = A i , s i+1 = A i+1 . 但此段程序有两个问
题: 其一, 它没有恢复 x i 、y i 、s i 的状态, 无法用 x i 、y i 进行下一次测零; 其二, 它是递归构造的, zero-test( ) 和 zero-
y i
i
test( x i ) 各需要使用两对辅助计数器, 使得最终整个程序需要使用 4 个计数器, 这显然是无法高效完成的. 为此, 可
以将 zero-test( y i ) 替换成图 6 中的 reset( y i ), 将 y i 、y i 的值记录到 s i 、s i 的同时重置为 y i = 0, y i = A i , 随后通过 zero-