Page 28 - 《软件学报》2026年第1期
P. 28
陈蔚骏 等: 向量加法系统可达性问题复杂性下界研究综述 25
图 16 右侧所示.
给定 λ 和 , 若 eval d,i 0 的某次执行从对应 λ 的好格局 α 出发且每次循环都执行到了允许的最大次数后得到 β,
i 0
且 2 α(B 0 ) 整除 α(A 0 ) 时, 不难得到如下结论.
● i > i 0 时, 每次对 的修改都伴随着对 a i 的修改, 因此 β(A i ) = α(A i ).
y
● 第 1 个循环最多执行 α(A 1 ) 次后得到中间格局 α 1 (c) = α(A 1 ).
● 第 2 个循环至多执行 α(A 0 ) 次后得到中间格局 α 2 (c) = α(A 1 − A 0 ) α 2 (A i ) = α(A 1 + A 0 ).
,
● 第 3 个循环至多执行 α(B 0 ) 次, 因此 β(B i−1 ) = α(B i−1 )+α(B 0 )+1 β(B i ) = α(B i )−1, 符合公式 (15).
,
● 第 4 个循环依次执行 α(A 0 )2 ,...,A 0 2 −α(B 0 ) 次, 共 α(A 0 ) 1−2 −α(B 0 ) ) 次且最终 β(A 0 ) = A 0 2 −α(B 0 ) .
(
−1
● 第 5 个循环执行 α(A 1 − A 0 ) 次, 使得最终 β(A i ) = α 2 (A i )+α(A 1 − A 0 ) = 2α(A 1 ) β(A 1 ) = ... = β(A i−1 ) = α(A 1 )−
,
α(A 1 − A 0 ) = α(A 0 ), 符合公式 (17).
B
update ( B 0 ) 中的外层循环至多执行 (β(B 0 )+1)/2 = 1+α(B 0 ) 次, 内层循环每次将 翻倍, 最终 β(B) =
d,1
2 1+α(B 0 ) α(B 0 ) = 2 β(B 0 ) , 因此, β 是对应 Eval(λ) 的好格局. Leroux [38] 还证明了如下引理.
引理 16 [38] . 若 α 是一个对应非平凡编码 λ 的合法格局, 执行 eval d,i 后得到的 β 也是合法的; 若 β 是好的, 则 α
,
也是好的, 并且 i = i λ β 对应编码 Eval(λ).
eval d 的定义与第 3.4.1 节一致, 并且引理 15 F d+1 (n) - 生成器
最终 对新的 eval d 也成立. 借此我们可以构造一个 2
{ }
Gen d = (P d ,X d ,(a,b,c),Z d ), 其中, X d 即上述所有计数器, , P d 如图 17 所示.
Z d = a d+1 ,b,b 0 ∪{b i } i∈[d] 0
0 b += n , b += n + , b = 2 ; n
1
d
n
0 a +=1, a += 2 , …, d a += 2 , n d a + 1 += 2 2n+ 1 ;
1
n
n
loop 0 a +=1, a += 2 , …, a += 2 , a + += 2 2n+ 1 ;
1
1
d
d
loop eval d ;
loop c +=1, dec( a 1 ,… ,a + d 1 ) ;
loop 0 b -=1;
图 17 优化后的 P d
考虑 P d 的某个 Z d -执行, 易知: 前 3 行构造了一个对应 λ 0 = ((n+1)e d ,n) 的好格局 α 0 , 且 α 0 (A 0 ) , 0. 执行完若
c
干次 eval d 后得到一个合法格局 β, 终止后 a d+1 和 {b i } i∈[d] 为 0 表明 β(A d+1 ) = β(A 1 ), 且 A 1 的值都转移到了 上, 因此
一定有 β(c) = β(A 1 ) ⩾ β(A 0 )2 β(B 0 ) ⩾ β(A 0 )β(B). 至少存在一种执行 β(c) = β(A 0 )β(B), 则 β 是个对应 (0 d ,F d+1 (n)) 的好
( F d+1 (n) )
格局, 终止后 b = 0, a 0 = 0, 从而得到了一个三元组 τ t = a 0 ,b,c,β(A 0 ),2 ; 其他分支满足 β(c) > β(A 0 )β(B), 虽然
不是三元组, 但不影响引理 10 的正确性, 因为后续程序使用 a 0 、b、c 测零时永远有 c > a 0 b, 无法得到任何{c}-执行.
最后, |X d | = 2d +8, |Z d | = d +4, 根据推论 2 可知, (2d + 8)-VASS 的可达性问题是 F d + 1 -难的. 最终观察到 b d 只
会减少, 因此可以用具体数值替代; 由于 x d 只会增加, 因此可以省略. 最终有如下定理.
定理 11 [38] . d ⩾ 3 时, (2d + 4)-VASS 可达性问题是 F d -难的.
此方法首次突破了因三元组技术带来的 3d +Ω(1) 的下界, 但某种程度上也具有程序可读性较差的缺点. 同时,
我们目前还无法判断, 这 d +Θ(1) 的提升究竟是源于指数形式的不变量, 还是与向量编码方法本身有关. 事实上在
下一节中, 我们将会看出此次优化完全是新不变量带来的, 因为在 Czerwiński 等人 [14,36,37] 的递归构造框架下, 我们
依然能够基于指数形式的不变量得到一致的结论.
3.5 (2d+3)-VASS 可达性问题是 F d -难的
Czerwiński 等人在文献 [37] 中提出了目前最先进的下界归约技术. 该方法结合了第 3.3 及 3.4 节中介绍的各
方法的优点.
1) 选择基于递归的方法构造 F d (n)-放大器, 使得构造的程序与相关证明可读性强.
2) 继承了第 3.3.2 节中 Czerwiński 等人 [14,36] 对三元组的解释, 将 B 理解为测零次数的上界, 使得递归过程可以
直接使用输入三元组进行测零.
C = AB 的不变量形式, 而是选择继承第 3.4.2 节中 Leroux [38] 提出的指数形式的不
3) 放弃了乘法三元组形如
变量, 通过复用减少了 d +Θ(1) 个计数器, 突破因三元组形式带来的 3d 的计数器数量下界.

