Hybrid Approach to Solve SAT and UNSAT Problems

Abstract

This work involves the construction of a hybrid approach to solve SAT and UNSAT problems. The solution combines techniques found in Stalmarck and DPLL algorithms for solving propositional satisfiability problems. We extend the Stalmarck rules in order to reduce computational cost during the deduction phase. We applied our solution to SAT and UNSAT instances. From the results it was found that this approach showed good results for UNSAT industrial instances. In some cases, our approach obtained gains of 45% to 60% in terms of efficient when compared to existing approaches. We compared our solution against the best known SAT solvers such as ZChaff and RSat.  The techniques and methods involved are described in the article.