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