Proceedings of SWAT'98, LNCS 1432, pp.246-254.

**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) ]

Back to the list of papers