关键词: 警示传播算法, SAT问题, 因子图, 骨干集

Abstract: The Warning Propagation (WP) algorithm is an important type of message passing algorithm, which is very effective in judging the satisfiability of propositional formulas. Through the analysis of the mathematical principle of the WP algorithm, it is found that when the algorithm converges, the assignment of some arguments is fixed with high probability, so that the formula can be simplified. Based on such features, the iterative equations and argument assignment conditions of WP algorithm are modified, and a message passing algorithm for solving the backbones of propositional formulas is designed. When the number of variables exceeds 400, the proposal improves the efficiency by 40% in comparison to the classic backbone set solving algorithm ［18,20,22］, and by 10% in comparison to the current commonly used algorithm ［19,21］. The results show that this method is very effective in solving the backbones of proposition formulas.

Key words: warning propagation, satisfiability, factor graph, backbones