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

Abstract

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 $\mathit{O}\mathrm{(}{2}^{\mathit{n}\mathrm{(}1-1\mathrm{/}\mathit{\alpha }\mathrm{)}}\mathrm{)}$ where $\mathit{\alpha }=ln\mathrm{(}\mathit{m}\mathrm{/}\mathit{n}\mathrm{)}+\mathit{O}\mathrm{(}lnln\mathit{m}\mathrm{)}$ 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^{\mathit{n}\mathrm{(}1-1\mathrm{/}log\mathrm{(}2\mathit{m}\mathrm{)}\mathrm{)}}$ bound for SAT.