Page 6 - 《软件学报》2021年第9期
P. 6

2630                                 Journal of Software  软件学报 Vol.32, No.9,  September 2021

             设 N 是正整数,x 1 ,x 2 ,…,x N 是布尔变量.对于任取的 x∈{x 1 ,x 2 ,…,x N },称¬x 和 x 为文字,其中,¬x 是 x 的否定.
         有限个文字的析取构成一个子句,而有限个子句的合取构成一个合取范式(conjunctive normal form,简称 CNF)
                                                         N
         公式.设 F 是一个 CNF 公式,如果存在一个真值指派σ∈{0,1} 使得 F 取值为真,则称 F 是可满足的,并称σ是 F
         的一个解.如果 F 没有解,则称 F 是不可满足的.例如,F=(x 1 ∨¬x 2 )∧(x 3 ∨¬x 4 ∨¬x 5 )是一个包含两个子句的 CNF 公
         式,而σ=(0,0,1,1,1)(这意味(x 1 ,x 2 ,x 3 ,x 4 ,x 5 )=(0,0,1,1,1))是 F 的一个解(这里,σ(¬x)=¬σ(x)).
             习惯地,将判定一个 CNF 公式是否可满足称为求解该公式.设整数 k>2,如果一个 CNF 公式的每个子句恰好
         包含 k 个文字,则称该公式是 k-CNF 公式.求解任意一个 k-CNF 公式的问题称为 k-SAT 问题.1973 年,Levin 证明
                                [1]
         了 3-SAT 问题是 NP-完全的 .这说明:如果 P≠NP,则 3-SAT 问题不存在多项式时间算法.因此,3-CNF 公式的随
         机难解实例生成,对于揭示 3-SAT 问题的难解实质和设计满足性测试的有效算法有着重要意义.
             均匀 k-SAT 模型用于生成具有 M 个子句和 N 个变量的随机 k-CNF 公式,其中,M 和 N 是正整数.该模型先
            k ⎛  N ⎞
         从 2  ⎜  ⎟  个可能的子句中均匀且相互独立地选取 M 个子句,而后将这些子句合取成一个 k-CNF 公式.设 F 是一
             ⎝  k  ⎠
         个随机 3-CNF 公式,其子句数 M 与变量数 N 的比值为α.1999 年,Friedgut 等人证明了随机 3-SAT 问题存在 SAT-
                       [2]
         UNSAT 相变现象 :存在一个变量数 N 的函数α 3 ,使得当α<α 3 时,随机 3-CNF 公式是高概率可满足的;而当α>α 3
         时,随机 3-CNF 公式是高概率不可满足的.虽然到目前为止还不知道α 3 的具体值,但文献[3,4]得到了 3.52≤α 3 ≤
         4.4898,而文献[5]基于一个单调性假设得到了α 3 ≤4.262.此外,模拟实验估计α 3 的值取得了较好的结果                      [6−9] :α 3 ≈
         4.267,并且随机 3-CNF 公式的难解实例集中在α=4.267 附近.综上,比值α不仅与随机 3-CNF 公式是否可满足有
         关,还与求解该类公式的难度有关.
             设 F 是一个 CNF 公式,x 是 F 的一个变量.称文字 x(¬x)在 F 中的出现次数是 x 在 F 中的正(负)出现次数,
         并称 x 在 F 中的正出现次数与负出现次数之和是 x 在 F 中的出现次数.设整数 s>0,如果在一个 k-CNF 公式中
         每个变量均出现 s 次,则称该公式是正则(k,s)-CNF 公式.文献[10]利用多项式归约技术证明了正则(3,4)-SAT 问
         题是 NP-完全的.这说明,存在难解的正则(3,4)-CNF 公式实例.文献[11]利用 Zchaff 求解器               [12] (该求解器是目前求
         解 3-CNF 公式最有效的完备求解器)进行的模拟实验表明:当每个变量正负出现次数之差的绝对值至多是 1 时,
         正则(3,s)-CNF 公式的随机难解实例集中在 s=11 附近,并且 s=11 时求解该类实例的难度远大于比值α=4.267 时
         求解随机 3-CNF 公式实例的难度.注意到,正则(3,s)-CNF 公式的子句数与变量数的比值恒为 s/3,因此,文献
         [10,11]的上述结论说明:当 s=4 或 11,即比值α=4/3 或 11/3 时,存在 3-CNF 公式的难解实例,只不过实例是正则的.
         受此启发,我们考虑了取定 s 时正则(3,s)-CNF 公式的随机难解实例生成问题.注意到:对于正则(3,s)-CNF 公式来
         说,s 取定意味着比值α≡s/3.因此,当 s 取定时,需要找到类似于比值α的新参数,使得该新参数不仅影响正则(3,s)-
         CNF 公式是否可满足,还影响求解该类公式的难度.文献[13−16]分别从 SAT-UNSAT 相变、解的个数等方面研
         究了严格正则(k,s)-CNF 公式,其中,s 是偶数,每个变量的正负出现次数均为 s/2.显然,在严格正则(k,s)-CNF 公式
         中,每个变量正负出现次数之差均为 0.结合文献[11,13−16],我们提出了每个变量正负出现次数之差的绝对值均
         为 d 的严格 d-正则(k,s)-CNF 公式.该类公式是正则(k,s)-CNF 公式的一个子类,而 d 是取定的非负整数.注意到:
         当 s 是偶数时,参数 d 的可能取值为 0,2,…,s;当 s 是奇数时,参数 d 的可能取值为 1,3,…,s.为方便讨论,在本文中,
         我们选择 s 是偶数的情形,即严格 d-正则(k,2r)-CNF 公式的情形,其中,r>0 是整数.为保持符号一致,我们将严格
         d-正则(k,2r)-CNF 公式仍表述为严格 d-正则(k,2s)-CNF 公式.
             类似于使用均匀 k-SAT 模型生成随机 k-CNF 公式,借鉴已有模型              [11,13,17,18] ,我们提出一个新的模型来生成严
         格 d-正则随机(k,2s)-CNF 公式.在这个模型生成公式时,先由 N 个变量得到 2Ns 个文字,其中,每个变量均出现 2s
                                     d     d
         次,并且均以相等的概率正出现 s +           或 s −  次;再从这 2Ns 个文字的置换全体中均匀地选择一个置换,并根据
                                     2     2
         该置换生成一个公式.为方便起见,称该模型是 SDRRK2S 模型.在下一节,我们将详细叙述这一模型.
             本文立足于 3-CNF 公式的随机难解实例生成.为此,我们通过模拟实验观察了 s 取定时,参数 d 与严格 d-正
         则随机(3,2s)-CNF 公式是否可满足及其求解难度的关系.我们分别选取了 s=1,2,…,10,并且对于每一个 s 值分别
   1   2   3   4   5   6   7   8   9   10   11