%Please find enclosed LaTeX source of our research abstract. It
%should LaTeX without difficulty. It includes some keywords
%to aid classification. 

%toby walsh

\documentstyle[12pt,a4]{article}

\title{SAT Hill-climbing Procedures}
\author{Ian P. Gent and Toby Walsh \\
I.P.Gent@edinburgh.ac.uk, T.Walsh@edinburgh.ac.uk \\
Department of Artificial Intelligence,\\
University of Edinburgh, \\
80 South Bridge, Edinburgh EH1~1HN}
% leave date blank
\date{}

\begin{document}

\maketitle

\begin{center}
Keywords: SAT, approximation procedures, hill-climbing.
\end{center}

Recently several
local hill-climbing procedures
for SAT have
been proposed \cite{gu,selman1,enigma}.
Much of the interest in these local hill-climbing procedures 
is because they seem to scale well and because they can
solve large and difficult SAT problems beyond the reach
of conventional algorithms like the
Davis-Putnam procedure.

These hill-climbing procedures share three common features. First, 
they attempt
to determine the satisfiability of a formula in conjuctive normal form.
Second, they
hill-climb on the number of satisfied clauses.
And third, their local neighbourhood (which they search for a better
truth assignment) is the set of truth assigments with the 
assignment to {\em one} variable changed. 
Typical of such procedures is 
GSAT \cite{selman1}, a greedy random hill-climbing procedure.
GSAT starts with a randomly generated truth assignment, 
and hill-climbs by changing (or ``flipping'') the variable
assignment which gives the largest increase in the number of clauses 
satisfied.

To investigate procedures like GSAT, we
have introduced a generalisation of GSAT called ``GenSAT" \cite{enigma}.
\begin{tabbing}
sss \= sss \= sss \= sssss \= sss \= \kill
{\bf procedure} GenSAT($\Sigma$) \\
\> {\bf for} i $:=1$ {\bf to} Max-tries \\
\> \> T $:=$ {\em initial($\Sigma$)} \ \  ; generate an initial truth assignment \\
\> \> {\bf for} j $:=1$ {\bf to} Max-flips \\
\> \> \> {\bf if} T satisfies $\Sigma$ {\bf then} {\bf return} T \\
\> \> \> {\bf else} \> Poss-flips $:=$ {\em hill-climb($\Sigma$,T)} \ \ ; compute best local neighbours \\
\> \> \> \> V $:=$ {\em pick}(Poss-flips) \ \ ; pick one to flip\\
\> \> \> \> T $:=$ T with V's truth assignment flipped \\
\> \> {\bf end} \\
\> {\bf end} \\
\> {\bf return} ``no satisfying assignment found"\\
\end{tabbing}
By varying the functions {\it initial}, 
{\it hill-climb} and {\it pick}, we have explored the importance
of such features as greediness and randomness for the performance
of this local hill-climbing. Surprisingly, neither greediness
nor randomness seem crucial \cite{enigma}. 

Most of our experiments have been (and will continue to be) on
difficult regions of random $k$-SAT. Problems in random $k$-SAT 
with N variables and L clauses are generated
as follows: for each clause a random subset of size $k$ of the N variables
is selected and each of these variables is made positive or negative
with probability $\frac{1}{2}$.
For random $3$-SAT the ratio L/N~=~4.3 has been identified as
giving problems 
which are particularly hard for Davis-Putnam and many other
algorithms. However, we also intend to perform experiments
on the sorts of structured problem sets encountered in practice. 

Our future research plans include the following topics:
\begin{description}
\item[Control strategies.] Investigation of other control
strategies for choosing which variables to flip.
\item[Score functions.] Development of new score functions for hill-climbing.
\item[Scalability.] Determination of how well these 
procedures scale (both theoretically and experimentally). 
\item[Parallelization.] Implementation of
a parallel version of GenSAT for the Connection Machine.
\item[Theory.] Construction of a theoretical model to describe 
the behaviour of these procedures.
\end{description}

We welcome collaboration and contact with other researchers interested
in approximation procedures for SAT (and, indeed, approximation
procedures for other NP-hard problems). In addition, we would
be pleased to receive any challenge SAT problems or
SAT problem generators.


\begin{thebibliography}{Gent \& Walsh 92}

\bibitem[Gent \& Walsh 92]{enigma}
I.~Gent and T.~Walsh.
\newblock {The} {Enigma} of {SAT} {Hill-climbing} {Procedures}.
\newblock {Technical Report} 605, Dept. of Artificial Intelligence, University
  of Edinburgh, 1992.

\bibitem[Gu 92]{gu}
Jun Gu.
\newblock Efficient local search for very large-scale satisfiability problems.
\newblock {\em SIGART Bulletin}, 3(1), January 1992.

\bibitem[Selman {\it et al} 92a]{selman1}
B.~Selman, H.~Levesque, and D.~Mitchell.
\newblock A {New} {Method} for {Solving} {Hard} {Satisfiability} {Problems}.
\newblock In {\em Proceedings of the 10th National Conference on AI}, pages
  440--446. American Association for Artificial Intelligence, 1992.

\end{thebibliography}

\end{document}