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}
- \caption{Peg solitaire board}\label{fig:sol}
+ \includegraphics[width=.2\linewidth]{eur.jpg}
+ \caption{English and European peg solitaire boards}\label{fig:sol}
\end{figure}
\begin{figure}[h]
\newpage
\subsection{Formalization}
-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 is defined as:
-$$\mathcal{P}=\left\{p\in \{0\ldots7\}^2|\text{where }\neg(
- (p_x<2\wedge p_y<2)\vee
+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)\right\}$$
+ (p_x<2\wedge p_y>4)\\
+ \}
+ \end{array}$$
-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.
+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 }\\
+ \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}$$
-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\}}
+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}$$
-Every iteration with $i>0$ we define with a function called $\mathcal{ITER}(i)$
-which for every move describes the updates for the positions. 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.
+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
\end{array}
$$
-The final state should be an inversion of the initial state. All holes should
-be empty except the middle hole $g$. $\mathcal{POST}$ is defined as follows:
+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}$$
-All of this together results in the following formula that is satisfiable if
+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
-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}$$
+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}
\begin{table}[h]
\centering
- \resizebox{.995\linewidth}{!}{
+ \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}$.
repositories / ar1516.git / commitdiff
