### Abstract

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 2^{n-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 language | English |
---|---|

Pages (from-to) | 141-151 |

Number of pages | 11 |

Journal | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |

Volume | 2996 |

Publication status | Published - 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

*Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)*,

*2996*, 141-151.