Improvement of Local Research in SAT Problem

Recently, local search methods for solving the SAT problem have attracted considerable attention because they are the best known approaches to several hard classes of satisfiability. In this paper, an efficient initial probability is presented, which can constrain the random initial assignment of variables in the local search method. Also discussed is how to use the initial probability to improve the current local search algorithms such as WSAT, NSAT, TSAT, SDF, etc.. The strategies are straightforward and intuitive, and are helpful for increasing the number of satisfied clauses at its beginning of local search, thus decreasing the number of flipping for finding a solution and making the local search process converge fast. For this method to be compared with the other current local algorithms, many general random 3-SAT problem instances, structured SAT problem instances in SATLIB and phase transition's SAT problem instances are tested. The actual experimental results indicate that the improved algorithms are more efficient than the current local search SAT solvers such as WSAT, and so on. Moreover, this method can also be applied to other related methods to improve their efficiency.