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

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

作　　者：芦磊 王晓峰[1,2] 梁晨 张九龙 LU Lei;WANG Xiao-feng;LIANG Chen;ZHANG Jiu-long(School of Computer Science and Engineering,North Minzu University,Yinchuan 750021;The Key Laboratory of Images and Graphics Intelligent Processing of State Ethnic Affairs Commission,North Minzu University,Yinchuan 750021,China)

机构地区：[1]北方民族大学计算机科学与工程学院,宁夏银川750021 [2]北方民族大学图像图形智能处理国家民委重点实验室,宁夏银川750021

出　　处：《计算机工程与科学》2022年第7期1282-1290,共9页Computer Engineering & Science

基　　金：国家自然科学基金(62062001,61762019,61862051,61962002);北方民族大学创新项目(YCX21083);宁夏自然科学基金(2020AAC03214,2020AAC03219,2019AAC03120,2019AAC03119)。

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

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

分 类 号：TP301[自动化与计算机技术—计算机系统结构]