Algorithms for SAT based on search in hamming balls

Evgeny Dantsin, Edward A. Hirsch, Alexander Wolpert

Research output

16 Citations (Scopus)


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 2 n-2√n/log2n 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.

Original languageEnglish
Pages (from-to)141-151
Number of pages11
JournalLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Publication statusPublished - 1 Dec 2004

Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Algorithms for SAT based on search in hamming balls'. Together they form a unique fingerprint.

  • Cite this