Based On Set Theory Sat Algorithm Design And Implementation

SAT is not only a classical problem of theoretical computer science, but also the first NP complete problem which has been discovered. The SAT problem is a set of solutions that make"TRUE"for a Boolean logical expression, which must give a solution if the situation of the problem is satisfied; and prove the situation when the problem is unsatisfiable. Comparison of well-known program, efficient SAT solutions are MiNiSat, zchaff, Grasp, etc. The SAT solution algorithm is widely applied in each kind of domain of the practical life, such as formal verification of circuit design, artificial intelligence, resources scheduling and so on. Although the SAT solution algorithm research has been quite sophisticated already, it's still a bottleneck to be broken in the practical application domain. For example, in the Formal Verification of circuit design, transforms the circuit variables into Boolean logic form Conjunctive Normal Form (CNF), and examines the electric circuit breakdown using the SAT solution, the traditional algorithm often takes a quite long time and the massive memories, even more we could not obtain the satisfying results afterall. Therefore, the numerous domestic and foreign scholars still have been emerging continuely to promote the new algorithm to raise the counting, in order to apply highly effective performance in the various trades and occupations.Although propositional logic's fundamental research was quite mature, the SAT problem and its algorithm has been increasingly applied actually today, however, the propositional logic and the related algorithm is still a rousing direction. Generally the SAT solution can be divided into two kinds: complete algorithm and incomplete algorithm, their typical representative is Davis-Putnam proposes based on the recollection search (DPLL algorithm) and the local heuristic search. Now the popular SAT algorithm is mainly the complete algorithm or the DPLL algorithm and improved.This thesis based on foundation of existing SAT question and related theories research as well as algorithmic analysis, proposed one new kind of SAT algorithm based on the DPLL algorithm and set theory, has the highly effective estimated performance and good memory occupied. Critical mechanisms includ set division of Boolean variable, branch decision-making strategy, improved BCP process, conflict detected mechanism and recollection mechanism.In this topic, the author participated in the topic of theoretical research and analysis work, and under the guidance of teachers at the completion of the overall algorithm design, and has carried on the algorithm, contrast test and applied the algorithm in the actual area.