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^an (a<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.

Full text: [ .ps.gz (39 Kb, (c)Springer-Verlag) ]