Local search for 3SAT

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
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 [1] or Hampson and Kibler's memoryless algorithm [2]. 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.

Troglodita approved!

Humberto Ortiz Zuazaga

Most recent change: 2005/1/4 at 20:51
Generated with GTML