href="http://nobi.ethz.ch/febi/ex_search_paper/paper.html#Avis92">[Avis 92]</A>, 
which has been used to exhaustively enumerate all configurations in a variety of 
combinatorial problems, including: vertices of polyhedra, triangulations, 
spanning trees, topological orderings. The idea is to use greedy local 
optimization algorithms as can be found for most problems. A greedy algorithms g 
is a mapping g: S -&gt; S from the state space into itself. The trajectories of 
g are free of cycles, so they form a forest. Each fix point of g, i.e. each sink 
of a g-trajectory, is the root of one tree. If it is possible to efficiently 
enumerate all these roots as an initialization step, then a backtrack search 
starting from each root becomes an exhaustive enumeration of the entire space. 
Backtracking can even dispense with a stack, because the function g always 
points to the predecessor of any node. 
<P>Whereas DFS, in the image of the labyrinth, is a policy for quickly 
penetrating as deeply as possible, its cautious partner breadth-first search 
(BFS) can be likened to a wave propagating through the labyrinth at equal speed 
in all directions. The memory cost of maintaining the wave front is significant, 
since all states in the front must be stored in their entirety. Combinations of 
DFS and BFS can be used to shape the wave front and to focus the search in a 
promising direction, an aspect often used in heuristic search. 
<P>The traversals above respect locality to various extents. DFS, while 
advancing and when backing up, always steps from one state to an adjacent state. 
BFS also moves to an adjacent state whenever it expands the wave front, and 
although states within the front need not be adjacent, they obey some locality 
in that they are concentric from the root. In contrast, other ``traversals'' 
sequence the states ``at random'', ignoring the graph structure of a space. 
There are two reasons for such a counter-intuitive approach. 
<P>First, there are situations where we expect little or no pruning of the space 
will occur at search time, and we are resigned to visit all states without 
exception, in arbitrary order. For many challenging problem classes, the effort 
required to solve one instance is comparable to solving all instances in the 
class. One suspects, for example, that determining the value of the initial 
position in chess requires knowing the value of very many chess positions - the 
one instance ``initial position'' is comparable in difficulty to the class ``all 
positions''. Second, every state has some internal representation, and these 
representations can be considered to be integers, or can be mapped to integers 
in an invertible way: given the integer, the state can be reconstructed. Such 
unique identifiers are called Goedel numbers in honor of the famous logician who 
used this technique to prove incompleteness theorems of mathematical logic. When 
states are identified with integers, the easiest way to list them all is from 
smallest to largest, even if the numerical order of the Goedel numbers has no 
relation to the graph structure. 
<P>Such chaotic traversals of the space have become standard, under the name of 
retrograde analysis, for solving games and puzzles (recall examples in section 
2). Pick any state of Merrils, for example, such as the one labeled ``Black to 
move loses'' in the picture at left. Without any further information we can 
construct an arbitrary predecessor state by ``unplaying'' a White move and 
labeling it ``White to move wins''. Backing up a won position is somewhat more 
elaborate, as the picture at right shows. Thus, starting from known values at 
the leaves of a game tree, repeated application of such minmax operations 
eventually propagates correct values throughout the entire space. <!--Figure: Backing up lost and won positions--><BR><BR><BR>
<CENTER><IMG alt="Figure 4" src="Exhaustive Search.files/figure_4_big.gif"> 
<BR><SMALL>Figure 3: Backing up lost and won positions</SMALL> </CENTER><BR><BR>
<P>Using retrograde analysis, the midgame and endgame state space of Merrils 
detailed in section 4, with 7.7 Billion positions, was calculated over a period 
of three years by a coalition of computers. <BR><BR><BR><A name=6></A>
<H3>6. Case Study: Merrils and its Verification</H3>
<P>Although the retrograde analysis mentioned above is the lion's share of a 
huge calculation, the case study of Merrils is not yet finished. The total state 
space of Merrils is roughly double this size, because the same board position 
represents two entirely different states depending on whether it occurs during 
the opening, while stones are being placed on the board, or during the mid- or 
endgame, while stones slide or jump. 
<P>It is interesting to compare the two state spaces: opening vs. midgame and 
endgame. The two spaces are superficially similar because each state is 
identified with a board position, most of which look identical in both spaces. 
The differences between the board positions that arise in the opening and the 
midgame are minor: the opening space contains states where a player has fewer 
than 3 stones, but lacks certain other states that can arise in the midgame. 
Thus, the two spaces are roughly of equal size, but their structure is entirely 
different. Whereas the midgame space contains many cycles, the opening space is 
a directed acyclic graph (dag) of depth exactly 18. If symmetries were ignored, 
the fanout would decreases from 24 at the root of this dag to about 7 at the 
leaves (not necessarily exactly 7 because of possible captures). Taking 
symmetries into account, the dag becomes significantly slimmer - for example, 
there are only four inequivalent first moves out of 24 possible. 
<P>The limited depth and fanout of the opening space suggests a forward search 
may be more efficient than a backward search. This is reinforced by the fact 
that the goal is not to determine the value of all positions that could arise in 
the opening, but to prove the conjecture that Merrils is a draw under optimal 
play by both parties. Thus, the effective fanout of the dag is further decreased 
by best-first heuristics. By first investigating moves known or guessed to be 
good, one can often prove the hoped-for result without having to consider poor 
moves. Experienced Merrils players know that at most one or two mills will be 
closed during a well-played opening. Thus one aims to prove the draw by opening 
play limited to reaching three midgame databases only: 9-9, 9-8, and 8-8. 
<P>The forward search chosen replaces the dag by a tree many of whose nodes 
represent the same state. For reasons of program optimization whose intricate, 
lengthy justification we omit, two auxiliary data structures supported this 
search. A database of opening positions at depth 8 plies, and a hash table of 
positions at 14 plies. Thus, whenever the same 14th-ply-state is reached along 
different move sequences (transpositions), all but the first search finds the 
correct value already stored. This is illustrated in the following picture of a 
tree constricted at the 14th ply. 
<P>The draw was proven with two minmax evaluations using the well-known 
alpha-beta algorithm <A 
href="http://nobi.ethz.ch/febi/ex_search_paper/paper.html#Knuth75">[Knuth 
75]</A>. One search proves that White, the first player to move, has at least a 
draw. The second search proves that Black has at least a draw. The effectiveness 
of alpha-beta is demonstrated by the fact that, of roughly 3.5 million positions 
at the 8 ply level, only 15'513 had to be evaluated to prove that White can hold 
the draw, and only 4'393 to prove that Black can hold the draw (the second 
player, Black, appears to have a small edge in Merrils). All others are pruned, 
i.e. can be eliminated as inferior without having been generated. This forward 
search took about 3 weeks of total run time on a Macintosh Quadra 800. <!--Figure: Analyzing the opening: a deep but narrow forward search--><BR><BR><BR>
<CENTER><IMG alt="Figure 5" src="Exhaustive Search.files/figure_5_big.gif"> 
<BR><SMALL>Figure 3: Analyzing the opening: a deep but narrow forward 
search</SMALL> </CENTER><BR><BR>
<P>How credible is the cryptic result ``Merrils is a draw'', obtained after 
three years of computation on a variety of machines that produced 10 Giga-Bytes 
of data? We undertook a most thorough verification of this result. Not because 
the Merrils draw is vital, but because the scope of this question greatly 
exceeds this particular problem. 
<P>Computer-aided proofs are becoming more important in mathematics and related 
branches of science - for example, they were essential for the four-color 
theorem, Ramsey theory or cellular-automata <A 
href="http://nobi.ethz.ch/febi/ex_search_paper/paper.html#Horgan93">[Horgan 
93]</A>. A common objection raised against computer proofs is that they cannot 
be understood, nor their correctness conclusively established by humans. Thus we 
took Merrils as a challenge to investigate the general issues and approaches to 
the problem of verifying computer proofs. 
<P>Computer-aided proofs typically lead to complex software packages, long 
run-times, and much data - three major sources of diverse errors. The latter 
fall into three categories: 
<OL>
  <LI><EM>Software errors</EM>: These may occur in the algorithms programmed for 
  the specific problem, or in the system software and tools used (compilers, 
  linkers, library programs). Although the latter errors are beyond the 
  programmer's direct control, he must be vigilant, because software that 
  handles everyday tasks reliably is often untested on files larger than usual. 
  <LI><EM>Hardware errors</EM>: The much-debated recent bug in the Pentium 
  microprocessor is a reminder that even arithmetic can't be relied on. Other 
  hardware is even less reliable. It is not uncommon for a bit to be flipped on 
  the disk, especially if the data is unused for long periods. This may be 
  caused by cosmic radiation, electric or magnetic fields. 
  <LI><EM>Handling errors</EM>: Long computations are seldom run without 
  interruption. Thus, the user gets involved in many error-prone chores such as 
  move data to different disks, compressing files or resuming computation on a 
  different platform. </LI></OL>
