Standard

Algorithms for SAT based on search in hamming balls. / Dantsin, Evgeny; Hirsch, Edward A.; Wolpert, Alexander.

In: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 2996, 01.12.2004, p. 141-151.

Research output: Contribution to journal › Article › peer-review

Harvard

Dantsin, E, Hirsch, EA & Wolpert, A 2004, 'Algorithms for SAT based on search in hamming balls', Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 2996, pp. 141-151.

APA

Dantsin, E., Hirsch, E. A., & Wolpert, A. (2004). Algorithms for SAT based on search in hamming balls. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2996, 141-151.

Vancouver

Dantsin E, Hirsch EA, Wolpert A. Algorithms for SAT based on search in hamming balls. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 2004 Dec 1;2996:141-151.

Author

Dantsin, Evgeny ; Hirsch, Edward A. ; Wolpert, Alexander. / Algorithms for SAT based on search in hamming balls. In: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 2004 ; Vol. 2996. pp. 141-151.

BibTeX

@article{24e4c607e67c4db6a9a41e34c5dafd96,
title = "Algorithms for SAT based on search in hamming balls",
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 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.",
author = "Evgeny Dantsin and Hirsch, {Edward A.} and Alexander Wolpert",
year = "2004",
month = dec,
day = "1",
language = "English",
volume = "2996",
pages = "141--151",
journal = "Lecture Notes in Computer Science",
issn = "0302-9743",
publisher = "Springer Nature",

}

RIS

TY - JOUR

T1 - Algorithms for SAT based on search in hamming balls

AU - Dantsin, Evgeny

AU - Hirsch, Edward A.

AU - Wolpert, Alexander

PY - 2004/12/1

Y1 - 2004/12/1

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

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

UR - http://www.scopus.com/inward/record.url?scp=26444523521&partnerID=8YFLogxK

M3 - Article

AN - SCOPUS:26444523521

VL - 2996

SP - 141

EP - 151

JO - Lecture Notes in Computer Science

JF - Lecture Notes in Computer Science

SN - 0302-9743

ER -

ID: 49828492