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 The formalization in this report is focussed on \emph{English peg solitaire}.
  17 \begin{figure}[h]
  18         \centering
  19         \includegraphics[width=.2\linewidth]{board.jpg}
  20         \includegraphics[width=.2\linewidth]{eur.jpg}
  21         \caption{English and European peg solitaire boards}\label{fig:sol}
  22 \end{figure}
  23
  24 \begin{figure}[h]
  25         $$\xymatrix@1@=1pt@M=1pt{
  26                 & 0 & 1 & 2 & 3 & 4 & 5 & 6\\
  27                 0 & & & \circ & \circ & \circ & & & & & &
  28                         \circ\ar@{-)}[rr] & \circ & \times & \rightarrow &
  29                                 \times & \times & \circ\\
  30                 1 & & & \circ & \circ & \circ\\
  31                 2 & \circ & \circ & \circ & \circ & \circ & \circ & \circ & & & &
  32                         \times & \circ & \circ\ar@{-)}[ll]& \rightarrow &
  33                                 \circ & \times & \times\\
  34                 3 & \circ & \circ & \circ & \times & \circ & \circ & \circ\\
  35                 4 & \circ & \circ & \circ & \circ & \circ & \circ & \circ & & & &
  36                         \circ\ar@{-)}[dd] & & \times & & \times & & \circ\\
  37                 5 & & & \circ & \circ & \circ & & & & & &
  38                         \circ & \rightarrow & \times & & \circ & \rightarrow& \times\\
  39                 6 & & & \circ & \circ & \circ & & & & & &
  40                         \times & & \circ & & \circ\ar@{-)}[uu] & & \times\\
  41         }$$
  42         \caption{Initial board state and possible moves}\label{fig:init}
  43 \end{figure}
  44
  45 \newpage
  46 \subsection{Formalization}
  47 Set $\mathcal{P}$ is the set of all legal board positions $p$ and is defined
  48 as:
  49 $$\begin{array}{l}
  50                 \mathcal{P}=\{p\in \{0\ldots7\}^2|\text{where}\\
  51         \qquad\qquad\neg((p_x<2\wedge p_y<2)\vee
  52         (p_x>4\wedge p_y>4)\vee
  53         (p_x>4\wedge p_y<2)\vee
  54         (p_x<2\wedge p_y>4)\\
  55         \}
  56         \end{array}$$
  57
  58 Set $\mathcal{M}$ is the set of all triples $(s, m, e)$ that form a legal move.
  59 Respectively the elements of the triples denote the start, middle and end
  60 position and the set is defined as:
  61 $$\begin{array}{l}
  62         \mathcal{M}=\{(s,m,e)\in \{0\ldots7\}^3|\text{where}\\
  63         \qquad\qquad(s_x=m_x\wedge m_x=e_x\wedge
  64                         (m_y=s_y+1\wedge e_y=m_y+1\vee m_y=s_y-1\wedge e_y=m_y-1)\vee\\
  65         \qquad\qquad(s_y=m_y\wedge m_y=e_y\wedge
  66                         (m_x=s_x+1\wedge e_x=m_x+1\vee m_x=s_x-1\wedge e_x=m_x-1)\\
  67         \}
  68 \end{array}$$
  69
  70 When there are $n$ holes in the board then there are exactly $n-1$ moves to win
  71 a game since in every move we can remove precisely $1$ peg.  For every
  72 iteration $i\in\{0\ldots n-1\}$ and for every position $p\in \mathcal{P}$ a
  73 variable representing the state of occupation is created. There is also a $h\in
  74 P$ defined that represents the initial hole and a $g\in P$ that defines the
  75 goal position. In \emph{English peg solitaire} $h=g=\langle 3,3\rangle$. With
  76 these definitions we can describe the initial state $\mathcal{INIT}$ as
  77 follows:
  78 $$\neg i_0x_{h_x}y_{h_y}\wedge\bigwedge_{p\in \mathcal{P}\setminus\{h\}}
  79 i_0x_{p_x}y_{p_y}$$
  80
  81 The following formula called $\mathcal{ITER}(i)$ defines all iterations $i>0$.
  82 Only the positions involved in the move are updated when the rest stay the
  83 same. Part $(1)$ of the formula describes the preconditions for a move to be
  84 valid. $(2)$ describes the result of the move and $(3)$ expresses the
  85 invariability of the other positions.
  86 $$\begin{array}{llr}
  87         \bigvee_{(s,m,e)\in M} \Biggl[&
  88         i_{i-1}x_{s_x}y_{s_y}\wedge
  89         i_{i-1}x_{m_x}y_{m_y}\wedge
  90         \neg i_{i-1}x_{e_x}y_{e_y}\wedge & (1)\\
  91         & \neg i_{i}x_{s_x}y_{s_y}\wedge
  92                 \neg i_{i}x_{m_x}y_{m_y}\wedge
  93                 i_{i}x_{e_x}y_{e_y}\wedge & (2)\\
  94         & \bigwedge_{o\in \mathcal{P}\setminus\{s,m,e\}}
  95                 i_ix_{o_x}y_{o_y}=i_{i-1}x_{o_x}y_{o_y}\quad\Biggr] & (3)
  96 \end{array}
  97 $$
  98
  99 The final state should a sole peg on position $g$. $\mathcal{POST}$ is defined
 100 as follows:
 101 $$i_0x_{g_x}y_{g_y}\wedge\bigwedge_{p\in \mathcal{P}\setminus\{g\}}
 102 \neg i_0x_{p_x}y_{p_y}$$
 103
 104 The following formula ties this together into a formula that is satisfiable if
 105 and only if there is a solution to English \textit{Peg solitaire}. The model
 106 satisfying the formula represents the sequence of moves to be performed in
 107 order to win a game.
 108 $$\mathcal{INIT}\wedge
 109 \mathcal{POST}\wedge\bigwedge_{i=1}^{31}\mathcal{ITER}(i)$$
 110
 111 \newpage
 112 \subsection{Solution}
 113 The conversion to SMT-Lib is trivial however on a $3.8Ghz$ processor running
 114 \textsc{yices} it takes about $4$ hours and $15$ minutes to find the solution
 115 listed in Table~\ref{tab:sol}. \textsc{z3} finds a solution in $10$ minutes and
 116 $37$ seconds.
 117
 118 \begin{table}[h]
 119         \centering
 120         \resizebox{.75\linewidth}{!}{
 121                 \input{src/4/a4.tex}
 122         }
 123         \caption{Solution for \emph{English peg solitaire}}\label{tab:sol}
 124 \end{table}
 125
 126 \subsection{Generalization}
 127 Variations of the game can be solved with the same machinery my only changing
 128 $\mathcal{P,M},g$ and $h$. For example \emph{European peg solitaire} can be
 129 solved by updating $g,h,\mathcal{P}$ and $\mathcal{M}$ to $g',h',\mathcal{P'}$
 130 and $\mathcal{M'}$ as follows:
 131 $$\begin{array}{l}
 132                 h'=(3,2), g'=(3,4)\\
 133                 \mathcal{P'}=\mathcal{P}\cup\{\langle1,1\rangle,\langle5,5\rangle,
 134                         \langle5,1\rangle,\langle1,5\rangle\}
 135 \end{array}$$
 136 And define $\mathcal{M'}$ the same as $\mathcal{M}$ but using $\mathcal{P'}$
 137 instead of $\mathcal{P}$.