Algorithms for SAT Based on Search in Hamming Balls

We present two simple algorithms for SAT and prove upper bounds on their running time. Given a Boolean formula F in conjunctive normal form, the first 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 2n−0.712 √ n steps, where n is the number of variables in F. To derandomize this algorithm, we use covering codes instead of random assignments. The deterministic algorithm solves SAT in at most 2n−2 √ n/ log2 n steps. To the best of our knowledge, this is the first non-trivial bound for a deterministic SAT algorithm with no restriction on clause length.

• Type: Conference
• Year: 2004
• Where: STACS
• Authors: Evgeny Dantsin, Edward A. Hirsch, Alexander Wolpert
• Keywords: Algorithm, Algorithm Solves Sat, Satisfying Assignment, STACS 2004, Theoretical Computer Science