Based On The Clause, The Right To Re-solve The Sat Problem

SAT problem was studied a lot in the area of the Electronic Design Automation (EDA), as well as in Artificial Intelligence (AI), because it has been widely used. People have done deeply research about this problem for a long time, and a lot of algorithms have been developed. DPLL is the most popular one, and based on the idea of DPLL, a lot of sat solvers were implemented. ZCHAFF is one of the most effective SAT solver. In this paper, we gave an introduction about the applications, the traditional algorithms, and the most popular solvers of the SAT problem, and did a deeply research for the decision strategy of the DPLL algorithm. We took into account for the fact that the depths of the clauses are different in some CNF formulas, and weighted the different depth clauses to improve the decision strategy. The experimental result showed that for the CNF problem which has different depth of clauses, this new strategy can improve the performance of the solver effectively. For some cases, the solver based on clause weight can get hundreds times runtime speedup than ZCHAFF, and it even can solve some problems that ZCHAFF can not so far.