\section{Solving solitaire}
\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
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.
The formalization in this report is focussed on \emph{English peg solitaire}.
\begin{figure}[h]
	\centering
	\includegraphics[width=.2\linewidth]{board.jpg}
	\includegraphics[width=.2\linewidth]{eur.jpg}
	\caption{English and European peg solitaire boards}\label{fig:sol}
\end{figure}

\begin{figure}[h]
	$$\xymatrix@1@=1pt@M=1pt{
		& 0 & 1 & 2 & 3 & 4 & 5 & 6\\
		0 & & & \circ & \circ & \circ & & & & & & 
			\circ\ar@{-)}[rr] & \circ & \times & \rightarrow &
				\times & \times & \circ\\
		1 & & & \circ & \circ & \circ\\
		2 & \circ & \circ & \circ & \circ & \circ & \circ & \circ & & & &
			\times & \circ & \circ\ar@{-)}[ll]& \rightarrow &
				\circ & \times & \times\\
		3 & \circ & \circ & \circ & \times & \circ & \circ & \circ\\
		4 & \circ & \circ & \circ & \circ & \circ & \circ & \circ & & & &
			\circ\ar@{-)}[dd] & & \times & & \times & & \circ\\
		5 & & & \circ & \circ & \circ & & & & & & 
			\circ & \rightarrow & \times & & \circ & \rightarrow& \times\\
		6 & & & \circ & \circ & \circ & & & & & & 
			\times & & \circ & & \circ\ar@{-)}[uu] & & \times\\
	}$$
	\caption{Initial board state and possible moves}\label{fig:init}
\end{figure}

\newpage
\subsection{Formalization}
Set $\mathcal{P}$ is the set of all legal board positions $p$ and is defined
as:
$$\begin{array}{l}
		\mathcal{P}=\{p\in \{0\ldots7\}^2|\text{where}\\
	\qquad\qquad\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)\\
	\}
	\end{array}$$

Set $\mathcal{M}$ is the set of all triples $(s, m, e)$ that form a legal move.
Respectively the elements of the triples denote the start, middle and end
position and the set is defined as:
$$\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_y=s_y+1\wedge e_y=m_y+1\vee m_y=s_y-1\wedge e_y=m_y-1)\vee\\
	\qquad\qquad(s_y=m_y\wedge m_y=e_y\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}$$

When there are $n$ holes in the board then there are exactly $n-1$ moves to win
a game since in every move we can remove precisely $1$ peg.  For every
iteration $i\in\{0\ldots n-1\}$ and for every position $p\in \mathcal{P}$ a
variable representing the state of occupation is created. There is also a $h\in
P$ defined that represents the initial hole and a $g\in P$ that defines the
goal position. In \emph{English peg solitaire} $h=g=\langle 3,3\rangle$. With
these definitions we can describe the initial state $\mathcal{INIT}$ as
follows:
$$\neg i_0x_{h_x}y_{h_y}\wedge\bigwedge_{p\in \mathcal{P}\setminus\{h\}}
i_0x_{p_x}y_{p_y}$$

The following formula called $\mathcal{ITER}(i)$ defines all iterations $i>0$.
Only the positions involved in the move are updated when the rest stay the
same. Part $(1)$ of the formula describes the preconditions for a move to be
valid. $(2)$ describes the result of the move and $(3)$ expresses the
invariability of the other positions.
$$\begin{array}{llr}
	\bigvee_{(s,m,e)\in M} \Biggl[& 
	i_{i-1}x_{s_x}y_{s_y}\wedge
	i_{i-1}x_{m_x}y_{m_y}\wedge
	\neg i_{i-1}x_{e_x}y_{e_y}\wedge & (1)\\
	& \neg i_{i}x_{s_x}y_{s_y}\wedge
		\neg i_{i}x_{m_x}y_{m_y}\wedge
		i_{i}x_{e_x}y_{e_y}\wedge & (2)\\
	& \bigwedge_{o\in \mathcal{P}\setminus\{s,m,e\}}
		i_ix_{o_x}y_{o_y}=i_{i-1}x_{o_x}y_{o_y}\quad\Biggr] & (3)
\end{array}
$$

The final state should a sole peg on position $g$. $\mathcal{POST}$ is defined
as follows:
$$i_0x_{g_x}y_{g_y}\wedge\bigwedge_{p\in \mathcal{P}\setminus\{g\}}
\neg i_0x_{p_x}y_{p_y}$$

The following formula ties this together into a formula that is satisfiable if
and only if there is a solution to English \textit{Peg solitaire}. The model
satisfying the formula represents the sequence of moves to be performed in
order to win a game.
$$\mathcal{INIT}\wedge
\mathcal{POST}\wedge\bigwedge_{i=1}^{31}\mathcal{ITER}(i)$$

\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}. \textsc{z3} finds a solution in $10$ minutes and
$37$ seconds.

\begin{table}[h]
	\centering
	\resizebox{.75\linewidth}{!}{
		\input{src/4/a4.tex}
	}
	\caption{Solution for \emph{English peg solitaire}}\label{tab:sol}
\end{table}

\subsection{Generalization}
Variations of the game can be solved with the same machinery my only changing
$\mathcal{P,M},g$ and $h$. For example \emph{European peg solitaire} can be
solved by updating $g,h,\mathcal{P}$ and $\mathcal{M}$ to $g',h',\mathcal{P'}$
and $\mathcal{M'}$ as follows:
$$\begin{array}{l}
		h'=(3,2), g'=(3,4)\\
		\mathcal{P'}=\mathcal{P}\cup\{\langle1,1\rangle,\langle5,5\rangle,
			\langle5,1\rangle,\langle1,5\rangle\}
\end{array}$$
And define $\mathcal{M'}$ the same as $\mathcal{M}$ but using $\mathcal{P'}$
instead of $\mathcal{P}$.
