A Class Of Sat Benchmark Algorithm And Its Applications

Propositional Satisfiability Problem (SAT) is a well known problem in computer science and artificial intelligence research. Many real-world problems can be transformed into SAT problems and many of these problem instances can be effectively solved via satisfiability. Hence, the research for fast and efficient SAT solvers is an important and useful topic. Satsifiability problems can come from many different sources, which lead to many different types of SAT benchmarks. The same SAT solver can perform differently on different types of benchmarks. People commonly believe these performance differences are due to intrinsic structural differences between various types of benchmarks. Based on such concept, the SATzilla software integrated many different SAT solving algorithms, and applies different algorithms to different types of satisfiability problems, and became one of the top winners in recent SAT competitions. Their experience suggests that development of targeted algorithms to solve specific types of SAT problems is potentially an important and effective strategy in SAT solver research. This paper design an efficient algorithm for one kind of benchmark that are structurally similar to benchmark generated from Model RB. The algorithm successfully used to solve the Graph Coloring Problem.There are two main kinds of SAT solvers: complete and incomplete solvers. Complete algorithm is different from the incomplete algorithm. It not only can guarantee find a model for a satisfiability problem, but also it can be used to prove that a problem is unsatisfiable. So that most of the SAT algorithms are complete algorithm. And many top rate SAT solvers are based on DPLL, such as zChaff, Rsat. This article is also based on DPLL framework to design algorithms.In this thesis, we study the satisfiability problems that are structurally similar to Model RB. The variable is divided into several groups. On this basis, the original problem is transformed into another problem. The new problem is find a set of variables form each groups, and these variables satisfy some condition. And then, we design wRBsat algorithm which is based on DPLL framework. The algorithm uses vector arrays to store data, the structure is advantage to access and manipulate data. When design the branch decision strategy, the process is divided into two steps: firstly, select the group index, this step will build a search tree; secondly, select a variable from the variable group which is selected in the first step, this step will decide the search path. This method keeps the algorithm is better to control the process of branch decision, thereby enhancing the efficiency of the algorithm. Computing framework of the algorithm make back-level is relatively small, and it is very convenient to save the historical data, so the efficiency of conflict analysis and backtracking process is very high.In this thesis, a large number of instances are used to test this algorithm, test results show that on this Benchmark wRBsat has higher efficiency. In addition, graph coloring problem is transformed into SAT problem; and then it can be use wRBsat to solve. Experimental results indicate the algorithm solve the Graph Coloring Problem is very successful.