Petersburg Department of Steklov Institute of Mathematics

PREPRINT 19/1998

Edward A. HIRSCH


This preprint was accepted September 28, 1998
Contact: Edward A. Hirsch

  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