<P>Hardware and handling errors are easiest to detect. Consistency checks at 
run-time or thereafter will uncover handling errors and non-recurring hardware 
glitches. Redoing the entire computation using independent system software and 
compiler on a different machine should find any errors in the hardware or system 
software. This leaves software errors stemming directly from the proof code. The 
best method of uncovering these, is to develop a second proof using a different 
algorithm. If no other algorithm is known, a third party can independently write 
code based on the same algorithm. 
<P>The Merrils databases were verified repeatedly with different algorithms and 
on different machines. Errors of all types mentioned above were detected and 
corrected until no further errors surfaced. A first series of verifications 
merely checked that the values stored with the positions are locally consistent. 
The game-theoretic value of any position p must be the min or max of the values 
of the successors of p. Although local consistency everywhere is a strong 
endorsement, it does not guarantee correctness, as the following example shows. <!--Figure: Locally consistent values in cycles are not necessarily correct--><BR><BR><BR>
<CENTER><IMG alt="Figure 6" src="Exhaustive Search.files/figure_6_big.gif"> 
<BR><SMALL>Figure 3: Locally consistent values in cycles are not necessarily 
correct</SMALL> </CENTER><BR><BR>
<P>The diagram at left shows a subspace all of whose positions are drawn (D). If 
the 5 positions that contain a cycle of length 4 are alternatingly labeled loss 
(L) and win (W) for the player to move, as shown at right, everything is locally 
consistent. It is incorrect, however, because in Merrils, as in many games, 
endless repetition is declared a draw. This error, moreover, can propagate 
upwards and infect all predecessor positions. 
<P>Thus, a second series of verifications used as additional information the 
length of the shortest forced sequence that realizes the game-theoretic value of 
any position. When considering the position attributes: 0 = loss in 0 moves 
(terminal position), 1 = win in 1 move, 2 = loss in 2 moves, ..., 255 = draw 
(cycle), in addition to the game-theoretic value, the cycle with positions 
labeled L, D, L, D is no longer locally consistent and the error is detected. 
<P>The entire verification was run on an Intel Paragon parallel computer with 96 
processors, at the rate of about 50'000 positions verified per second. The 
largest database (8-7, 1'072'591'519 positions) required 400 minutes. 
<BR><BR><BR><A name=7></A>
<H3>7. Projects and Outlook</H3>
<P>In an attempt to explore the possibilities and limits of exhaustive search, 
we pursue a number of other problems that span a variety of applications and 
techniques. The following snapshots of ongoing projects illustrate the potential 
breadth of exhaustive search (see also <A 
href="http://nobi.ethz.ch/febi/ex_search_paper/paper.html#Nievergelt93">[Nievergelt 
93]</A>). <A name=7.1></A>
<H4>7.1. Using Heuristics to Trade Accuracy for Space and Time: Pawn endings in 
chess</H4>
<P>An irritating feature of many exhaustive search computations is the fact that 
the program will search large subspaces where human insight could tell at a 
glance that nothing will be found. Such expert knowledge is frequently found in 
problem domains that admit natural visualizations, where humans' powerful visual 
pattern recognition ability let's us say ``this doesn't look right'', even if we