Research On Algorithm For Satisfiability Problem Based On 2-SAT Solver

Satisfiability (SAT) problem has been the core problem of research on computational theory. SAT is a classic NP-complete problem, and the quick solver to it is very important both in theory and in practice. Research on SAT has been applied widely to various fields, such as Electronic Design Automation, Artificial Intelligent and so on. In spite of its NPC property, the problem can be solved in polynomial time if the number of literals in a clause is limited to 2 (2-SAT). In this paper, we focus our research on using 2-SAT solver to improve the speed of SAT solver and introduce two new algorithms.We first introduce a concept called 2-SAT sub problem. And we realized that if SAT is satisfiable, it has a satisfiable 2-SAT sub problem, which means satisfiability can be proved through finding a satisfiable 2-SAT sub problem. Inspired by this fact, we introduce a new SAT solver based on finding satisfiable 2-SAT sub problem. The solver first constructs the 2-SAT problem randomly and applies the BinSat (2-SAT solver) to it. If the 2-SAT is not satisfiable, it adjusts the content of 2-SAT to make it more likely to be satisfiable. Experiments show that, the new SAT solver performs well on various problems and is a promising algorithm.Unit resolution used by DPLL style algorithms will reduce many clauses to 2 or less literals. If we apply BinSat to these newly deduced binary clauses we may detect more conflict quickly and thus yield more unit resolutions. However, we can not apply it directly, for the overhead is considerable. We improve BinSat and make it incremental, so that we don't repeat work unnecessary. We then introduce a new DPLL style SAT solver integrated with the incremental BinSat. Experiments show that, the SAT solver is competitive with SATO on problems involving substantial binary clauses.