\section{Solving solitaire}
\subsection{Problem description}
-Standard \emph{Peg solitaire} is a game played with marbles or pegs on a board
-with $33$ holes as displayed in Figure~\ref{lst:pegs}. In the Figure dots
-represent a peg and o's represent a empty hole. The goal is to end up with the
-last peg in the middle hole and all other pegs removed from the board.
-To achieve this you have make moves that capture another peg. You can capture
-another peg by finding a peg bordering it in a certain direction and on the
-other side there needs to be an empty spot. The four possible moves are
-displayed in Figure~\ref{lst:moves}.
-
-Since there is no such thing as an empty move we know the game is always
-finished in $31$ steps. This is because in the start position there are $32$
-pegs on the playing field, every move we remove one peg, thus requiring $31$
-moves to end up with only one peg.
+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}.
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. Instead of requiring the last peg to be in the
-middle of the board, the last peg can be anywhere on the board.
-
-\begin{lstlisting}[caption={Standard English peg solitaire starting
-position},label={lst:pegs}]
- ...
- ...
-.......
-...o...
-.......
- ...
- ...
-\end{lstlisting}
+end condition more flexible by allowing the last peg anywhere on the board.
+\begin{figure}[H]
+ \centering
+ \includegraphics[width=.2\linewidth]{board.jpg}
+ \caption{Peg solitaire board}\label{fig:sol}
+\end{figure}
-\begin{lstlisting}[caption={Moves in all possible directions},
-label={lst:moves}]
-right left down up
- . . o .
-..o->oo. o..->.oo . -> o . -> o
- o o . o
-\end{lstlisting}
+\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}
\subsection{Formalization}
-Basically there are two possible formalization techniques we can use.
-Formalization per position and formalization per peg.
+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.\\
-Formalization per position means that we keep track of all the board positions
-and model what the position would be in the next state considering all possible
-moves. Every move there are only three positions on the board that are updated.
-On the entire board there are only $76$ possible combinations of three
-positions that can result in a move. This means that the formalization results
-in a big disjunction of the $76$ different moves.
+Set $\mathcal{P}$ is the set of all legal board positions and can be 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\}$$
-The second method would be to formalize the game in means of the pegs. For
-every peg we keep track of the location and when the peg is removed we put them
-in the bin. In this way when we end up with only one peg with a valid winning
-location and the rest in the bin the game is over. Expected is that this method
-has a much higher branching factor. Moves always consist of two pegs. So for
-every move we have to check every combination of pegs and every direction. This
-means that when there are $32$ pegs in the game there are
-$32\cdot31\cdot4=3968$ possible moves we should check. Ofcourse we can prune a
-lot of combinations very quickly because one of the pegs might already in the
-bin or the position of the pegs was not correct but it is still a very large
-branching factor. Because of the high branching factor we first attempt to
-solve the problem using the position based approach.
+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.
+$$\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}$$
-\begin{lstlisting}[caption={Coordinate system},label={lst:coord}]
- 0123456
-0 ooo
-1 ooo
-2ooooooo
-3ooooooo
-4ooooooo
-5 ooo
-6 ooo
-\end{lstlisting}
+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:
+$$\neg i_0x_{g_x}y_{g_y}\wedge\bigwedge_{p\in \mathcal{P}\setminus\{g\}}
+i_0x_{p_x}y_{p_y}$$
-To represent each position, as in Listing~\ref{lst:coord}, we assign per
-iteration $i$ for $i\in I$ where $I=\{0..32\}$ a variable $i_ix_xy_y$ per
-position where $(x,y)\in P$ where $P=\{(x,y) | (x,y)\text{ position on the
-board}\}$. So for example for the topmost row we have for $i=0$ the variables
-$\{i_0x_2y_0, i_0x_2y_1, i_0x_3y_0, i_0x_3y_1, i_0x_4y_0, i_0x_4y_1\}$.
+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.
+$$\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}
+$$
-To iterate over all moves we have to distinguish start and end positions from
-the middle position. All positions from $P$ are legal start or end positions
-but some are excluded from being a legal middle position of a move. Basically
-all positions in $P$ except for the corners are legal middle positions and
-therefore we define $P'$ that only contains legal middle positions and
-therefore $P'=P\setminus\{(2,0), (4,0), (0,2), (0,4), (6,2), (6,4), (2,6),
-(4,6)\}$
+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:
+$$i_0x_{g_x}y_{g_y}\wedge\bigwedge_{p\in \mathcal{P}\setminus\{g\}}
+\neg i_0x_{p_x}y_{p_y}$$
-\begin{align}
- \neg i_0x_3y_3\wedge\bigwedge_{(x,y)\in
-P\setminus\{(3,3)\}}\left(i_0x_xy_y\right)\wedge\\
- \bigwedge^{I}_{i=1}
- \bigvee_{(sx, sy)\in P}\bigvee_{(mx, my)\in P'}
- \bigvee_{(ex, ey)\in P}\Bigl(
- & \bigl((sy=my\wedge my=ey\wedge sx=mx+1\wedge mx=ex+1)\vee\\
- & \quad(sy=my\wedge my=ey\wedge sx=mx-1\wedge mx=ex-1)\vee\\
- & \quad(sx=mx\wedge mx=ex\wedge sy=my+1\wedge my=ey+1)\vee\\
- & \quad(sx=mx\wedge mx=ex\wedge sy=my-1\wedge my=ey-1)\bigr)\wedge\\
- & i_{i-1}x_{sx}y_{sy}\wedge
- i_{i-1}x_{mx}y_{my}\wedge
- \neg i_{i-1}x_{ex}y_{ey}\wedge\\
- & \neg i_{i}x_{sx}y_{sy}\wedge
- \neg i_{i}x_{mx}y_{my}\wedge
- i_{i}x_{ex}y_{ey}\wedge\\
- & \bigwedge_{(ox,oy)\in P\setminus\{(ex,ey),(mx,my),(sx,sy)\}}\left(
- i_ix_{ox}y_{oy}=i_{i-1}x_{ox}y_{oy}\right)\Bigr)\wedge\\
- i_{31}x_3y_3\wedge\bigwedge_{(x,y)\in P\setminus\{(3,3)\}}\neg i_{31}x_xy_y
-\end{align}
+All of this together in the following formula 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.
+$$\mathcal{INIT}\wedge\left(\bigwedge_{i=1}^{31}\mathcal{ITER}(i)\right)
+\wedge\mathcal{POST}$$
-\lstinputlisting[caption={Solution for peg solitaire},label={lst:sol}]
- {./src/4/a4.tex}
+\subsection{Solution}
+The conversion to SMT-Lib is trivial
repositories / ar1516.git / blobdiff