Survey Propagation Algorithm In 3-SAT Problem Solving

Satisfiability problem (SAT) is given a Boolean function to decide whether there is some assignment to its variables making it true, or to determine that it is false. It is the first NP-complete proposed by Stephen Cook in 1971. SAT is an important issue in computer science and artificial intelligence and has a wide applications in software engineering, VLSI integrated circuit design. 3-SAT problem is that the SAT problems are represented as the expression of all CNF and each clause the number of variables is fixed at 3. 3-SAT has also been shown to be NP-complete. When the number of sentences / number of variables is greater than a certain threshold, 3-SAT problem becomes very difficult to solve, so large-scale 3-SAT is an active area of research. In the decades following, many scholars have done a lot of work in this area, proposed a variety of algorithms. There are mainly two classes of algorithms for solving instances of SAT in practice: the complete algorithm and stochastic local search algorithms.The most famousc omplete one is Davis, who proposed DPLL algorithm. A DPLL SAT solver employs a systematic backtracking search procedure to explore the space of variable assignments looking for satisfying assignments This algorithm is always able to determine whether this propositional formula is satisfiable, but its complexity is exponential, for the large-scale SAT problems or difficult to solve the SAT problems, the efficiency of this algorithm is very low, and can not be used practicallyStochastic local search methods are being used to solve SAT problems when there is no or limited knowledge of the specific structure of the problem instances to be solved, but such methods may not be able to determine the satisfiability of any formula. Many large-scale SAT problem can be solved quickly by this local search methods. Survey Propagation (SP) is a new algorithm for solving hard combinatorial problems. It was discovered by Mezard, Parisi, and Zecchina (2002), and is so far the only known method successful at solving random Boolean satisability (SAT) problems with 1 million variables and beyond in near-linear time in the hardest region. The SP method is quite radical in that it tries to approximate certain marginal probabilities related to the set of satisfying assignments. It then iteratively assigns values to variables with the most extreme probabilities. This thesis uses the chaos theory and new way of updating the message to speed up the sp algorithm. First, the initialization survey information is generated by the chaotic sequence instead of using random values. The drop in value is very stable, which is ensuring uniform initialization. By comparison of the actual discovery, a survey of the value of a more uniform initialization procedure can be effective in reducing the number of iterations and update. Second, there is a large number of redundant updates in original SP algorithm, so we use a new survey update mechanism which is used on the determination for an updated forecast, greatly reducing the unnecessary update calls. In actual operation it is clear that the optimized update calls by 40% -50%, the algorithm efficiency of 20% -30% a significant improvement.