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.
GNU General Public License
Here is the ANSI C source code for a simple local search routine for SAT, similar to Gent and Walsh's HSAT  or Hampson and Kibler's memoryless algorithm . Some routines may assume an int is at least 32 bits. (36K gzip'ed tarfile).
cnf.nw cnf.c and cnf.h define the data structures for the problem.
hill.nw 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 Chalenge Site
The programs were developed using noweb, a language independent literate programming tool.
hill.nw and cnf.nw are the original web source files woven to HTML. Thhe document files produced from latexing the woven web files are also available in dvi, postscript, and acrobat formats. 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 GNU/linux, a free operating system, using free software (GNU Emacs, gcc, TeX and LaTeX, noweb, and the X Window System).
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
Most recent change: 2005/1/4 at 20:51
Generated with GTML