Statistical Analysis And Behavior Loop Control Strategy Of Local Search Based On TNM Algorithm For Solving SAT Problem

The propositional satisfiability problem is the first problem to be proved to be NP-Complete(Non-deterministic Polynomial Complete) by Steven Cook. It is the cornerstone of the computational complexity theory and is an important issue in the region of computer science and artificial intelligence. For industrial applications, it can be widely used to solve problems about mechanical theorem proving, the design and test of VLSI, security protocol verification, and planning and scheduling and so on. Thererfore, it is of great importance to make scientific researches on efficient and practical algorithms for solving the satisfiability problem.The algorithms of solving the SAT problem fall into two camps: complete algorithms and incomplete algorithms. Compared to complete algorithms, incomplete algorithms can solve the larger scale instance of SAT problem in a shorter amount of time but there is no guarantee that an existing solution is eventually found. To date, stochastic local search methods are the most powerful and successful methods among the incomplete algorithms which easily get stuck in local minima. TNM is a typical stochastic local search algorithm. It uses the history of the most recent consecutive falsifications of a clause due to the flipping of one variable in this clause. We established a database to record local search behavior information, and executed statistical analysis on flip event. Through analyzing the results, we found that TNM sometimes visit the same location within the search space more than once, which may cause behavior cycle, and thus proposed a control strategy to escape from the behavior loop. Applying this strategy into TNM algorithm, we designed a new local search algorithm called TNM+.TNM and TNM+ were used to solve different types of instances, and compared their average flipping numbers and average solving time. Experiment results showed that TNM+ using improvement strategy has less average flipping numbers and better efficiency than TNM in most cases.