计算机工程与科学

作者：芦磊, 王晓峰, 梁晨, 张九龙

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

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

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

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

来源：2022年第7期

《计算机工程与科学》期刊编辑部

查看计算机工程与科学杂志2022年第7期