Behavior Analysis And Probability Control Strategy Of Local Search Algorithm For Solving SAT Problem

The propositional satisfiability problem is the first problem to be proved to beNP-Complete (Non-deterministic Polynomial Complete) by Steven Cook, and there is ofgreat significance in computer science theory and applications. For theory research, it isthe cornerstone of the computational complexity theory, and all of the NPC problems canbe reduced to SAT problem in polynomial time. For industrial applications, it can be usedto solve problems about equivalence checking, bounded model checking, electronicdesign automation, and statistical physics and so on. Thererfore, efficient and practicalalgorithms and techniques have been a hot research spot until now.Currently local search algorithms are very effective for solving SAT problem.Sattime is a typical local search algorithm, and has won a silver medal in the randomcategory in the2011SAT competition. It is based on Novelty family algorithms andexploits the satisfying history of clauses. The behavior analysis and pattern mining for itssolving process uncovered some causal relationships between variables and clauses. Weestablished a database to record local search behavior informations, and excuted datamining on flip event, including association rules mining and frequent sequences mining.Through analyzing the mining results, we found that Sattime sometimes selects the samevariable selected in the last step, which may cause loop back, and thus proposed twoprobability control strategies: strengthen strategy for choosing clauses and strengthenstrategy for choosing variables. Applying these two strategies into Sattime algorithm, wedesigned a new local search algorithm called Sattime-P.We used Sattime and Sattime-P to solve different types of instances, and comparedtheir average flipping numbers and average solving time. Experiment results showed thatSattime-P using improvement strategies has less average flipping numbers and betterefficiency than Sattime in most cases.