The Study Of Random 3-SAT Algorithm In Propositional Logic

Satisfiability (SAT) problem is the first NP-complete problem proposed by Stephen Cook in 1971. As an important issue in computer science, SAT has been widely applied to various fields, such as artificial intelligence, software engineering, VLSI integrated circuit design, etc.3-SAT problem is a kind of clause set in which the number of the literals in each clause is fixed at 3. As a sub-problem of SAT Problem,3-SAT problem is also a kind of NP complete problems. While some 3-SAT problems are practical ones produced in the procedure of industrial transformation, another kind of problems are the generated automatically by machines. The practical ones cannot meet the demand of the test of all kinds of SAT algorithm. Actually, most of the 3-SAT problems fall into the latter category, i.e., random 3-SAT problems. Random 3-SAT problems are hard to solve, especially when the number of variables grows to 1000 or even to 1 million. Therefore, it has been an active field to efficiently solve such large-scale random 3-SAT problems. Since random 3-SAT problem has been proposed in the 1980s, many researchers had made great efforts during the past decades, and proposed a variety of algorithms, such as Sparrow2011, ProbSAT, CCMC and so on. However, they are not efficient enough to deal with the problems with huge number of variables.Based on the comprehensive analysis of disadvantages of the previous algorithms, this work makes several contributions to improve the efficiency of solving large-scale random 3-SAT problems, they are listed as following:1. It concentrates on the structure of SAT problem, analyses the frequency of the occurrence of the literals appear in the clause set and build up the potential relationship between the literals and the judgment of the satisfiability of the clause sets. Furthermore, it provides some important definitions of key degree of the literals and the key literal. Finally, it proposes an optimization method of the initial truth assignment to the clause sets based on the key literal rule and the DPLL rules.2. It proposes a new algorithm called WASAT. The method is employed with an evaluation function, which could help to search a better assignment in each epoch. With an initial assignment and a clause re-weighting strategy, the algorithm therefore has the ability to jump out of the local optimum solution.3. Experiments on open data sets indicate that the proposed algorithm outperformed the three baselines algorithms:Sparrow2011, ProbSAT, and CCMC.