\documentstyle[jair,twoside,11pt,theapa]{article} \input epsf \jairheading{1}{1993}{47-59}{6/93}{9/93} \ShortHeadings{An Empirical Analysis of Search in \GSAT} {Gent \& Walsh} \firstpageno{47} \def\GSAT{{\sc GSAT}} \def\CSAT{{\sc CSAT}} \def\GenSAT{{\sc GenSAT}} \def\SAT{{\sc SAT}} \def\kSAT{{\sc $k$-SAT}} \def\3SAT{{\sc 3-SAT}} \def\N{\mbox{\rm N}} \def\NN{\mbox{\rm \tiny N}} \def\L{\mbox{\rm L}} \def\LL{\mbox{\rm \scriptsize L}} \newcommand{\secref}[1]{\S \ref{#1}} \begin{document} \title{An Empirical Analysis of Search in GSAT} \author{\name Ian P. Gent \email I.P.Gent@edinburgh.ac.uk \\ \addr Department of Artificial Intelligence, University of Edinburgh \\ 80 South Bridge, Edinburgh EH1~1HN, United Kingdom \AND \name Toby Walsh \email walsh@loria.fr \\ \addr INRIA-Lorraine, 615, rue du Jardin Botanique, \\ 54602 Villers-les-Nancy, France } \maketitle \vspace{-0.075cm} \begin{abstract} We describe an extensive study of search in \GSAT, an approximation procedure for propositional satisfiability. \GSAT\ performs greedy hill-climbing on the number of satisfied clauses in a truth assignment. Our experiments provide a more complete picture of \GSAT's search than previous accounts. We describe in detail the two phases of search: rapid hill-climbing followed by a long plateau search. We demonstrate that when applied to randomly generated \3SAT\ problems, there is a very simple scaling with problem size for both the mean number of satisfied clauses and the mean branching rate. Our results allow us to make detailed numerical conjectures about the length of the hill-climbing phase, the average gradient of this phase, and to conjecture that both the average score and average branching rate decay exponentially during plateau search. We end by showing how these results can be used to direct future theoretical analysis. This work provides a case study of how computer experiments can be used to improve understanding of the theoretical properties of algorithms. \end{abstract} \vspace{-0.075cm} \section{Introduction} \label{sec-intro} Mathematicians are increasingly recognizing the usefulness of experiments with computers to help advance mathematical theory. It is surprising therefore that one area of mathematics which has benefitted little from empirical results is the theory of algorithms, especially those used in AI. Since the objects of this theory are abstract descriptions of computer programs, we should in principle be able to reason about programs entirely deductively. However, such theoretical analysis is often too complex for our current mathematical tools. Where theoretical analysis is practical, it is often limited to (unrealistically) simple cases. For example, results presented in \cite{greedy-alg} for the greedy algorithm for satisfiability do not apply to interesting and hard region of problems as described in ~\secref{sec-problems}. In addition, actual behaviour on real problems is sometimes quite different to worst and average case analyses. We therefore support the calls of McGeoch \cite{mcgeoch1}, Hooker \cite{hooker1} and others for the development of an empirical science of algorithms. In such a science, experiments as well as theory are used to advance our understanding of the properties of algorithms. One of the aims of this paper is to demonstrate the benefits of such an empirical approach. We will present some surprising experimental results and demonstrate how such results can direct future efforts for a theoretical analysis. The algorithm studied in this paper is \GSAT, a randomized hill-climbing procedure for propositional satisfiability (or \SAT) \cite{selman-gsat,gsat-ext}. Propositional satisfiability is the problem of deciding if there is an assignment for the variables in a propositional formula that makes the formula true. Recently, there has been considerable interest in \GSAT\ as it appears to be able to solve large and difficult satisfiability problems beyond the range of conventional procedures like Davis-Putnam \cite{selman-gsat}. We believe that the results we give here will actually apply to a larger family of procedures for satisfiability called \GenSAT\ \cite{gensat}. Understanding such procedures more fully is of considerable practical interest since \SAT\ is, in many ways, the archetypical (and intractable) NP-hard problem. In addition, many AI problems can be encoded quite naturally in \SAT\ ({\it eg.} constraint satisfaction, diagnosis and vision interpretation, refutational theorem proving, planning). This paper is structured as follows. In \secref{sec-gsat} we introduce \GSAT, the algorithm studied in the rest of the paper. In \secref{sec-problems} we define and motivate the choice of problems used in our experiments. The experiments themselves are described in \secref{sec-graphs}. These experiments provide a more complete picture of \GSAT's search than previous informal accounts. The results of these experiments are analysed more closely in \secref{sec-numerical} using some powerful statistical tools. This analysis allow us to make various experimentally verifiable conjectures about \GSAT's search. For example, we are able to conjecture: the length of GSAT's initial hill-climbing phase; the average gradient of this phase; the simple scaling of various important features like the score (on which hill-climbing is performed) and the branching rate. In \secref{sec-theory} we suggest how such results can be used to direct future theoretical analysis. Finally, in \secref{sec-related} we describe related work and end with some brief conclusions in \secref{sec-conclusions}. \section{GSAT} \label{sec-gsat} \GSAT\ is a random greedy hill-climbing procedure. \GSAT\ deals with formulae in conjunctive normal form (CNF); a formula, $\Sigma$ is in CNF iff it is a conjunction of clauses, where a clause is a disjunction of literals. \GSAT\ starts with a randomly generated truth assignment, then hill-climbs by ``flipping" the variable assignment which gives the largest increase in the number of clauses satisfied (called the ``score'' from now on). Given the choice between several equally good flips, \GSAT\ picks one at random. If no flip can increase the score, then a variable is flipped which does not change the score or (failing that) which decreases the score the least. Thus \GSAT\ starts in a random part of the search space and searches for a global solution using only local information. Despite its simplicity, this procedure has been shown to give good performance on hard satisfiability problems~\cite{selman-gsat}. {\samepage \begin{tabbing} sss \= sss \= sss \= sssss \= sss \= \kill {\bf procedure} GSAT($\Sigma$) \\ \> {\bf for} i $:=1$ {\bf to} Max-tries \\ \> \> T $:=$ random truth assignment \\ \> \> {\bf for} j $:=1$ {\bf to} Max-flips \\ \> \> \> {\bf if} T satisfies $\Sigma$ {\bf then} {\bf return} T \\ \> \> \> {\bf else} \> Poss-flips $:=$ set of vars which increase satisfiability most \\ \> \> \> \> V $:=$ a random element of Poss-flips \\ \> \> \> \> T $:=$ T with V's truth assignment flipped \\ \> \> {\bf end} \\ \> {\bf end} \\ \> {\bf return} ``no satisfying assignment found" \end{tabbing}} \pagebreak In \cite{gensat} we describe a large number of experiments which suggest that neither greediness not randomness is important for the performance of this procedure. These experiments also suggest various other conjectures. For instance, for random \3SAT problems (see \secref{sec-problems}) the log of the runtime appears to scale with a less than linear dependency on the problem size. Conjectures such as these could, as we noted in the introduction, be very profitably used to direct future efforts to analyse \GSAT\ theoretically. Indeed, we believe that the experiments reported here suggest various conjectures which would be useful in a proof of the relationship between runtime and problem size (see \secref{sec-theory} for more details) \section{Problem Space} \label{sec-problems} To be able to perform experiments on an algorithm, you need a source of problems on which to run the algorithm. Ideally the problems should come from a probability distribution with some well-defined properties, contain a few simple parameters and be representative of problems which occur in real situations. Unfortunately, it is often difficult to meet all these criteria. In practice, one is usually forced to accept either problems from a well-defined distribution with a few simple parameters or a benchmark set of real problems, necessarily from some unknown distribution. In these experiments we adopt the former approach and use CNF formulae randomly generated according to the random \kSAT\ model. Problems in random \kSAT\ with N variables and L clauses are generated as follows: a random subset of size $k$ of the N variables is selected for each clause, and each variable is made positive or negative with probability $\frac{1}{2}$. For random \3SAT, there is a phase transition from satisfiable to unsatisfiable when L is approximately 4.3N~\cite{mitchell-hard-easy,larrabee-tsuji,crawford-auton}. At lower L, most problems generated are under-constrained and are thus satisfiable; at higher L, most problems generated are over-constrained and are thus unsatisfiable. As with many NP-complete problems, problems in the phase transition are typically much more difficult to solve than problems away from the transition \cite{cheeseman-hard}. The region L=4.3N is thus generally considered to be a good source of hard \SAT\ problems and has been the focus of much recent experimental effort. \section{GSAT's search} \label{sec-graphs} When \GSAT\ was first introduced, it was noted that search in each try is divided into two phases. In the first phase of a try, each flip increases the score. However, this phase is relatively short and is followed by a second phase in which most flips do not increase the score, but are instead sideways moves which leave the same number of clauses satisfied. This phase is a search of a ``plateau" for the occasional flip that can increase the score.\footnote{Informal observations to this effect were made by Bart Selman during the presentation of \cite{selman-gsat} at AAAI-92. These observations were enlarged upon in \cite{rp605}.} One of the aims of this paper is to improve upon such informal observations by making {\em quantitative} measurements of \GSAT's search, and by using these measurements to make several experimentally testable predictions. In our experiments, we followed three methodological principles >from \cite{mcgeoch1}. First, we performed experiments with large problem sizes and many repetitions, to reduce variance and allow for emergent properties. Second, we sought good views of the data. That is, we looked for features of performance which are meaningful and which are as predictable as possible. Third, we analysed our results closely. Suitable analysis of data may show features which are not clear from a simple presentation. In the rest of this paper we show how these principles enabled us to make very detailed conjectures about \GSAT's search. Many features of \GSAT's search space can be graphically illustrated by plotting how they vary during a try. The most obvious feature to plot is the score, the number of satisfied clauses. In our quest for a good view of \GSAT's search space, we also decided to plot ``poss-flips" at each flip: that is, the number of equally good flips between which \GSAT\ randomly picks. This is an interesting measure since it indicates the branching rate of \GSAT's search space. We begin with one try of \GSAT\ on a 500 variable random \3SAT\ problem in the difficult region of L = 4.3N (Figure \ref{fig-onetry}a). Although there is considerable variation between tries, this graph illustrates features common to all tries. Both score (in Figure \ref{fig-onetry}a) and poss-flips (in Figure \ref{fig-onetry}b) are plotted as percentages of their maximal values, that is L and N respectively. The percentage score starts just above 87.5\%, which might seem surprisingly high. Theoretically, however, we expect a random truth assignment in \kSAT\ to satisfy $\frac{2^k-1}{2^k}$ of all clauses (in this instance, $\frac{7}{8}$). As expected from the earlier informal description, the score climbs rapidly at first, and then flattens off as we mount the plateau. The graph is discrete since positive moves increase the score by a fixed amount, but some of this discreteness is lost due to the small scale. To illustrate the discreteness, in Figure~\ref{fig-onetry}b we plot the change in the number of satisfied clauses made by each flip (as its exact value, unscaled). Note that the $x$-axis for both plots in Figure~\ref{fig-onetry}b is the same. \begin{figure}[h] %%export from xfig done with portrait mode, and scaling = 70% \begin{tabular}{cc} \epsfbox{/home/dream5/ipg/tex/jair/Figs/onetryscore.eps} & \epsfbox{/home/dream5/ipg/tex/jair/Figs/onetry.pfdelta.eps} \\ (a) Score &(b) Change in score, and poss-flips\\ \end{tabular} \caption{\GSAT's behaviour during one try, N = 500, L = 2150, first 250 flips} \label{fig-onetry} \end{figure} The behaviour of poss-flips is considerably more complicated than that of the score. It is easiest first to consider poss-flips once on the plateau. The start of plateau search, after 115 flips, coincides with a very large increase in poss-flips, corresponding to a change from the region where a small number of flips can increase the score by 1 to a region where a large number of flips can be made which leave the score unchanged. Once on the plateau, there are several sharp dips in poss-flips. These correspond to flips where an increase by 1 in the score was effected, as can be seen from Figure~\ref{fig-onetry}b. It seems that if you can increase the score on the plateau, you only have a very small number of ways to do it. Also, the dominance of flips which make no change in score graphically illustrates the need for such ``sideways" flips, a need that has been noted before \cite{selman-gsat,gensat}. Perhaps the most fascinating feature is the initial behaviour of poss-flips. There are four well defined wedges starting at 5, 16, 26, and 57 flips, with occasional sharp dips. These wedges demonstrate behaviour analogous to the that of poss-flips on the plateau. The plateau spans the region where flips typically do not change the score: we call this region $H_0$ since hill-climbing typically makes zero change to the score. The last wedge spans the region $H_1$ where hill-climbing typically increases the score by 1, as can be seen very clearly >from Figure~\ref{fig-onetry}b. Again Figure~\ref{fig-onetry}b shows that the next three wedges (reading right to left) span regions $H_2$, $H_3$, and $H_4$. As with the transition onto the plateau, the transition between each region is marked by a sharp increase in poss-flips. Dips in the wedges represent unusual flips which increase the score by more than the characteristic value for that region, just as the dips in poss-flips on the plateau represent flips where an increase in score was possible. This exact correlation can be seen clearly in Figure~\ref{fig-onetry}b. Note that in this experiment, in no region $H_j$ did a change in score of $j+2$ occur, and that there was no change in score of $-1$ at all. In addition, each wedge in poss-flips appears to decay close to linearly. This is explained by the facts that once a variable is flipped it no longer appears in poss-flips (flipping it back would decrease score), that most of the variables in poss-flips can be flipped independently of each other, and that new variables are rarely added to poss-flips as a consequence of an earlier flip. On the plateau, however, when a variable is flipped which does not change the score, it remains in poss-flips since flipping it back also does not change the score. To determine if this behaviour is typical, we generated 500 random \3SAT\ problems with N=500 and L=4.3N, and ran 10 tries of \GSAT\ on each problem. Figure~\ref{fig-av}a shows the mean percentage score\footnote{In this paper we assign a score of 100\% to flips which were not performed because a satisfying truth assignment had already been found.} while Figure~\ref{fig-av}b presents the mean percentage poss-flips together with the mean change in score at each flip. (The small discreteness in this figure is due to the discreteness of Postscript's plotting.) \begin{figure}[htb] \begin{tabular}{cc} \epsfbox{/home/dream5/ipg/tex/jair/Figs/avscore4.3.500.eps}& \epsfbox{/home/dream5/ipg/tex/jair/Figs/gsat500avdelta.eps}\\ (a) Mean score& (b) Mean change in score, poss-flips \end{tabular} \caption{Mean \GSAT\ behaviour, N = 500, L = 4.3N, first 250 flips} \label{fig-av} \end{figure} The average percentage score is very similar to the behaviour on the individual run of Figure~\ref{fig-onetry}, naturally being somewhat smoother. The graph of average poss-flips seems quite different, but it is to be expected that you will neither observe the sharply defined dips in poss-flips from Figure~\ref{fig-onetry}b, nor the very sharply defined start to the wedges, since these happen at varying times. It is remarkable that the wedges are consistent enough to be visible when averaged over 5,000 tries; the smoothing in the wedges and the start of the plateau is caused by the regions not starting at exactly the same time in each try. Figure~\ref{fig-av} does not distinguish between satisfiable and unsatisfiable problems. There is no current technique for determining the satisfiability of 500 variable \3SAT\ problems in feasible time. From instances we have been able to test, we do not believe that large differences from Figure~\ref{fig-av} will be seen when it is possible to plot satisfiable and unsatisfiable problems separately, but this remains an interesting topic to investigate in the future. Experiments with other values of N with the same ratio of clauses to variables demonstrated qualitatively similar behaviour. More careful analysis shows the remarkable fact that not only is the behaviour qualitatively similar, but quantitatively similar, with a simple linear dependency on N. If graphs similar to Figure~\ref{fig-av} are plotted for each N with the x-axis scaled by N, behaviour is almost {\em identical}. To illustrate this, Figure~\ref{fig-scaleshort} shows the mean percentage score, percentage poss-flips, and change in score, for N = 500, 750, and 1000, for L = 4.3N and for the first 0.5N flips (250 flips at N = 500). Both Figure~\ref{fig-scaleshort}a and Figure~\ref{fig-scaleshort}b demonstrate the closeness of the scaling, to the extent that they may appear to contain just one thick line. In Figure~\ref{fig-scaleshort}b there is a slight tendency for the different regions of hill-climbing to become better defined with increasing N. \begin{figure}[htb] \begin{tabular}{cc} \epsfbox{/home/dream5/ipg/tex/jair/Figs/scalescore4.3.short.eps}& \epsfbox{/home/dream5/ipg/tex/jair/Figs/Scale.pfdelta.4.3.eps}\\ (a) Mean score& (b) Mean change in score, poss-flips \end{tabular} \caption{Scaling of mean \GSAT\ behaviour, N = 500, 750, 1000, first 0.5N flips} \label{fig-scaleshort} \end{figure} The figures we have presented only reach a very early stage of plateau search. To investigate further along the plateau, we performed experiments with 100, 200, 300, 400, and 500 variables from 0 to 2.5N flips.\footnote{At 100 variables, 2.5N flips is close to the optimal value for Max-flips. However, experiments have suggested that Max-flips may need to vary quadratically for larger N \cite{gensat}.} In Figure~\ref{fig-scale4.3}a shows the mean percentage score in each case, while Figure~\ref{fig-scale4.3}b shows the mean percentage poss-flips, magnified on the $y$-axis for clarity. Both these figures demonstrate the closeness of the scaling on the plateau. In Figure~\ref{fig-scale4.3}b the graphs are not quite so close together as in Figure~\ref{fig-scale4.3}a. The phases of hill-climbing become much better defined with increasing N. During plateau search, although separate lines are distinguishable, the difference is always considerably less than 1\% of the total number of variables. \begin{figure}[htb] \begin{tabular}{cc} \epsfbox{/home/dream5/ipg/tex/jair/Figs/Scalescore4.3.eps} &\epsfbox{/home/dream5/ipg/tex/jair/Figs/Scalepf4.3.eps} \\ (a) mean score, L = 4.3N&(b) mean poss-flips, L = 4.3N \end{tabular} \caption{Scaling of mean \GSAT\ behaviour, N = 100, 200, 300, 400, 500} \label{fig-scale4.3} \end{figure} The problems used in these experiments (random \3SAT\ with L=4.3N) are believed to be unusually hard and are satisfiable with probability approximately $\frac{1}{2}$. Neither of these facts appears to be relevant to the scaling of \GSAT's search. To check this we performed a similar range of experiments with a ratio of clauses to variables of 6. Although almost all such problems are unsatisfiable, we observed exactly the same scaling behaviour. The score does not reach such a high value as in Figure~\ref{fig-scale4.3}a, as is to be expected, but nevertheless shows the same linear scaling. On the plateau, the mean value of poss-flips is lower than before. We again observed this behaviour for L = 3N, where almost all problems are satisfiable. The score approaches 100\% faster than before, and a higher value of poss-flips is reached on the plateau, but the decay in the value of poss-flips seen in Figure~\ref{fig-scale4.3}b does not seem to be present. To summarise, we have shown that \GSAT's hill-climbing goes through several distinct phases, and that the average behaviour of certain important features scale in linear fashion with N. These results provide a considerable advance on previous informal descriptions of \GSAT's search. \section{Numerical Conjectures} \label{sec-numerical} In this section, we will show that detailed numerical conjectures can be made if the data presented graphically in \secref{sec-graphs} is analysed numerically. We divide our analysis into two parts: first we deal with the plateau search, where behaviour is relatively simple, then we analyse the hill-climbing search. \label{sec-regression} \label{sec-plat} On the plateau, both average score and poss-flips seem to decay exponentially with a simple linear dependency on problem size. To test this, we performed regression analysis on our experimental data, using the models \begin{eqnarray} S(x) & = & \N \cdot ( B - C\cdot e^{-\frac{x}{A\cdot \NN}}) \label{eq-model-score}\\ P(x) & = & \N \cdot ( E + F\cdot e^{-\frac{x}{D\cdot \NN}}) \label{eq-model-pflips} \end{eqnarray} where $x$ represents the number of flips, $S(x)$ the average score at flip $x$ and $P(x)$ the average number of possible flips. To determine \GSAT's behaviour just on the plateau, we analysed data on mean score, starting from 0.4N flips, a time when plateau search always appears to have started (see \secref{sec-hc}). Our experimental data fitted the model very well. Detailed results for ${\rm N} = 500$ are given in Table~\ref{tab-score} to three significant figures. The values of A, B, and C change only slightly with N, providing further evidence for the scaling of \GSAT's behaviour. For L = 3N the asymptotic mean percentage score is very close to 100\% of clauses being satisfied, while for L = 4.3N it is approximately 99.3\% of clauses and for L = 6N it is approximately 98.2\% of clauses. A good fit was also found for mean poss-flips behaviour (see Table~\ref{tab-possflips} for ${\rm N} = 500$), except for L = 3N, where the mean value of poss-flips on the plateau may be constant. It seems that for L = 4.3N the asymptotic value of poss-flips is about 10\% of N and that for 6 it is about 5\% of N. It is important to note that the behaviour we analysed was for mean behaviour over both satisfiable and unsatisfiable problems. It is likely that individual problems will exhibit similar behaviour with different asymptotes, but we do not expect even satisfiable problems to yield a mean score of 100\% asymptotically. Note that as N increases a small error in percentage terms may correspond to a large error in the actual score. As a result, our predictions of asymptotic score may be inaccurate for large N, or for very large numbers of flips. Further experimentation is necessary to examine these issues in detail. \begin{table}[htb] \begin{center} \begin{tabular}{|c|c|c|c|c|c|} \hline L/N&N&A&B&C&$R^2$\\\hline 3&500&0.511&2.997&0.0428&0.995\\ %%score3.N.out \hline 4.3&500&0.566&4.27&0.0772&0.995\\ %%score4.3.N.out \hline 6&500&0.492&5.89&0.112&0.993\\ \hline \end{tabular} \end{center} \caption{Regression results for average score of \GSAT.\protect\footnotemark} \label{tab-score} \end{table} %% just putting this somewhere to get it on the right page \footnotetext{The value of $R^2$ is a number in the interval $[0,1]$ indicating how well the variance in data is explained by the regression formula. $1 - R^2$ is the ratio between variance of the data from its predicted value, and the variance of the data from the mean of all the data. A value of $R^2$ close to 1 indicates that the regression formula fits the data very well.} \begin{table}[htb] \begin{center} \begin{tabular}{|c|c|c|c|c|c|} \hline L/N&N&D&E&F&$R^2$\\\hline 4.3&500&0.838&0.100&0.0348&0.996\\ %%pf4.3.N.out \hline 6&500&0.789&0.0502&0.0373&0.999\\ \hline \end{tabular} \end{center} \caption{Regression results on average poss-flips of \GSAT.} \label{tab-possflips} \end{table} \label{sec-hc} We have also analysed \GSAT's behaviour during its hill-climbing phase. Figure~\ref{fig-onetry}b shows regions where most flips increase the score by 4, then by 3, then by 2, then by 1. Analysis of our data suggested that each phase lasts roughly twice the length of the previous one. This motivates the following conjectures: \GSAT\ moves through a sequence of regions $H_j$ for $j= ...,3,2,1$ in which the majority of flips increase the score by $j$, and where the length of each region $H_j$ is proportional to $2^{-j}$ (except for the region $H_0$ which represents plateau search). To investigate this conjecture, we analysed 50 tries each on 20 different problems for random \3SAT\ problems at N=500 and L=4.3N. We very rarely observe flips in $H_j$ that increase the score by {\em less} than $j$, and so {define} $H_j$ as the region between the first flip which increases the score by exactly $j$ and the first flip which increases the score by less than $j$ (unless the latter actually appears before the former, in which case $H_j$ is empty). One simple test of our conjecture is to compare the total time spent in $H_j$ with the total time up to the end of $H_j$; we predict that this ratio will be $\frac{1}{2}$. For $j = 1$ to 4 the mean and standard deviations of this ratio, and the length of each region are shown in Table~\ref{table-hc}.\footnote{The data for ``All climbing'' is the length to the start of $H_0$.} This data supports our conjecture although as j increases each region is slightly longer than predicted. The total length of hill-climbing at N=500 is 0.22N flips, while at N=100 it is 0.23N. This is consistent with the scaling behaviour observed in \secref{sec-graphs}. \begin{table}[htb] \begin{center} \begin{tabular}{|c|cc|cc|} \hline Region&mean ratio&s.d.&mean length&s.d. \\ \hline All climbing&---&---&112&7.59\\ $H_1$&0.486&0.0510&54.7&7.69\\ $H_2$&0.513&0.0672&29.5&5.12\\ $H_3$&0.564&0.0959&15.7&3.61\\ $H_4$&0.574&0.0161&7.00&2.48\\\hline \end{tabular} \end{center} \caption{Comparative and Absolute Lengths of hill-climbing phases} \label{table-hc} \end{table} Our conjecture has an appealing corollary. Namely, that if there are $i$ non-empty hill-climbing regions, the average change in score per flip during hill-climbing is: \begin{eqnarray} \frac{1}{2}\cdot 1 + \frac{1}{4}\cdot 2 + \frac{1}{8}\cdot 3 + \frac{1}{16}\cdot 4 + \cdots + \frac{1}{2^i}\cdot i &\approx&2. \end{eqnarray} It follows from this that mean gradient of the entire hill-climbing phase is approximately 2. At N=500, we observed a mean ratio of change in score per flip during hill-climbing of 1.94 with a standard deviation of 0.1. At N=100, the ratio is 1.95 with a standard deviation of 0.2. The model presented above ignores flips in $H_j$ which increase the score by more than $j$. Such flips were seen in Figure~\ref{fig-onetry}b in regions $H_3$ to $H_1$. In our experiment 9.8\% of flips in $H_1$ were of size 2 and 6.3\% of flips in $H_2$ were of size 3. However, flips of size $j+2$ were very rare, forming only about 0.02\% of all flips in $H_1$ and $H_2$. We conjectured that an exponential decay similar to that in $H_0$ occurs in each $H_j$. That is, we conjecture that the average change in number of satisfied clauses from flip $x$ to flip $x+1$ in $H_j$ is given by: \begin{equation} j + E_j\cdot e^{-\frac{x}{D_j\cdot \NN}} \label{eq-model-hc} \end{equation} This might correspond to a model of \GSAT's search in which there are a certain number of flips of size $j+1$ in each region $H_j$, and the probability of making a $j+1$ flip is merely dependent on the number of such flips left; the rest of the time, \GSAT\ is obliged to make a flip of size $j$. Our data from 1000 tries fitted this model well, giving values of $R^2$ of 96.8\% for $H_1$ and 97.5\% for $H_2$. The regression gave estimates for the parameters of: $D_1 = 0.045$, $E_1 = 0.25$, $D_2 = 0.025$, $E_2 = 0.15$. Not surprisingly, since the region $H_3$ is very short, data was too noisy to obtain a better fit with the model (\ref{eq-model-hc}) than with one of linear decay. These results support our conjecture, but more experiments on larger problems are needed to lengthen the region $H_j$ for $j \geq 3$. \section{Theoretical Conjectures} \label{sec-theory} Empirical results like those given in \secref{sec-regression} can be used to direct efforts to analyse algorithms theoretically. For example, consider the plateau region of \GSAT's search. If the model (\ref{eq-model-score}) applies also to successful tries, the asymptotic score is L, giving \begin{eqnarray*} S(x) & = & \L - C\cdot \N \cdot e^{-\frac{x}{A\cdot \NN}} \end{eqnarray*} Differentiating with respect to $x$ we get, \begin{eqnarray*} \frac{\mbox{\rm d} S(x)}{\mbox{\rm d}x} & = & \frac{C}{A}\cdot e^{-\frac{x}{a\cdot \NN}} ~ = ~ \frac{\L-S(x)}{A\cdot \N} \end{eqnarray*} The gradient is a good approximation for $D_x$, the average size of a flip at $x$. Hence, \begin{eqnarray*} D_x & = & \frac{\L-S(x)}{A \cdot \N} \end{eqnarray*} Our experiments suggest that downward flips and those of more than +1 are very rare on the plateau. Thus, a good (first order) approximation for $D_x$ is as follows, where $prob(D_x=j)$ is the probability that a flip at $x$ is of size $j$. \begin{eqnarray*} D_x & = & \sum_{j=-\LL}^{\LL} \ j\cdot prob(D_x=j) ~~~=~~~ prob(D_x=1) \end{eqnarray*} Hence, \begin{eqnarray*} prob(D_x=1) & = & \frac{\L-S(x)}{A\cdot \N} \end{eqnarray*} That is, on the plateau the probability of making a flip of size $+1$ may be directly proportional to $\L - S(x)$, the average number of clauses remaining unsatisfied and inversely proportional N, to the number of variables. A similar analysis and result can be given for $prob(D_x=j+1)$ in the hill-climbing region $H_j$, which would explain the model (\ref{eq-model-hc}) proposed in \secref{sec-hc}. If our theoretical conjecture is correct, it can be used to show that the mean number of flips on successful tries will be proportional to ${\rm N} \ln {\rm N}$. Further investigation, both experimental and theoretical, will be needed to determine the accuracy of this prediction. Our conjectures in this section should be seen as conjectures as to what a formal theory of \GSAT's search might look like, and should be useful in determining results such as average runtime and the optimal setting for a parameter like Max-flips. In addition, if we can develop a model of \GSAT's search in which $prob(D_x=j)$ is related to the number of unsatisfied clauses and N as in the above equation, then the experimentally observed exponential behaviour and linear scaling of the score will follow immediately. \section{Related Work} \label{sec-related} Prior to the introduction of \GSAT\ in \cite{selman-gsat}, a closely related set of procedures were studied by Gu~\cite{gu}. These procedures have a different control structure to \GSAT\ which allows them, for instance, to make sideways moves when upwards moves are possible. This makes it difficult to compare our results directly. Nevertheless, we are confident that the approach taken here would apply equally well to these procedures, and that similar results could be expected. Another ``greedy algorithm for satisfiability'' has been analysed in \cite{greedy-alg}, but our results are not directly applicable to it because, unlike GSAT, it disallows sideways flips. In \cite{gensat} we describe an empirical study of \GenSAT, a family of procedures related to \GSAT. This study focuses on the importance of randomness, greediness and hill-climbing for the effectiveness of these procedures. In addition, we determine how performance depends on parameters like Max-tries and Max-flips. We showed also that certain variants of \GenSAT\ could outperform \GSAT\ on random problems. It would be very interesting to perform a similar analysis to that given here of these closely related procedures. \GSAT\ is closely related to simulated annealing \cite{laarhoven1} and the Metropolis algorithm, which both use greedy local search with a randomised method of allowing non-optimal flips. Theoretical work on these algorithms has not applied to \SAT\ problems, for example \cite{jerrum-cliques,jerrum-sorkin}, while experimental studies of the relationship between \GSAT\ and simulated annealing have as yet only reached tentative conclusions \cite{selman-kautz-93,spears-sa}. Procedures like \GSAT\ have also been successfully applied to constraint satisfaction problems other than satisfiability. For example,~\cite{minton-heuristic-repair} proposed a greedy local search procedure which performed well scheduling observations on the Hubble Space Telescope, and other constraint problems like the million-queens, and 3-colourability. It would be very interesting to see how the results given here map across to these new problem domains. \section{Conclusions} \label{sec-conclusions} We have described an empirical study of search in \GSAT, an approximation procedure for satisfiability. We performed detailed analysis of the two basic phases of \GSAT's search, an initial period of fast hill-climbing followed by a longer period of plateau search. We have shown that the hill-climbing phases can be broken down further into a number of distinct phases each corresponding to progressively slower climbing, and each phase lasting twice as long as the last. We have also shown that, in certain well defined problem classes, the average behaviour of certain important features of \GSAT's search (the average score and the average branching rate at a given point) scale in a remarkably simple way with the problem size We have also demonstrated that the behaviour of these features can be modelled very well by simple exponential decay, both in the plateau and in the hill-climbing phase. Finally, we used our experiments to conjecture various properties ({\it eg.} the probability of making a flip of a certain size) that will be useful in a theoretical analysis of \GSAT. These results illustrate how carefully performed experiments can be used to guide theory, and how computers have an increasingly important r\^{o}le to play in the analysis of algorithms. \acks{This research is supported by a SERC Postdoctoral Fellowship to the first author and a HCM Postdoctoral fellowship to the second. We thank Alan Bundy, Ian Green, and the members of the Mathematical Reasoning Group for their constructive comments and for the quadrillion CPU cycles donated to these and other experiments from SERC grant GR/H/23610. We also thank Andrew Bremner, Judith Underwood, and the reviewers of this journal for other help.} \vskip 0.2in \bibliographystyle{theapa} \begin{thebibliography}{} \bibitem[\protect\BCAY{Cheeseman, Kanefsky, \BBA\ Taylor}{Cheeseman et~al.}{1991}]{cheeseman-hard} Cheeseman, P., Kanefsky, B., \BBA\ Taylor, W. \BBOP1991\BBCP. \newblock \BBOQ Where the really hard problems are\BBCQ\ \newblock In {\Bem Proceedings of the 12th IJCAI}, \BPGS\ 163--169. International Joint Conference on Artificial Intelligence. \bibitem[\protect\BCAY{Crawford \BBA\ Auton}{Crawford \BBA\ Auton}{1993}]{crawford-auton} Crawford, J.\BBACOMMA\ \BBA\ Auton, L. \BBOP1993\BBCP. \newblock \BBOQ {Experimental} results on the crossover point in satisfiability problems\BBCQ\ \newblock In {\Bem Proceedings of the Eleventh National Conference on Artificial Intelligence}, \BPGS\ 21--27. AAAI Press/The MIT Press. \bibitem[\protect\BCAY{Gent \BBA\ Walsh}{Gent \BBA\ Walsh}{1993}]{gensat} Gent, I.~P.\BBACOMMA\ \BBA\ Walsh, T. \BBOP1993\BBCP. \newblock \BBOQ {Towards} an {Understanding} of {Hill-climbing} {Procedures} for {SAT}\BBCQ\ \newblock In {\Bem Proceedings of the Eleventh National Conference on Artificial Intelligence}, \BPGS\ 28--33. AAAI Press/The MIT Press. \bibitem[\protect\BCAY{Gent \BBA\ Walsh}{Gent \BBA\ Walsh}{1992}]{rp605} Gent, I.~P.\BBACOMMA\ \BBA\ Walsh, T. \BBOP1992\BBCP. \newblock \BBOQ The enigma of {SAT} hill-climbing procedures\BBCQ\ \newblock Research paper\ 605, Dept. of Artificial Intelligence, University of Edinburgh. \bibitem[\protect\BCAY{Gu}{Gu}{1992}]{gu} Gu, J. \BBOP1992\BBCP. \newblock \BBOQ Efficient local search for very large-scale satisfiability problems\BBCQ\ \newblock {\Bem SIGART Bulletin}, {\Bem 3\/}(1). \bibitem[\protect\BCAY{Hooker}{Hooker}{1993}]{hooker1} Hooker, J.~N. \BBOP1993\BBCP. \newblock \BBOQ Needed: An empirical science of algorithms\BBCQ\ \newblock \BTR, Graduate School of Industrial Administration, Carnegie Mellon University, Pittsburgh PA. \bibitem[\protect\BCAY{Jerrum}{Jerrum}{1992}]{jerrum-cliques} Jerrum, M. \BBOP1992\BBCP. \newblock \BBOQ Large cliques elude the {Metropolis} process\BBCQ\ \newblock {\Bem Random Structures and Algorithms}, {\Bem 3\/}(4), 347--359. \bibitem[\protect\BCAY{Jerrum \BBA\ Sorkin}{Jerrum \BBA\ Sorkin}{1993}]{jerrum-sorkin} Jerrum, M.\BBACOMMA\ \BBA\ Sorkin, G. \BBOP1993\BBCP. \newblock \BBOQ Simulated annealing for graph bisection\BBCQ\ \newblock \BTR\ ECS-LFCS-93-260, Department of Computer Science, University of Edinburgh. \bibitem[\protect\BCAY{Koutsoupias \BBA\ Papadimitriou}{Koutsoupias \BBA\ Papadimitriou}{1992}]{greedy-alg} Koutsoupias, E.\BBACOMMA\ \BBA\ Papadimitriou, C.~H. \BBOP1992\BBCP. \newblock \BBOQ On the greedy algorithm for satisfiability\BBCQ\ \newblock {\Bem Information Processing Letters}, {\Bem 43}, 53--55. \bibitem[\protect\BCAY{Larrabee \BBA\ Tsuji}{Larrabee \BBA\ Tsuji}{1992}]{larrabee-tsuji} Larrabee, T.\BBACOMMA\ \BBA\ Tsuji, Y. \BBOP1992\BBCP. \newblock \BBOQ Evidence for a {Satisfiability} {Threshold} for {Random} {3CNF} {Formulas}\BBCQ\ \newblock \BTR\ UCSC-CRL-92-42, {Baskin} {Center} for Computer Engineering and Information Sciences, {University of California}, {Santa Cruz}. \bibitem[\protect\BCAY{McGeoch}{McGeoch}{1986}]{mcgeoch1} McGeoch, C. \BBOP1986\BBCP. \newblock {\Bem {Experimental} {Analysis} of {Algorithms}}. \newblock Ph.D.\ thesis, Carnegie Mellon University. \newblock Also available as CMU-CS-87-124. \bibitem[\protect\BCAY{Minton, Johnston, Philips, \BBA\ Laird}{Minton et~al.}{1990}]{minton-heuristic-repair} Minton, S., Johnston, M.~D., Philips, A.~B., \BBA\ Laird, P. \BBOP1990\BBCP. \newblock \BBOQ Solving large-scale constraint satisfaction and scheduling problems using a heuristic repair method\BBCQ\ \newblock In {\Bem AAAI-90, Proceedings Eighth National Conference on Artificial Intelligence}, \BPGS\ 17--24. AAAI Press/MIT Press. \bibitem[\protect\BCAY{Mitchell, Selman, \BBA\ Levesque}{Mitchell et~al.}{1992}]{mitchell-hard-easy} Mitchell, D., Selman, B., \BBA\ Levesque, H. \BBOP1992\BBCP. \newblock \BBOQ Hard and easy distributions of {SAT} problems\BBCQ\ \newblock In {\Bem Proceedings, 10th National Conference on Artificial Intelligence}. AAAI Press/The MIT Press. \bibitem[\protect\BCAY{Selman \BBA\ Kautz}{Selman \BBA\ Kautz}{1993a}]{gsat-ext} Selman, B.\BBACOMMA\ \BBA\ Kautz, H. \BBOP1993a\BBCP. \newblock \BBOQ Domain-independent extensions to {GSAT}: Solving large structured satisfiability problems\BBCQ\ \newblock In {\Bem Proceedings, IJCAI-93}. International Joint Conference on Artificial Intelligence. \bibitem[\protect\BCAY{Selman \BBA\ Kautz}{Selman \BBA\ Kautz}{1993b}]{selman-kautz-93} Selman, B.\BBACOMMA\ \BBA\ Kautz, H. \BBOP1993b\BBCP. \newblock \BBOQ An empirical study of greedy local search for satisfiability testing\BBCQ\ \newblock In {\Bem Proceedings of the Eleventh National Conference on Artificial Intelligence}, \BPGS\ 46--51. AAAI Press/The MIT Press. \bibitem[\protect\BCAY{Selman, Levesque, \BBA\ Mitchell}{Selman et~al.}{1992}]{selman-gsat} Selman, B., Levesque, H., \BBA\ Mitchell, D. \BBOP1992\BBCP. \newblock \BBOQ A new method for solving hard satisfiability problems\BBCQ\ \newblock In {\Bem Proceedings, 10th National Conference on Artificial Intelligence}. AAAI Press/The MIT Press. \bibitem[\protect\BCAY{Spears}{Spears}{1993}]{spears-sa} Spears, W.~M. \BBOP1993\BBCP. \newblock \BBOQ Simulated annealing for hard satisfiability problems\BBCQ\ \newblock \BTR\ AIC-93-015, AI Center, Naval Research Laboratory. \bibitem[\protect\BCAY{van Laarhoven \BBA\ Aarts}{van Laarhoven \BBA\ Aarts}{1987}]{laarhoven1} van Laarhoven, P.\BBACOMMA\ \BBA\ Aarts, E. \BBOP1987\BBCP. \newblock {\Bem Simulated Annealing: Theory and Applications}. \newblock D. Reidel Publishing Company, Dordrecht, Holland. \end{thebibliography} \end{document}