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

可满足(SAT)问题是指:是否存在一组布尔变元赋值,使得合取范式公式中每个子句至少有一个文字为真.多文字可满足SAT问题是指:是否存在一组布尔变元赋值,使得CNF公式中每个子句至少有两个文字为真.显然,此问题仍然是一个NP难问题.为了研究解决多文字可满足SAT问题的算法,引入随机实例产生模型,设计求解多文字可满足SAT问题的置信传播算法.最后,用实例模型产生了大量数据进行实验验证,结果表明:该算法求解多文字可满足SAT问题的性能优于其他启发式算法.

Belief propagation algorithm for solving multi literal satisfiability problem

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 difficult 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.