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

王永平 等:取定 s 的严格 d-正则随机(3,2s)-SAT 问题的可满足临界 2639

择了 N=165,180,195,210.现在,以 s=30 为例,说明模拟实验如何进行.当 s=30 时,由表 1 可知,d 0 的数值解是
22.6038.为此,需分别取 d=0,2,…,22.当 s=30 时,对于任意的 N∈{165,180,195,210}和 d∈{0,2,…,22},我们按照如
下步骤进行一次实验.
Step 1. 设 k=3,用 SDRRK2S 模型生成 100 个实例.
Step 2. 使用 Zchaff 求解器 [12] 分别求解这 100 个实例.记求解器成功求解的实例总数是 n,并记不可满足
实例总数是 n u .
Step 3. 计算 n u /n 并记之为 r s .显然,r s 表示在成功求解实例中不可满足实例所占比例.
注意到:当 s=30 时,总共需要进行 4×12=48 次实验,而且在各次实验中,三元对(s,N,d)互不相同.为方便讨论,
记此 48 次实验中的任意一个是 E.设 F 是一个严格 d-正则随机(3,2s)-CNF 公式,其中,参数 s,N 以及 d 恰好是实
验 E 中三元对的各相应值,则实验 E 的 100 个实例可看作对公式 F 的 100 次模拟.进一步,实验 E 的 r s 可看作对
F 是不可满足的概率的模拟.这说明,我们的实验是合理的.
表 2~表 4 分别给出了 s=20,30,40 时的模拟实验结果,其中,11.8310,22.6038,34.3585 分别是 s=20,30,40 时 d 0
的数值解.由表 2 可知:当 s=20 时,对于任取的 d<11.8310 和 N∈{165,180,195,210},都有 r s =1.注意到,r s 可看作对
公式是不可满足的概率的模拟.因此,表 2 支持定理 3.同理,表 3 和表 4 也均支持定理 3.
Table 2 Values of r s when s=20 and d<11.8310
表 2 当 s=20 并且 d<11.8310 时的 r s 值
d 0 2 4 6 8 10
N=165 1 1 1 1 1 1
N=180 1 1 1 1 1 1
N=195 1 1 1 1 1 1
N=210 1 1 1 1 1 1

Table 3 Values of r s when s=30 and d<22.6038
表 3 当 s=30 并且 d<22.6038 时的 r s 值
d 0 2 4 6 8 10 12 14 16 18 20 22
N=165 1 1 1 1 1 1 1 1 1 1 1 1
N=180 1 1 1 1 1 1 1 1 1 1 1 1
N=195 1 1 1 1 1 1 1 1 1 1 1 1
N=210 1 1 1 1 1 1 1 1 1 1 1 1
Table 4 Values of r s when s=40 and d<34.3585
表 4 当 s=40 并且 d<34.3585 时的 r s 值
d 0 2 4 6 8 10 12 14 16 18 20 22 24 26 28 30 32 34
N=165 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1
N=180 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1
N=195 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1
N=210 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1
此外,同表 2~表 4 中各个 r s 均等于 1 一样,当 s=50,60 时,模拟实验结果也均为 r s =1(为节约篇幅,我们没有展
示这些结果).因此,s=50,60 时的模拟实验结果也均支持定理 3.综上,模拟实验结果验证了理论证明所得下界的
正确性.
注意到:在上述模拟实验中,各个 r s 均等于 1.这说明定理 3 所得下界仍然比较粗糙,需要进一步改进.

4 结 论

基于严格正则(k,2s)-CNF 公式,我们提出了每个变量正负出现次数之差的绝对值均为 d 的严格 d-正则
(k,2s)-CNF 公式.我们使用了新提出的 SDRRK2S 模型生成严格 d-正则随机(k,2s)-CNF 公式.初步进行的模拟实
验表明:当整数 5<s<11 取定时,参数 d 不仅与严格 d-正则随机(3,2s)-CNF 公式是否可满足有关,还与求解该类公
式的难度有关.因此,立足于 3-CNF 公式的随机难解实例生成,我们研究了严格 d-正则随机(3,2s)-SAT 问题在 s