Page 8 - 《软件学报》2021年第9期

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

SAT 问题的 HARD-EASY 相变现象与 SAT-UNSAT 相变现象有着一定联系.例如:当 s=6 时,SAT-UNSAT 相变点
位于 d=2 与 d=4 之间(如图 1(b)所示),而 HARD-EASY 相变点位于 d=2 处(见图 2(b)).再如:当 s=10 时,SAT-UNSAT
相变点位于 d=8 与 d=10 之间(如图 1(c)所示),而 HARD-EASY 相变点位于 d=8 处(见图 2(c)).因此,在理论上研
究严格 d-正则随机(3,2s)-SAT 问题在 s 取定时的 SAT-UNSAT 相变现象有助于 3-CNF 公式的随机难解实例生
成.在本文中,我们借鉴已有做法 [13] ,通过构造一个特殊随机实验和使用一阶矩方法给出了严格 d-正则随机
(3,2s)- SAT 问题在 s 取定时可满足临界值的一个下界.模拟实验结果验证了理论证明所得下界的正确性.
1 SDRRK2S 模型

2005 年,Boufkhad 等人 [17] 提出了一种不同于均匀 k-SAT 模型的新模型来生成具有 N 个变量和αN 个子句
的随机 k-CNF 公式.显然,该模型所生成公式的子句数与变量数的比值恰好是α.在该模型生成公式时,每个变量
⎢ kα ⎥ kα ⎢ kα ⎥ ⎢ kα ⎥
对应的两个文字均以概率 p = ⎢ ⎥ + 1− 出现 ⎢ ⎥ 次,以概率 1−p 出现 ⎢ ⎥ + 1次.这说明,每个变量出现次
⎣ 2 ⎦ 2 ⎣ 2 ⎦ ⎣ 2 ⎦
数的期望值均为 kα.因此,文献[17]所讨论的公式已经非常接近正则的 k-CNF 公式.记文字多重集{x 1 ,…,x 1 ,
¬x 1 ,…,¬x 1 ,x 2 ,…,x 2 ,¬x 2 ,…,¬x 2 ,…,x N ,…,x N ,¬x N ,…,¬x N }为 L,其中,对于每一个 i∈[N]={1,2,…,N},x i 与¬x i 的个数都
⎢ kα ⎥ ⎢ kα ⎥ ||L
是 ⎢ ⎥ 或 ⎢ ⎥ + 1.文献[17]的模型先均匀地将集合 L 划分成 个部分,使得每个部分均包含 k 个文字(在本
⎣ 2 ⎦ ⎣ 2 ⎦ k
||L
文中,符号|⋅|总表示某个集合的元素个数);然后,通过将 个部分各自构成子句来得到一个随机公式.文献[17]
k
的模拟实验(使用了文献[3]提出的贪心算法)表明:所生成的公式存在 SAT-UNSAT 相变现象,而且当 k=3 时,难解
实例集中在α=3.5 附近.这说明,文献[17]的模型有助于 3-CNF 公式的随机难解实例生成.此外,文献[17]还分别使
用一阶矩方法和文献[3]提出的贪心算法证明了:当 k=3 并且α>3.7822 时,所生成的公式是高概率不可满足的;
而当 k=3 并且α<2.46 时,所生成的公式是高概率可满足的.随后,Rathi 等人 [18] 通过在文献[17]的模型上增加一个
限制条件来生成随机 k-CNF 公式.该条件要求每个变量对应的两个文字具有相同的出现次数.在文献[18]中,
Rathi 等人分别使用一阶矩方法和二阶矩方法证明了:当 k=3 并且α>3.7822 时,所生成的公式是高概率不可满足
的;而当 k=3 并且α<2.667 时,所生成的公式是高概率可满足的.
如果在一个子句中,每个变量至多出现一次,则称该子句是合法子句;否则是非法子句.一个格局公式 [17] 可
能包含非法子句.文献[17,18]的模型生成的是格局公式.当一个格局公式不包含非法子句时,称之为简单公式.周
锦程等人 [11] 提出了一个模型来生成不包含重复子句的简单正则随机(3,s)-CNF 公式.在文献[11]的模型生成公
式时:若 s 是偶数,则每个变量对应的两个文字均出现 s/2 次;若 s 是奇数,则每个变量均出现 s 次,但以相等的概
s + 1 s − 1
率正出现 或 次.表面上,文献[11]的模型由文字多重集(见文献[17]的相应叙述)得到随机公式的方式
2 2
与文献[17]的情形有很大的不同,但二者本质上是相同的,只不过文献[11]的模型除去了不是简单公式或包含重
复子句的实例.文献[11]的模拟实验(使用 Zchaff 求解器 [12] )表明:所生成的公式存在 SAT-UNSAT 相变现象,而且
难解实例集中在 s=11 附近(即比值α=3.667 附近).这说明文献[11]的模型虽然不同于文献[17]的模型,但仍然有
助于 3-CNF 公式的随机难解实例生成.文献[11]还使用一阶矩方法证明了:当 s>11 时,所生成的公式是高概率不
可满足的.此外,由于所生成的公式是简单公式而且不包含重复子句,文献[11]的模型不太容易生成公式实例.因
此,在文献[13]中,周锦程等人放弃了简单公式以及不包含重复子句的限制,修改了文献[17]的模型以生成正则
随机(k,2s)-CNF 公式.在文献[13]的模型生成公式时,每个变量对应的两个文字均出现 s 次,从而每个变量均出现
2s 次.本质上,文献[13]的模型是通过均匀地选择文字多重集(见文献[17]的相应叙述)的一个置换来得到一个随
机公式的,从而得到的也是格局公式.在文献[13]中,周锦程等人通过构造一个特殊随机实验,并结合一阶矩方法
证明了:当 k=3 并且比值α>3.7822 时,所生成的公式是高概率不可满足的.此外,当 k 较大时,周锦程等人 [15] 利用
一阶复本对称破缺理论并结合一阶矩方法改进了文献[13]的结果.
SDRRK2S 模型用来生成严格 d-正则随机(k,2s)-CNF 公式.注意到:在一个严格 d-正则(k,2s)-CNF 公式中,