AN EFFICIENT ALGORITHM FOR THE 3-SATISFIABILITY PROBLEM

Among many different ways, the satisfiability problem (SAT) can be stated as the resolution of a boolean equation f(x) = 0. This equation can be solved by computing the complete prime basis of f by a consensus method. This type of method for solving SAT has been known for a long time but it has not led to efficient algorithms. More recently some authors have proposed practical algorithms for solving the satisfiability problem based on the Davis and Putnam scheme in which the unit consensus operation is an important feature. In this paper we present an efficient implicit enumeration algorithm which also uses the notion of consensus but which can be viewed as a compromise between the computation of the complete prime basis of a boolean function f and the Davis and Putnam scheme. This algorithm is favorably compared with an efficient implementation of the Davis and Putnam scheme on randomly generated 3-satisfiability instances with 100, 200 and 300 variables.