Study On SAT Solving Algorithm Based On Clause Weight

The propositional satisfiability problem(SAT problem)is the kernel problem in the field of mathematical logic,computer science,design and verification of integrated circuit,and artificial intelligence.For a long time,the solution of the SAT problem has been studied deeply,and many algorithms of solving the SAT problem have been put forward,one of the most popular is the CDCL algorithm.Based on the CDCL algorithm,there are a lot of solvers developed,such as:Chaff,zChaff,Minisat,Glucose,Lingeling and so on.These solvers connected with many algorithms,such as CDCL solver,which are constructed decision-making process,conflict analysis,clause learning and backtracking.In this paper,we put emphasis on decision-making process to study.We try and take into account the length of the clause,and then we use a lot method to make many short clauses to be satisfied,the purpose is to improve the efficiency of the algorithm to solve the SAT problem.Based on the CDCL algorithm framework,using the heuristic information,analyzing of static information about the structure of the clause,there are several aspects of the research work:1.Due to the length of the clause,it has a great influence to the process of variable selection.We considered the length of the clause in clause set,and the number of variable occurrences,we defined the average length of variables in clause set and give some relevant properties;then we combined with average length in clause set and the number of variable occurrences,and given variable weight function.Then we designed a new initial variable selection algorithm.2.In order to be able to say a short clause in the decision-making process influence,we combine with the principle of short clause to satisfy and the length of the clause,clause weight join VSIDS variable selection strategy,design a new variable selection strategy.3.Based on the initial variables selection strategy and branching selection strategy,we introduce them into CDCL solver variables selection in the process and forming two new solvers for solving the SAT problem—VW-SAT solver and CW-SAT solver,and illustrate the effectiveness of the algorithm.