\subsection{Problem description}
Standard \emph{English Peg solitaire} is a single player game played on a board
with $33$ holes and is played with $32$ pegs. In the initial position all holes
-are occupied except for the middle hole. A traditional board is shown in
-Figure~\ref{fig:sol}. The goal of the game is to remove all but one peg on the
-middle position. The player can remove a peg by jumping over the peg
-orthogonally to a position two holes away. The middle peg is then removed from
-the board. To visualize board configurations we use the symbol $\circ$ for a
-position occupied by a peg and the symbol $\times$ by a position not occupied.
-The initial board configuration and possible moves are shown in
-Figure~\ref{fig:init}.
+except the middle hole are occupied by a peg as shown in Figure~\ref{fig:sol}.
+The goal of the game is to end up with one peg on the middle position. The
+player can remove a peg by jumping over the peg orthogonally to a position two
+holes away. The middle peg is then removed from the board. To visualize board
+configurations we use the symbol $\circ$ for a position occupied by a peg and
+the symbol $\times$ by a position not occupied. The initial board
+configuration and possible moves are shown in Figure~\ref{fig:init}.
Variations on the game exists with different board shapes such as triangles,
rotated squares or bigger crosses. There is also an alternative that makes the
end condition more flexible by allowing the last peg anywhere on the board.
-\begin{figure}[H]
+\begin{figure}[h]
\centering
\includegraphics[width=.2\linewidth]{board.jpg}
\caption{Peg solitaire board}\label{fig:sol}
\end{figure}
-\begin{figure}[H]
+\begin{figure}[h]
$$\xymatrix@1@=1pt@M=1pt{
& 0 & 1 & 2 & 3 & 4 & 5 & 6\\
0 & & & \circ & \circ & \circ & & & & & &
\caption{Initial board state and possible moves}\label{fig:init}
\end{figure}
+\newpage
\subsection{Formalization}
-Because in every move a peg is captured the game ends in exactly $31$ moves
-since there are $32$ pegs and one is left with a sole peg. A position $p$ means
-the $x$ and the $y$ coordinate as shown in Figure~\ref{fig:init}. Stating for a
-point $p$, $p_x$ or $p_y$ it means the respective $x$ and $y$ component of the
-position.\\
+Since in every move a peg is captured the game can only be won in exactly $31$
+moves because there are $32$ pegs in the starting condition and $1$ in the
+goal. Position $p=\langle x,y\rangle$ or $p_x,p_y$ means the $x$ and the $y$
+coordinate as shown in Figure~\ref{fig:init}.\\
-Set $\mathcal{P}$ is the set of all legal board positions and can be defined
-as:
+Set $\mathcal{P}$ is the set of all legal board positions and is defined as:
$$\mathcal{P}=\left\{p\in \{0\ldots7\}^2|\text{where }\neg(
(p_x<2\wedge p_y<2)\vee
(p_x>4\wedge p_y>4)\vee
(p_x>4\wedge p_y<2)\vee
(p_x<2\wedge p_y>4)\right\}$$
-Set $\mathcal{M}$ is the set of position triples that form a legal move. $s$
-denotes the start position, $m$ denotes the middle position and $e$ the final
-position.
+Set $\mathcal{M}$ is the set of all position triples that form a legal move.
+The elements $s,m,e$ denotes respectively the start, middle and end position of
+the move.
$$\begin{array}{l}
\mathcal{M}=\{(s,m,e)\in \{0\ldots7\}^3|\text{where }\\
\qquad\qquad(s_x=m_x\wedge m_x=e_x\wedge
(m_x=s_x+1\wedge e_x=m_x+1\vee m_x=s_x-1\wedge e_x=m_x-1)\\
\end{array}$$
-For every iteration $i\in\{0\ldots32\}$ and for every position $p\in \mathcal{P}$
-we create a variable representing the state of occupation. We also define
-$g=\langle3,3\rangle$ as being the middle position. With these definitions we
-can describe the initial state $\mathcal{INIT}$ as follows:
+For every iteration $i\in\{0\ldots32\}$ and for every position $p\in
+\mathcal{P}$ a variable representing the state of occupation is created. We
+also define $g=\langle3,3\rangle$ as being the middle position. With these
+definitions we can describe the initial state $\mathcal{INIT}$ as follows:
$$\neg i_0x_{g_x}y_{g_y}\wedge\bigwedge_{p\in \mathcal{P}\setminus\{g\}}
i_0x_{p_x}y_{p_y}$$
$$i_0x_{g_x}y_{g_y}\wedge\bigwedge_{p\in \mathcal{P}\setminus\{g\}}
\neg i_0x_{p_x}y_{p_y}$$
-All of this together in the following formula is satisfiable if
+All of this together results in the following formula that is satisfiable if
and only if there is a solution to English \textit{Peg solitaire}. The model
-that satisfies the formula is the sequence of moves to be performed to win a
-game.
+that satisfies the formula also represents the sequence of moves to be
+performed in order to win a game.
$$\mathcal{INIT}\wedge\left(\bigwedge_{i=1}^{31}\mathcal{ITER}(i)\right)
\wedge\mathcal{POST}$$
+\newpage
\subsection{Solution}
The conversion to SMT-Lib is trivial however on a $3.8Ghz$ processor running
\textsc{yices} it takes about $4$ hours and $15$ minutes to find the solution
listed in Table~\ref{tab:sol}.
-\begin{table}[H]
+
+\begin{table}[h]
\centering
-\input{src/4/a4.tex}
+ \resizebox{.995\linewidth}{!}{
+ \input{src/4/a4.tex}
+ }
\caption{Solution for \emph{English peg solitaire}}\label{tab:sol}
\end{table}
repositories / ar1516.git / commitdiff