You are viewing a javascript disabled version of the site. Please enable Javascript for this site to function properly.
Go to headerGo to navigationGo to searchGo to contentsGo to footer
In content section. Select this link to jump to navigation

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(2n(11/α)) where α=ln(m/n)+O(lnlnm) 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(11/log(2m)) bound for SAT.