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  的计数器数量下界.
   23   24   25   26   27   28   29   30   31   32   33