Local search algorithms for SAT: Worst-case analysis.

Recent experiments demonstrated that local search algorithms (e.g. GSAT) axe 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 2itα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. [ABSTRACT FROM AUTHOR]