Derandomization of Schuler’s Algorithm for SAT

Recently Schuler [17] presented a randomized algorithm that solves SAT in expected time at most $2^{n(1-1/{\rm log}_{2}(2m))}$ up to a polynomial factor, where n and m are, respectively, the number of variables and the number of clauses in the input formula. This bound is the best known upper bound for testing satisfiability of formulas in CNF with no restriction on clause length (for the case when m is not too large comparing to n). We derandomize this algorithm using deterministic k-SAT algorithms based on search in Hamming balls, and we prove that our deterministic algorithm has the same upper bound on the running time as Schuler’s randomized algorithm.