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