An algorithm for the satisfiability problem of formulas in conjunctive normal form

We consider the satisfiability problem on Boolean formulas in conjunctive normal form. We show that a satisfying assignment of a formula can be found in polynomial time with a success probability of 2(-n(1 - 1/(1 + logm))), where n and m are the number of variables and the number of clauses of the formula, respectively. If the number of clauses of the formulas is bounded by V for some constant c, this gives an expected run time of O(p(n) (.) 2(n(1-1/(1+c logn)))) for a polynomial p. (C) 2004 Elsevier Inc. All rights reserved.