This preprint was accepted September 28, 1998
Contact:
Edward A. Hirsch
ABSTRACT: In 1992 B.~Selman, H.~Levesque and D.~Mitchell proposed GSAT, a greedy local search algorithm for the Boolean satisfiability problem. Good performance of this algorithm and its modifications has been demonstrated by many experimental results. In 1993 I.~P.~Gent and T.~Walsh proposed CSAT, a version of GSAT that almost does not use greediness. It has been recently proved that CSAT can find a satisfying assignment for a restricted class of formulas in the time $c^n$, where $c<2$ is a constant. In this paper we prove a lower bound of the order $2^n$ for GSAT and CSAT. Namely, we construct formulas $F_n$ of $n$ variables, such that GSAT or CSAT finds a satisfying assignment for $F_n$ only if this assignment or one of its $n$ neighbours is chosen as the initial assignment for the search.