a2/4.tex

   1 \section{Solving solitaire}
   2 \subsection{Problem description}
   3 Standard \emph{English Peg solitaire} is a single player game played on a board
   4 with $33$ holes and is played with $32$ pegs. In the initial position all holes
   5 except the middle hole are occupied by a peg as shown in Figure~\ref{fig:sol}.
   6 The goal of the game is to end up with one peg on the middle position. The
   7 player can remove a peg by jumping over the peg orthogonally to a position two
   8 holes away. The middle peg is then removed from the board. To visualize board
   9 configurations we use the symbol $\circ$ for a position occupied by a peg and
  10 the symbol $\times$ by a position not occupied. The initial board
  11 configuration and possible moves are shown in Figure~\ref{fig:init}.
  12
  13 Variations on the game exists with different board shapes such as triangles,
  14 rotated squares or bigger crosses. There is also an alternative that makes the
  15 end condition more flexible by allowing the last peg anywhere on the board.
  16 \begin{figure}[h]
  17         \centering
  18         \includegraphics[width=.2\linewidth]{board.jpg}
  19         \caption{Peg solitaire board}\label{fig:sol}
  20 \end{figure}
  21
  22 \begin{figure}[h]
  23         $$\xymatrix@1@=1pt@M=1pt{
  24                 & 0 & 1 & 2 & 3 & 4 & 5 & 6\\
  25                 0 & & & \circ & \circ & \circ & & & & & &
  26                         \circ\ar@{-)}[rr] & \circ & \times & \rightarrow &
  27                                 \times & \times & \circ\\
  28                 1 & & & \circ & \circ & \circ\\
  29                 2 & \circ & \circ & \circ & \circ & \circ & \circ & \circ & & & &
  30                         \times & \circ & \circ\ar@{-)}[ll]& \rightarrow &
  31                                 \circ & \times & \times\\
  32                 3 & \circ & \circ & \circ & \times & \circ & \circ & \circ\\
  33                 4 & \circ & \circ & \circ & \circ & \circ & \circ & \circ & & & &
  34                         \circ\ar@{-)}[dd] & & \times & & \times & & \circ\\
  35                 5 & & & \circ & \circ & \circ & & & & & &
  36                         \circ & \rightarrow & \times & & \circ & \rightarrow& \times\\
  37                 6 & & & \circ & \circ & \circ & & & & & &
  38                         \times & & \circ & & \circ\ar@{-)}[uu] & & \times\\
  39         }$$
  40         \caption{Initial board state and possible moves}\label{fig:init}
  41 \end{figure}
  42
  43 \newpage
  44 \subsection{Formalization}
  45 Since in every move a peg is captured the game can only be won in exactly $31$
  46 moves because there are $32$ pegs in the starting condition and $1$ in the
  47 goal. Position $p=\langle x,y\rangle$ or $p_x,p_y$ means the $x$ and the $y$
  48 coordinate as shown in Figure~\ref{fig:init}.\\
  49
  50 Set $\mathcal{P}$ is the set of all legal board positions and is defined as:
  51 $$\mathcal{P}=\left\{p\in \{0\ldots7\}^2|\text{where }\neg(
  52         (p_x<2\wedge p_y<2)\vee
  53         (p_x>4\wedge p_y>4)\vee
  54         (p_x>4\wedge p_y<2)\vee
  55         (p_x<2\wedge p_y>4)\right\}$$
  56
  57 Set $\mathcal{M}$ is the set of all position triples that form a legal move.
  58 The elements $s,m,e$ denotes respectively the start, middle and end position of
  59 the move.
  60 $$\begin{array}{l}
  61         \mathcal{M}=\{(s,m,e)\in \{0\ldots7\}^3|\text{where }\\
  62         \qquad\qquad(s_x=m_x\wedge m_x=e_x\wedge
  63                         (m_y=s_y+1\wedge e_y=m_y+1\vee m_y=s_y-1\wedge e_y=m_y-1)\vee\\
  64         \qquad\qquad(s_y=m_y\wedge m_y=e_y\wedge
  65                         (m_x=s_x+1\wedge e_x=m_x+1\vee m_x=s_x-1\wedge e_x=m_x-1)\\
  66 \end{array}$$
  67
  68 For every iteration $i\in\{0\ldots32\}$ and for every position $p\in
  69 \mathcal{P}$ a variable representing the state of occupation is created. We
  70 also define $g=\langle3,3\rangle$ as being the middle position. With these
  71 definitions we can describe the initial state $\mathcal{INIT}$ as follows:
  72 $$\neg i_0x_{g_x}y_{g_y}\wedge\bigwedge_{p\in \mathcal{P}\setminus\{g\}}
  73 i_0x_{p_x}y_{p_y}$$
  74
  75 Every iteration with $i>0$ we define with a function called $\mathcal{ITER}(i)$
  76 which for every move describes the updates for the positions. Only the
  77 positions involved in the move are updated when the rest stay the same. Part
  78 $(1)$ of the formula describes the preconditions for a move to be valid. $(2)$
  79 describes the result of the move and $(3)$ expresses the invariability of the
  80 other positions.
  81 $$\begin{array}{llr}
  82         \bigvee_{(s,m,e)\in M} \Biggl[&
  83         i_{i-1}x_{s_x}y_{s_y}\wedge
  84         i_{i-1}x_{m_x}y_{m_y}\wedge
  85         \neg i_{i-1}x_{e_x}y_{e_y}\wedge & (1)\\
  86         & \neg i_{i}x_{s_x}y_{s_y}\wedge
  87                 \neg i_{i}x_{m_x}y_{m_y}\wedge
  88                 i_{i}x_{e_x}y_{e_y}\wedge & (2)\\
  89         & \bigwedge_{o\in \mathcal{P}\setminus\{s,m,e\}}
  90                 i_ix_{o_x}y_{o_y}=i_{i-1}x_{o_x}y_{o_y}\quad\Biggr] & (3)
  91 \end{array}
  92 $$
  93
  94 The final state should be an inversion of the initial state. All holes should
  95 be empty except the middle hole $g$. $\mathcal{POST}$ is defined as follows:
  96 $$i_0x_{g_x}y_{g_y}\wedge\bigwedge_{p\in \mathcal{P}\setminus\{g\}}
  97 \neg i_0x_{p_x}y_{p_y}$$
  98
  99 All of this together results in the following formula that is satisfiable if
 100 and only if there is a solution to English \textit{Peg solitaire}. The model
 101 that satisfies the formula also represents the sequence of moves to be
 102 performed in order to win a game.
 103 $$\mathcal{INIT}\wedge\left(\bigwedge_{i=1}^{31}\mathcal{ITER}(i)\right)
 104 \wedge\mathcal{POST}$$
 105
 106 \newpage
 107 \subsection{Solution}
 108 The conversion to SMT-Lib is trivial however on a $3.8Ghz$ processor running
 109 \textsc{yices} it takes about $4$ hours and $15$ minutes to find the solution
 110 listed in Table~\ref{tab:sol}.
 111
 112
 113 \begin{table}[h]
 114         \centering
 115         \resizebox{.995\linewidth}{!}{
 116                 \input{src/4/a4.tex}
 117         }
 118         \caption{Solution for \emph{English peg solitaire}}\label{tab:sol}
 119 \end{table}