ECCC-Report TR04-017https://eccc.weizmann.ac.il/report/2004/017Comments and Revisions published for TR04-017en-usMon, 08 Mar 2004 12:09:12 +0200
Paper TR04-017
| Derandomization of Schuler's Algorithm for SAT |
Evgeny Dantsin,
Alexander Wolpert
https://eccc.weizmann.ac.il/report/2004/017Recently 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.
Mon, 08 Mar 2004 12:09:12 +0200https://eccc.weizmann.ac.il/report/2004/017