Study On SAT Sloving Algorithm Based On CDCL

The satisfiability (SAT) problem propositional of logic formulas plays a very important role artificial intelligence. With the development of artificial intelligence field, the SAT problem need to be solved become larger, but traditional algorithms can not adapt to large-scale SAT problem. Therefore, some solvers for large-scale SAT problem came into being, such as Chaff, zChaff, minisat, Lingeling and many other famous solvers. These solvers do not only include a single algorithm, but also construct on the traditional DPLL algorithms on a system, which connected with a group algorithms, such as CDCL solver, which is constructed decision-making process, conflict analysis, clause learning and backtracking. Because of decision-making process of variable has a very important position in the algorithm framework, a good policy of variable decision can reduce the number of conflicts and save a lot of time. Therefore the policy decision-making process of variable study has more important significance. In the paper, to combine with CDCL solver structure do the research work of the following aspects.1. The article puts forward an heuristic strategy that based on the number of the occurrence of the clause and literal, and give the definition of correlation on the literal and the clause, and also give the definition of the correlation between the clause and the clause set, then give the strategy of heuristic about the beginning clause decision.2. To give the definition of conflict status which is based on the correlation definition, and get the theory of conflict status stable that make use of the condition about the number of conflicts reducing with giving the assignment of variable. Therefore, to connect the stable conflict status with CDCL structure to get the new conflict-SAT algorithm.3. The article uses the 2013 and 2014 SAT competition instance to test the new algorithm, and compare the testing result with the other formulas solvers, and also test the new algorithm by making use of the TPTP library instance about the TSP problem, then analysis the result and get conclusion.