求解可满足问题的调查传播算法以及步长的影响规律

Survey Propagation Algorithm for SAT and Its Performance Dominated by Step Length

该文研究了求解可满足问题的调查传播算法.该算法利用合取范式因子图进行调查消息的迭代,并根据每一次迭代的收敛情况对部分布尔变量赋值以对问题进行简化,最后把简化的问题利用局部搜索算法来求解.文中所谓步长是指在每一次迭代收敛之后根据赋值倾向进行赋值的变量个数.该文根据模拟实验观察到步长对调查传播算法的影响规律,即随着步长的递增,算法的时间耗费以及算法的有效性都有近似单调递减的趋势.

This paper investigates an efficient algorithm for Boolean Satisfiability Problem (SAT), called Survey Propagation (SP). The SP algorithm was firstly published in the magazine of Science in August 2002, which has essential connections with statistical physics. This paper exploits it from the point of pure algorithm view. The SP algorithm considerably reduces the SAT instance by repeated iterations of survey messages on the factor graph of the Boolean formula in conjunctive normal form. In the end, the reduced problem is solved via local search algorithm called WalkSAT. By the step length it means the number of variables fixed according to the bias after each convergence of iteration. The paper studied how the parameter of step length influences the SP algorithm in two-folds, namely efficiency and validity. The efficiency is measured by the total time cost during solving the instances, and the validity of the algorithm is measured by the rate of the number of successfully solved instances. The detailed experiments, conducted on the random instances and the instances from benchmarks of SATLIB, reveals that the step length plays a dominated role. That is, with step length increasing, the efficiency and validity decreases nearly monotonously.