求解多文字可满足SAT问题的置信传播算法  

Belief propagation algorithm for solving multi literal satisfiability problem

作　　者：芦磊 王晓峰[1,2] 牛鹏飞 刘子琳 Lu Lei;Wang Xiaofeng;Niu Pengfei;Liu Zilin(College of Computer Science&Engineering,Yinchuan 750021,China;Key Laboratory of Images&Graphics Intelligent Processing of State Ethnic Affairs Commission,Yinchuan 750021,China)

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

出　　处：《计算机应用研究》2021年第9期2710-2715,共6页Application Research of Computers

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

摘　　要：可满足(SAT)问题是指:是否存在一组布尔变元赋值,使得合取范式公式中每个子句至少有一个文字为真。多文字可满足SAT问题是指:是否存在一组布尔变元赋值,使得CNF公式中每个子句至少有两个文字为真。显然,此问题仍然是一个NP难问题。为了研究解决多文字可满足SAT问题的算法,引入随机实例产生模型,设计求解多文字可满足SAT问题的置信传播算法。最后,用实例模型产生了大量数据进行实验验证,结果表明:该算法求解多文字可满足SAT问题的性能优于其他启发式算法。The SAT problem refers to whether there is a set of Boolean variable assignments that makes at least one literal in each clause of the CNF formula true.The multi literal SAT problem refers to whether there is a set of Boolean variable assignments that makes at least two literals in each clause of the CNF formula true.Obviously,this problem is still an NP-hard problem.In order to study the algorithm to solve the multi literal SAT problem,this paper introduced a random example generation model,and designed a belief propagation algorithm to solve the multi literal SAT problem.Finally,it generated a large amount of data by the example model for experimental verification,and the results show that the performance of this algorithm for solving literal SAT problem is better than other heuristic algorithms.

关 键 词：多文字可满足 置信传播算法 WalkSAT算法 可满足问题 

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