Survey Propagation Algorithm for SAT and Its Performance Dominated by Step Length
Ming Shao · Chinese Journal of Computers · 2005
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.