TR03-072 Authors: Evgeny Dantsin, Edward Hirsch, Alexander Wolpert

Publication: 8th October 2003 15:18

Downloads: 2055

Keywords:

We 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.