A Faster Clause-Shortening Algorithm for SAT with No Restriction on Clause Length
Evgeny Dantsin, Alexander Wolpert · Journal on Satisfiability Boolean Modeling and Computation · 2005
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 algori