多文字可满足SAT问题的相变点上界

计算机工程与科学 ›› 2022, Vol. 44 ›› Issue (07): 1282-1290.

多文字可满足SAT问题的相变点上界

芦磊1,王晓峰1,2,梁晨1,张九龙1

(1.北方民族大学计算机科学与工程学院，宁夏银川 750021；
2.北方民族大学图像图形智能处理国家民委重点实验室，宁夏银川 750021)

收稿日期:2021-10-09 修回日期:2021-12-07 接受日期:2022-07-25 出版日期:2022-07-25 发布日期:2022-07-25
基金资助:
国家自然科学基金(62062001,61762019,61862051,61962002)；北方民族大学创新项目(YCX21083)；宁夏自然科学基金(2020AAC03214,2020AAC03219,2019AAC03120,2019AAC03119)

The upper bound of phase transition point of multi literal satisfiability problem

LU Lei1,WANG Xiao-feng1,2,LIANG Chen1,ZHANG Jiu-long1

(1.School of Computer Science and Engineering,North Minzu University,Yinchuan 750021;
2.The Key Laboratory of Images and Graphics Intelligent Processing of State Ethnic Affairs Commission,
North Minzu University,Yinchuan 750021,China)

Received:2021-10-09 Revised:2021-12-07 Accepted:2022-07-25 Online:2022-07-25 Published:2022-07-25

摘要/Abstract

摘要： 可满足（SAT）问题是指：是否存在一组布尔变元赋值，使得随机合取范式（CNF）公式中每个子句至少有1个文字为真。多文字可满足SAT问题是指：是否存在一组布尔变元赋值，使得随机CNF公式中每个子句至少有2个文字为真。此问题仍然是一个NP难问题。定义约束密度α为CNF公式子句数与变元数之比，对该问题的相变点上界α*进行了研究。如果α>α*，则多文字可满足SAT问题高概率不可满足。通过一阶矩一个简单的推断，可以证明α*=-ln 2/ln(1-(k+1)/2k)，当k=3时，α*=1。利用Kirousis等人的局部最大值技术，提升了多文字可满足3-SAT问题的相变点上界α*=0.7193。最后，选择了大量数据进行实验验证,结果表明，理论结果与实验结果相吻合。

关键词: 多文字可满足, SAT问题, 不满足阈值, 相变点上界, 合取范式

Abstract: The satisfiability problem (SAT) refers to whether there is a set of boolean variable assignments that make at least one literal in each clause of the conjunctive normal form (CNF) formula true. The multi literal SAT problem refers to whether there is a set of boolean variable assignments that make at least two literals in each clause of the CNF formula true. Obviously, this problem is still an NP difficult problem. Defining as the ratio of the number of clauses in the CNF formula to the number of variables, we study the upper bound α* of phase transition point of the problem. If α strictly exceeds α*, the multi literal satisfaction problem is almost certainly unsatisfiable. A simple inference of the first moment can be used to prove α*=-ln 2/ln1-(k+1)/2k. α*=1 when k=3. The local maximum technique proposed by Kirousis et al is used to improve the upper bound α* of phase transition point of the multi literal 3-SAT problem to 0.719 3. Finally, a large amount of data is selected for experimental verification, and the results show that the theoretical results are consistent with the experimental results.

Key words: multi literal satisfiability, satisfiability problem, unsatisfiability threshold, upper bound of phase transition point, CNF

芦磊, 王晓峰, 梁晨, 张九龙. 多文字可满足SAT问题的相变点上界[J]. 计算机工程与科学, 2022, 44(07): 1282-1290.

LU Lei, WANG Xiao-feng, LIANG Chen, ZHANG Jiu-long. The upper bound of phase transition point of multi literal satisfiability problem[J]. Computer Engineering & Science, 2022, 44(07): 1282-1290.

参考文献［3］

