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 clauseshortening approach proposed by Schuler [14]. The running time of the algorithm is O 2n(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 2n(1-1/ log(2m))

• Type: Journal
• Year: 2006
• Where: JSAT
• Authors: Evgeny Dantsin, Alexander Wolpert
• Keywords: Algorithm, Conjunctive Normal Form, JSAT 2006, Randomized Algorithm