Warning Propagation Algorithm For The Regular(3,4)-SAT Problem

Based on the critical characterization of the minimal unsatisfiable formula,a 3-CNF formula can be reduced to a regular(3,4)-CNF formula within polynomial time.Thus the regular(3,4)-SAT problem is NP-complete.The Warning propagation(WP)algorithm converges in high probability on the regular(3,4)-SAT instance sets by reducing,however,if the instances are satisfiable,it hardly finds a satisfying assignment efficiently.So WP algorithm fails to solve the reduced regular(3,4)-SAT problem.In this thesis,in order to solve the problem that WP algorithm hardly to solve the satisfiable reduced regular(3,4)-SAT instance sets,we proposed a modified strategy for the WP algorithm which based on the structure feature of the reduced regular(3,4)-CNF formula.We also introduced the definition of WP-solvable formula,which combined the information propagation mechanism of the WP algorithm and the concept of backbone set and backdoor set,and the convergence of WP algorithm on the WPsolvable formula are studied.The main results are as follows:(1)There are three changes of the formula structural feature between the reduced regular(3,4)-CNF formula and the original 3-CNF formula: First,the positive and negative occurrences of each variable has been found to be stable in the reduced regular(3,4)-CNF formula.Second,each variable in the reduced regular(3,4)-CNF formula is included in at least two circles.Third,consider a reduced regular(3,4)-CNF formula F is satisfiable,that F must have a backbone set,and the size of backbone set is at least 9m(m is the number of clauses of the original 3-CNF formula).(2)In the experiment of WP algorithm for random 3-SAT problem,we found that the WP-algorithm converges to trivial fixed points with high probability with the constraint density increases,which means that the algorithm assigns a variable values with a random select in the initial iteration step.This has an impact on the performance of the algorithm for SAT problem.Therefore,a strategy based on the maximum polarity variable was proposed to improve the WP algorithm.The experimental results show that the improved WP algorithm is better than the original algorithm.(3)For the problem that the WP algorithm hardly to solve the satisfiable reduced regular(3,4)-SAT instance sets,a modification strategy of the WP algorithm based on the structure feature of positive and negative occurrences of the reduced regular(3,4)-CNF formula was proposed.The experimental results show that the modified WP algorithm can effectively solve the reduced regular(3,4)-SAT instance sets.(4)We proved that the tree formulas are also WP-solvable.Furthermore,based on the planted distribution model,we proved that the WP algorithm has a high probability of convergence on a 3-CNF formula if the formula is WP-solvable.