［1］	Cook S A.The complexity of theorem-proving procedures［C］∥Proc of the 3rd Annual ACM Symposium on Theory of Computing,1971:151-158.
［2］	Kaporis A C,Kirousis L M,Stamatiou Y C,et al.The unsat- isfiability threshold revisited［J］.Discrete Applied Mathematics,2007,155(12):81-95.
［3］	Xu Dao-yun. Applications of minimal unsatisfiable formulas to polynomially reduction for formulas［J］.Journal of Software,2006,17(5):1204-1212.(in Chinese)
［4］	Franco J,Paull M.Probabilistic analysis of the Davis Putnam procedure for solving the satisfiability problem［J］.Discrete Applied Mathematics,1983,5(1):77-87.
［5］	Mitchell D G,Selman B,Levesque H J.Hard and easy distributions of SAT problems［C］∥Proc of the 10th National Conference on Artificial Intelligence,1992:459-465.
［6］	Kamath A P,Motwani R,Palem K V,et al.Tail bounds for occupancy and the satisfiability threshold conjecture［J］.Random Structures & Algorithms,1994,7(1):59-80.
［7］	Dubois O,Boufkhad Y.A general upper bound for the satisfiability threshold of random r-SAT formulae［J］.Journal of Algorithms,1997,24(2):395-420.
［8］	Kirousis L M, Kranakis E,Krizanc D,et al.Approximating the unsatisfiability threshold of random formulas［J］.Random Structures & Algorithms,2015,12(3):253-269.
［9］	Dubois O,Boufkhad Y,Mandler J.Typical random 3-SAT formulae and the satisfiability threshold［J］.Electronic Colloquium on Computational Complexity,2003,10(7):1-2.
［10］	Dubois O.Upper bounds on the satisfiability threshold［J］.Theoretical Computer Science,2001,265(1-2):187-197.
［11］	Kirousis L M, Stamatiou Y C,Zito M.The unsatisfiability threshold conjecture:Techniques behind upper bound improvements［M］∥Computational Complexity and Statistical Physics.New York:Oxford University Press,2005.
［12］	Díaz J,Kirousis L,Mitsche D,et al.On the satisfiability threshold of formulas with three literals per clause［J］.Theo- retical Computer Science,2009,410(30-32):2920-2934.
［13］	Mézard M, Zecchina R. Random K-satisfiability problem:From an analytic solution to an efficient algorithm［J］.Physical Review E Statistical Nonlinear & Soft Matter Physics,2002,66(5):56-126.
［14］	Monasson R,Zecchina R.Statistical mechanics of the random K-SAT model［J］.Physical Review E Statistical Physics Plasmas Fluids & Related Interdisciplinary Topics,1996,56(2):1357-1370.
［15］	Achlioptas D,Chtcherba A D,Istrate G,et al.The phase transition in 1-i-nk SAT and NAE 3-SAT［C］∥Proc of the 12th Annual ACM-SIAM Symposium on Discrete Algorithms,2001:721-722.
［16］	Ding J, Sly A,Sun N.Satisfiability threshold for random regular NAE-SAT［J］.Communications in Mathematical Physics,2016,341(2):435-489.
［17］	Knysh S,Smelyanskiy V N,Morris R D.Approximating satisfiability transition by suppressing fluctuations［J］.arXiv:cond-mat/0403416,2004.
［18］	Kalapala V,Moore C.The phase transition in exact cover［J］.arXiv:cs/0508037,2005.
［19］	Moore C.The phase transition in random regular exact cover［J］.arXiv:1502.07591,2015.
［20］	Panagiotou K,Pasch M.Satisfiability thresholds for regular occupation problems［C］∥Proc of the 46th International Colloquium on Automata,Languages,and Programming,2019:1.
［21］	Béla B. Random graphs［M］.2nd Edition.Cambridge:Cambridge University Press,2001.
［22］	Kirousis L M,Stamatiou Y C.An inequality for reducible,increasing properties of randomly generated words［R］.Patras:Computer Technology Institute,University of Patras,1996.
［23］	Alon N,Spencer J H.The probabilistic method［M］.Manhattan:John Wiley & Sons,2004.
［24］	Janson S.New versions of Suen’s correlation inequality［J］.Random Structures & Algorithms,1998,13(3):467-483.
［25］	Suen W C S.A correlation inequality and a Poisson limit theorem for nonoverlapping balanced subgraphs of a random graph［J］.Random Structures & Algorithms,1990,1(2):231-242.
［26］	Knuth D E.The art of computer programming［M］.London:Pearson Education,1997.
［27］	Gasper G,Rahman M.Encyclopedia of mathematics and its applications［M］.Cambridge:Cambridge University Press,1990.
［28］	Kirousis L, Kranakis E,Krizanc D.An upper bound for a basic hypergeometric series:Technical Report TR-96-07［R］.Ottawa:School of Computer Science,Carleton University,1996.
［29］	Abramowitz M, Stegun I A.Handbook of mathematical function:with formulas,graphs,and mathematical tables［J］.American Journal of Physics,1998,56(10):958.
	附中文参考文献：
［3］	许道云.极小不可满足公式在多项式归约中的应用［J］.软件学报，2006,17(5):1204-1212.

[1]	王帅, 王晓峰, 梁田, 李志. 一种求解命题公式骨干集的警示传播算法[J]. 计算机工程与科学, 2021, 43(11): 2056-2061.
[2]	吴贯锋1,2，徐扬2,3,陈青山1,2,何星星2,3，常文静1,2. 基于频次的SAT问题学习子句混合评估算法[J]. 计算机工程与科学, 2019, 41(08): 1374-1380.
[3]	陈秀兰，刘婷. 基于动态奖惩的CDCL SAT求解器分支启发式算法[J]. 计算机工程与科学, 2019, 41(03): 490-497.
[4]	付慧敏1,2,徐扬2，何星星2,宁欣然1,2. 基于任务分配与调度的GSAT算法求解3-SAT问题[J]. 计算机工程与科学, 2018, 40(08): 1366-1374.
[5]	王晓峰,许道云,唐瑞雪. 基于DPLL的混合遗传算法求解SAT问题[J]. J4, 2010, 32(5): 54-56.
[6]	赵同昇[1] 朱文兴[2]. MAX—SAT问题一种改进的局部搜索算法[J]. J4, 2008, 30(11): 50-52.