ECCC-Report TR03-072https://eccc.weizmann.ac.il/report/2003/072Comments and Revisions published for TR03-072en-usWed, 08 Oct 2003 15:18:12 +0200
Paper TR03-072
| Algorithms for SAT based on search in Hamming balls |
Evgeny Dantsin,
Edward Hirsch,
Alexander Wolpert
https://eccc.weizmann.ac.il/report/2003/072We present a simple randomized algorithm for SAT and prove an upper
bound on its running time. Given a Boolean formula F in conjunctive
normal form, the algorithm finds a satisfying assignment for F
(if any) by repeating the following: Choose an assignment A at
random and search for a satisfying assignment inside a Hamming ball
around A (the radius of the ball depends on F). We show that this
algorithm solves SAT with a small probability of error in
at most 2^{n - 0.712\sqrt{n}} steps, where
n is the number of variables in F. We also derandomize this
algorithm using covering codes instead of random assignments. The
deterministic algorithm solves SAT in
at most 2^{n - 2\sqrt{n/\log_2 n}} steps.
To the best of our knowledge, this is the first non-trivial bound
for a deterministic SAT algorithm.
Wed, 08 Oct 2003 15:18:12 +0200https://eccc.weizmann.ac.il/report/2003/072