@inproceedings{66665624c02b4729bd07ae8e503d565b,
title = "Local search algorithms for SAT: Worst-case analysis",
abstract = "Recent experiments demonstrated that local search algorithms (e.g. GSAT) are able to find satisfying assignments for many {"}hard{"} Boolean formulas. However, no non-trivial worst-case upper bounds were proved, although many such bounds of the form 2αn (α < 1 is a constant) are known for other SAT algorithms, e.g. resolution-like algorithms. In the present paper we prove such a bound for a local search algorithm, namely for CSAT. The class of formulas we consider covers most of DIMACS benchmarks, the satisfiability problem for this class of formulas is NP-complete.",
author = "Hirsch, {Edward A.}",
note = "Publisher Copyright: {\textcopyright} 1998, Springer-Verlag. All rights reserved.; 6th Scandinavian Workshop on Algorithm Theory, SWAT 1998 ; Conference date: 08-07-1998 Through 10-07-1998",
year = "1998",
doi = "10.1007/BFb0054372",
language = "אנגלית",
isbn = "3540646825",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
pages = "246--254",
editor = "Stefan Arnborg and Lars Ivansson",
booktitle = "Algorithm Theory — SWAT 1998 - 6th Scandinavian Workshop on Algorithm Theory, Proceedings",
}