We give a randomized algorithm for testing satisfiability of Boolean formulas in conjunctive normal form with no restriction on clause length. Its running time is at most 2~(n(1-1/α)) up to a polynomial factor, where α = ln(m) + O(ln ln m) and n, m are respectively the number of variables and the number of clauses in the input formula. This bound is asymptotically better than the previously best known 2~(n(1-1/log(2m))) bound for SAT.
展开▼
