\section{Solving solitaire}
-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.
+
+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}
+
+\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}
+
+\subsection{Formalization}
+Basically there are two possible formalization techniques we can use.
+Formalization per position and formalization per peg.
+
+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.
+
+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.
+
+\begin{lstlisting}[caption={Coordinate system},label={lst:coord}]
+ 0123456
+0 ooo
+1 ooo
+2ooooooo
+3ooooooo
+4ooooooo
+5 ooo
+6 ooo
+\end{lstlisting}
+
+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\}$. In
+this way we can describe the start position, where $i=0$, by the following
+formula meaning that all the positions are occupied except for the middle
+position with coordinate $(3,3)$:
+$$\neg i_0x_3y_3\wedge\bigwedge_{(x,y)\in P\setminus\{(3,3)\}}i_0x_xy_y$$
+
+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)\}$
+All iterations following that can be described as the following formula:
+
+\begin{align}
+\bigwedge^{I}_{i=1}
+ \bigvee_{(sx, sy)\in P}\bigvee_{(mx, my)\in P'}
+ \bigvee_{(ex, ey)\in P}\Bigl(
+ & 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)
+\end{align}
+
+To get a trace for a winning game we negate the final condition and add it to
+the formula:
+$$i_{31}x_3y_3\wedge\bigwedge_{(x,y)\in P\setminus\{(3,3)\}}\neg i_{31}x_xy_y$$
+
+\lstinputlisting[caption={Solution for peg solitaire},label={lst:sol}]
+ {./src/4/a4.tex}
repositories / ar1516.git / blobdiff