Readme file for the local search program "testhill" v 0.1, 1993/10/27.
--
Copyright (C) 1993, Fred Annexstein, John Franco, Humberto
Ortiz-Zuazaga, Manian Swaminathan.

This program is free software; you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation; either version 2 of the License, or (at
your option) any later version.

This program is distributed in the hope that it will be useful, but
WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
General Public License for more details.

You should have received a copy of the GNU General Public License
along with this program; if not, write to the Free Software
Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
--

Here is the ANSI C source code for a simple local search routine for
SAT, similar to Gent and Walsh's HSAT [1] or Hampson and Kibler's
memoryless algorithm [2].  Some routines may assume an int is at least
32 bits.

cnf.c and cnf.h define the data structures for the problem.

hill.c and hill.h define the local search routine.

testhill.c is a test harness for the routines, when compiled, it will
try to read a file named on the command line as a DIMACS cnf format
instance and running the local search routine.

These programs require the UCSC parser to be linked into the
executable.  It may be obtained from:

dimacs.rutgers.edu:
/pub/challenge/satisfiability/contributed/UCSC/instances/Cnfparse.tar.Z

The programs were developed using noweb, a language independent
literate programming tool available from:

bellcore.com:pub/norman/noweb.shar.Z

hill.nw and cnf.nw are the original web source files.  hill.dvi and
cnf.dvi are the device independent files produced from latexing the
woven web files.  I find them much nicer to read than the .c and .h
files.  If you install noweb, the makefile has commented out rules for
producing the dvi and source files from the webs.

These programs were developed on a 386SX-16 PC clone, running linux, a
free operating system, using free software (GNU Emacs, gcc, TeX and
LaTeX, noweb, and the X Window System).

References

1) I. P. Gent and T. Walsh (1993): Towards an understanding of
hill-climbing procedures for SAT. Technical report available from
DIMACS ftp repository.

2) S. Hampson and D. Kibler (1993): Plateaus and plateau search in
boolean satisfiability problems: plateau search techniques.  Informal
proceedings of DIMACS SAT challenge.

--
Humberto Ortiz-Zuazaga
zuazaga@ucunix.san.uc.edu
