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

软件学报 ISSN 1000-9825, CODEN RUXUEW E-mail: jos@iscas.ac.cn
Journal of Software,2021,32(9):2629−2641 [doi: 10.13328/j.cnki.jos.006049] http://www.jos.org.cn
©中国科学院软件研究所版权所有. Tel: +86-10-62562563

∗
取定 s 的严格 d-正则随机(3,2s)-SAT 问题的可满足临界

1,2
王永平 , 许道云 1
1
(贵州大学 计算机科学与技术学院,贵州 贵阳 550025)
2 (贵州财经大学 数统学院,贵州 贵阳 550025)
通讯作者: 许道云, E-mail: dyxu@gzu.edu.cn

摘 要: 3-CNF 公式的随机难解实例生成对于揭示 3-SAT 问题的难解实质和设计满足性测试的有效算法有着重
要意义.对于整数 k>2 和 s>0,如果在一个 k-CNF 公式中每个变量正负出现次数均为 s,则称该公式是严格正则(k,2s)-
CNF 公式.受严格正则(k,2s)-CNF 公式的结构特征启发,提出每个变量正负出现次数之差的绝对值均为 d 的严格 d-
正则(k,2s)-CNF 公式,并使用新提出的 SDRRK2S 模型生成严格 d-正则随机(k,2s)-CNF 公式.取定整数 5<s<11,模拟
实验显示,严格d-正则随机(3,2s)-SAT问题存在 SAT-UNSAT相变现象和HARD-EASY相变现象.因此,立足于3-CNF
公式的随机难解实例生成,研究了严格 d-正则随机(3,2s)-SAT 问题在 s 取定时的可满足临界.通过构造一个特殊随机
实验和使用一阶矩方法,得到了严格 d-正则随机(3,2s)-SAT 问题在 s 取定时可满足临界值的一个下界.模拟实验结果
验证了理论证明所得下界的正确性.
关键词: 3-CNF 公式;随机难解实例生成;正则子类;严格 d-正则随机(3,2s)-SAT 问题;可满足临界
中图法分类号: TP301

中文引用格式: 王永平,许道云.取定 s 的严格 d-正则随机(3,2s)-SAT 问题的可满足临界.软件学报,2021,32(9):2629−2641.
http://www.jos.org.cn/1000-9825/6049.htm
英文引用格式: Wang YP, Xu DY. Satisfiability threshold of strictly d-regular random (3,2s)-SAT problem for fixed s. Ruan Jian
Xue Bao/Journal of Software, 2021,32(9):2629−2641 (in Chinese). http://www.jos.org.cn/1000-9825/6049.htm

Satisfiability Threshold of Strictly d-regular Random (3,2s)-SAT Problem for Fixed s
1,2
WANG Yong-Ping , XU Dao-Yun 1
1
(College of Computer Science and Technology, Guizhou University, Guiyang 550025, China)
2
(School of Mathematics and Statistics, Guizhou University of Finance and Economics, Guiyang 550025, China)
Abstract: Generating random hard instances of the 3-CNF formula is an important factor in revealing the intractability of the 3-SAT
problem and designing effective algorithms for satisfiability testing. Let k>2 and s>0 be integers, a k-CNF formula is a strictly regular
(k,2s)-CNF one if the positive and negative occurrence number of every variable in the formula are s. On the basis of the strictly regular
(k,2s)-CNF formula, the strictly d-regular (k,2s)-CNF formula is proposed in which the absolute value of the difference between positive
and negative occurrence number of every variable is d. A novel model is constructed to generate the strictly d-regular random (k,2s)-CNF
formula. The simulated experiments show that the strictly d-regular random (3,2s)-SAT problem has an SAT-UNSAT phase transition and
a HARD-EASY phase transition when the parameter 5<s<11 is fixed, and that the latter is related to the former. Hence, the satisfiability
threshold of the strictly d-regular random (3,2s)-SAT problem is studied when the parameter s is fixed. A lower bound of the satisfiability
threshold is obtained by constructing a random experiment and using the first moment method. The subsequent simulated experiments
verify well the lower bound proved.
Key words: 3-CNF formula; generating random hard instances; subclass with regular structure; strictly d-regular random (3,2s)-SAT
problem; satisfiability threshold

∗ 基金项目: 国家自然科学基金(61762019, 61862051)
Foundation item: National Natural Science Foundation of China (61762019, 61862051)
收稿时间: 2019-03-22; 修改时间: 2019-11-28; 采用时间: 2020-04-03; jos 在线出版时间: 2020-05-26