-
题名求解多文字可满足SAT问题的置信传播算法
被引量:1
- 1
-
-
作者
芦磊
王晓峰
牛鹏飞
刘子琳
-
机构
北方民族大学计算机科学与工程学院
北方民族大学图像图形智能处理国家民委重点实验室
-
出处
《计算机应用研究》
CSCD
北大核心
2021年第9期2710-2715,共6页
-
基金
国家自然科学基金资助项目(62062001,61762019,61862051,61962002)
北方民族大学重大专项(ZDZX201901)
宁夏自然科学基金资助项目(2020AAC03214,2020AAC03219,2019AAC03120,2019AAC03119)。
-
文摘
可满足(SAT)问题是指:是否存在一组布尔变元赋值,使得合取范式公式中每个子句至少有一个文字为真。多文字可满足SAT问题是指:是否存在一组布尔变元赋值,使得CNF公式中每个子句至少有两个文字为真。显然,此问题仍然是一个NP难问题。为了研究解决多文字可满足SAT问题的算法,引入随机实例产生模型,设计求解多文字可满足SAT问题的置信传播算法。最后,用实例模型产生了大量数据进行实验验证,结果表明:该算法求解多文字可满足SAT问题的性能优于其他启发式算法。
-
关键词
多文字可满足
置信传播算法
WalkSAT算法
可满足问题
-
Keywords
multi literal satisfiability
belief propagation algorithm
WalkSAT
satisfiability problem
-
分类号
TP301
[自动化与计算机技术—计算机系统结构]
-
-
题名多文字可满足SAT问题的相变点上界
- 2
-
-
作者
芦磊
王晓峰
梁晨
张九龙
-
机构
北方民族大学计算机科学与工程学院
北方民族大学图像图形智能处理国家民委重点实验室
-
出处
《计算机工程与科学》
CSCD
北大核心
2022年第7期1282-1290,共9页
-
基金
国家自然科学基金(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。最后,选择了大量数据进行实验验证,结果表明,理论结果与实验结果相吻合。
-
关键词
多文字可满足
SAT问题
不满足阈值
相变点上界
合取范式
-
Keywords
multi literal satisfiability
satisfiability problem
unsatisfiability threshold
upper bound of phase transition point
CNF
-
分类号
TP301
[自动化与计算机技术—计算机系统结构]
-