###
Petersburg Department of Steklov Institute of Mathematics

#
PREPRINT 19/1998

Edward A. HIRSCH
##
HARD FORMULAS FOR SAT LOCAL SEARCH ALGORITHMS

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.

Back to all preprints

Back to the Petersburg Department of
Steklov Institute of Mathematics