TR04-017 Authors: Evgeny Dantsin, Alexander Wolpert

Publication: 8th March 2004 12:09

Downloads: 2473

Keywords:

Recently Schuler \cite{Sch03} presented a randomized algorithm that

solves SAT in expected time at most $2^{n(1-1/\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.