A Faster Clause-Shortening Algorithm for SAT with No Restriction on Clause Length

We give a randomized algorithm for testing satisfiability of Boolean formulas in conjunctive normal form with no restriction on clause length. This algorithm uses the clause-shortening approach proposed by Schuler [14]. The running time of the algorithm is O ( 2 n ( 1 − 1 / α ) ) where α = ln ( m / n ) + 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 ( 2 m ) ) bound for SAT.