A more efficient satisfiability problem solver
Jon Feuss, Andrea F. Lobo · Journal of computing sciences in colleges · 2006
The Boolean Satisfiability problem (SAT) has been of great interest to researchers since being proven NP-Complete (Cook, 1971). The Boolean Satisfiability problem asks the question: Given a formula in conjunctive normal form, does there exist an assignment to a subset of the literals in the formula such that the formula evaluates to true? In recent years, many procedural advancements have been made to SAT solving algorithms, including powerful heuristics for selecting the next variable to be assigned, such as Jeroslow-Wang (Jeroslow, Wang, 1990) and VSIDS (Moskewicz, et. al. 2001). Heuristics play an important role in SAT solvers, as they can dramatically decrease their runtimes. Additionally, advanced clause learning techniques (Zhang, et. al., 2001) have been developed to avoid re-exploration of the search space that has been shown to contain no satisfying assignments.