This directory contains two files. They are postscript versions
of two recent reports. These papers will soon be available as
Technical Reports from Dept of AI, University of Edinburgh, Scotland.

enigma.ps    "The Enigma of SAT Hill-climbing Procedures"

In this paper, we investigate a family of hill-climbing
procedures related to GSAT, a greedy random hill-climbing procedure 
for satisfiability. These procedures are able to solve large and
difficult satisfiability problems beyond the range of conventional 
procedures like David-Putnam. We explore the role of greediness, 
randomness and hill-climbing in the effectiveness of these procedures. 
In addition, we observe some quite remarkable and universal features 
of their search for a satisfying truth assignment.

gensat.ps    "Towards an Understanding of Hill-climbing Procedures
              for SAT"

Recently several local hill-climbing procedures for propositional
satisfiability have been proposed which are able to solve large and
difficult problems beyond the reach of conventional algorithms like
Davis-Putnam. By the introduction of some new variants of these 
procedures, we provide strong experimental evidence to support
the conjecture that neither greediness nor randomness is important 
in these procedures. One of the variants introduced seems to offer 
significant improvements over earlier procedures. In addition, we 
investigate experimentally how performance depends on their parameters.
Our results suggest that run-time scales less than simply exponentially 
in the problem size.