a2/4.tex

   1 \section{Solving solitaire}
   2 \subsection{Problem description}
   3 Standard \emph{Peg solitaire} is a game played with marbles or pegs on a board
   4 with $33$ holes as displayed in Figure~\ref{lst:pegs}. In the Figure dots
   5 represent a peg and o's represent a empty hole. The goal is to end up with the
   6 last peg in the middle hole and all other pegs removed from the board.
   7 To achieve this you have make moves that capture another peg. You can capture
   8 another peg by finding a peg bordering it in a certain direction and on the
   9 other side there needs to be an empty spot. The four possible moves are
  10 displayed in Figure~\ref{lst:moves}.
  11
  12 Since there is no such thing as an empty move we know the game is always
  13 finished in $31$ steps. This is because in the start position there are $32$
  14 pegs on the playing field, every move we remove one peg, thus requiring $31$
  15 moves to end up with only one peg.
  16
  17 Variations on the game exists with different board shapes such as triangles,
  18 rotated squares or bigger crosses. There is also an alternative that makes the
  19 end condition more flexible.  Instead of requiring the last peg to be in the
  20 middle of the board, the last peg can be anywhere on the board.
  21
  22 \begin{lstlisting}[caption={Standard English peg solitaire starting
  23 position},label={lst:pegs}]
  24   ...
  25   ...
  26 .......
  27 ...o...
  28 .......
  29   ...
  30   ...
  31 \end{lstlisting}
  32
  33 \begin{lstlisting}[caption={Moves in all possible directions},
  34 label={lst:moves}]
  35 right     left      down      up
  36                      .    .    o    .
  37 ..o->oo.  o..->.oo   . -> o    . -> o
  38                      o    o    .    o
  39 \end{lstlisting}
  40
  41 \subsection{Formalization}
  42 Basically there are two possible formalization techniques we can use.
  43 Formalization per position and formalization per peg.
  44
  45 Formalization per position means that we keep track of all the board positions
  46 and model what the position would be in the next state considering all possible
  47 moves. Every move there are only three positions on the board that are updated.
  48 On the entire board there are only $76$ possible combinations of three
  49 positions that can result in a move. This means that the formalization results
  50 in a big disjunction of the $76$ different moves.
  51
  52 The second method would be to formalize the game in means of the pegs. For
  53 every peg we keep track of the location and when the peg is removed we put them
  54 in the bin. In this way when we end up with only one peg with a valid winning
  55 location and the rest in the bin the game is over. Expected is that this method
  56 has a much higher branching factor. Moves always consist of two pegs. So for
  57 every move we have to check every combination of pegs and every direction. This
  58 means that when there are $32$ pegs in the game there are
  59 $32\cdot31\cdot4=3968$ possible moves we should check. Ofcourse we can prune a
  60 lot of combinations very quickly because one of the pegs might already in the
  61 bin or the position of the pegs was not correct but it is still a very large
  62 branching factor. Because of the high branching factor we first attempt to
  63 solve the problem using the position based approach.
  64
  65 \begin{lstlisting}[caption={Coordinate system},label={lst:coord}]
  66   0123456
  67 0  ooo
  68 1  ooo
  69 2ooooooo
  70 3ooooooo
  71 4ooooooo
  72 5  ooo
  73 6  ooo
  74 \end{lstlisting}
  75
  76 To represent each position, as in Listing~\ref{lst:coord}, we assign per
  77 iteration $i$ for $i\in I$ where $I=\{0..32\}$ a variable $i_ix_xy_y$ per
  78 position where $(x,y)\in P$ where $P=\{(x,y) | (x,y)\text{ position on the
  79 board}\}$. So for example for the topmost row we have for $i=0$ the variables
  80 $\{i_0x_2y_0, i_0x_2y_1, i_0x_3y_0, i_0x_3y_1, i_0x_4y_0, i_0x_4y_1\}$.  In
  81 this way we can describe the start position, where $i=0$, by the following
  82 formula meaning that all the positions are occupied except for the middle
  83 position with coordinate $(3,3)$:
  84 $$\neg i_0x_3y_3\wedge\bigwedge_{(x,y)\in P\setminus\{(3,3)\}}i_0x_xy_y$$
  85
  86 To iterate over all moves we have to distinguish start and end positions from
  87 the middle position. All positions from $P$ are legal start or end positions
  88 but some are excluded from being a legal middle position of a move. Basically
  89 all positions in $P$ except for the corners are legal middle positions and
  90 therefore we define $P'$ that only contains legal middle positions and
  91 therefore $P'=P\setminus\{(2,0), (4,0), (0,2), (0,4), (6,2), (6,4), (2,6),
  92 (4,6)\}$
  93 All iterations following that can be described as the following formula:
  94
  95 \begin{align}
  96 \bigwedge^{I}_{i=1}
  97         \bigvee_{(sx, sy)\in P}\bigvee_{(mx, my)\in P'}
  98         \bigvee_{(ex, ey)\in P}\Bigl(
  99         & i_{i-1}x_{sx}y_{sy}\wedge
 100                 i_{i-1}x_{mx}y_{my}\wedge
 101                 \neg i_{i-1}x_{ex}y_{ey}\wedge\\
 102         & \neg i_{i}x_{sx}y_{sy}\wedge
 103                 \neg i_{i}x_{mx}y_{my}\wedge
 104                 i_{i}x_{ex}y_{ey}\wedge\\
 105         & \bigwedge_{(ox,oy)\in P\setminus\{(ex,ey),(mx,my),(sx,sy)\}}\left(
 106         i_ix_{ox}y_{oy}=i_{i-1}x_{ox}y_{oy}\right)\Bigr)
 107 \end{align}
 108
 109 To get a trace for a winning game we negate the final condition and add it to
 110 the formula:
 111 $$i_{31}x_3y_3\wedge\bigwedge_{(x,y)\in P\setminus\{(3,3)\}}\neg i_{31}x_xy_y$$
 112
 113 \lstinputlisting[caption={Solution for peg solitaire},label={lst:sol}]
 114         {./src/4/a4.tex}