一种求解命题公式骨干集的警示传播算法

A warning propagation algorithm for solving proposition formula backbones

警示传播WP算法是一类重要的信息传播算法,在命题公式的可满足性判定中非常有效。通过对WP算法的数学原理分析发现,当算法收敛时以高概率固定部分变元的赋值,可以对公式进行化简。基于这样的特征修改WP算法的迭代方程和变元赋值条件,设计了一种求解命题公式骨干集的信息传播算法。当变元数目超过400时,与经典骨干集求解算法对比,效率提高了40%,与目前常用算法对比也有10%的提高。结果表明,所提算法求解命题公式骨干集时非常有效。

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.