\section{Implementation}
\subsection{Screen encoding}
When parsed the sokoban screen is stripped of all walls and unreachable empty
spaces are removed. Moreover, a screen is rejected if either there are no
boxes, there is no agent or the number of boxes is not equal to the number of
targets.

Let $T=\{free,box,target,agent,targetagent,targetbox\}$ be the set of possible
states of a tile. Tiles are numbered and thus a sokoban screen is the set $F$
containing a $x_i\in T$ for every tile. We introduce a function $ord(x, y)$
that returns the tile number for a given $x$ and $y$ coordinate and a function
$iord(i)$ that does the reverse. To encode the
state we introduce an encoding function that encodes a state in three boolean
variables:
$$encode(t)=\begin{cases}
	001 & \text{if }t=free\\
	010 & \text{if }t=box\\
	011 & \text{if }t=target\\
	100 & \text{if }t=targetbox\\
	101 & \text{if }t=agent\\
	110 & \text{if }t=agentbox
\end{cases}$$

This means that the encoding of a screen takes $3*|F|$ variables.

\subsection{Transition encoding}
We introduce a variable denoting the intended direction of movement $m \in
\{\text{up}, \text{down}, \text{left}, \text{right}\}$. Per move we define a
$\delta$ and $\gamma$ variable which represent the change in coordinate value
respectively for the next position and the position next to the next postition.
$$\delta_{(x,y)}(m)=\begin{cases}
	(x-1, y) & \text{if } m = left\\
	(x+1, y) & \text{if } m = right\\
	(x, y+1) & \text{if } m = down\\
	(x, y-1) & \text{if } m = up\\
\end{cases}\quad
\gamma{(x,y)}(m)=\begin{cases}
	(x-2, y) & \text{if } m = left\\
	(x+2, y) & \text{if } m = right\\
	(x, y+2) & \text{if } m = down\\
	(x, y-2) & \text{if } m = up\\
\end{cases}$$

We define the tile update function $next(i_1, i_2, i_3)$ where $i_1$ contains
the agent and $i_2$ and $i_3$ are adjacent to it in some direction.
$$next(i_1, i_2, i_3)=\left\{\begin{array}{lp{2pt}l}
% Three state transitions
	(free, agent, box) & \text{if } & 
		i_1=agent \wedge i_2=box \wedge i_3=free\\
	(target, agent, box) & \text{if } & 
		i_1=targetagent \wedge i_2=box \wedge i_3=free\\
	(free, targetagent, box) & \text{if } &
		i_1=agent \wedge i_2=targetbox \wedge i_3=free\\
	(free, agent, targetbox) & \text{if } &
		i_1=agent \wedge i_2=box \wedge i_3=targetbox\\
	(target, targetagent, box) & \text{if } &
		i_1=targetagent \wedge i_2=targetbox \wedge i_3=free\\
	(target, agent, targetbox) & \text{if } &
		i_1=targetagent \wedge i_2=box \wedge i_3=target\\
	(free, targetagent, targetbox) & \text{if } &
		i_1=agent \wedge i_2=targetbox \wedge i_3=target\\
	(target, targetagent, targetbox) & \text{if } &
		i_1=targetagent \wedge i_2=targetbox \wedge i_3=target\\
% Two state transitions
	(free, agent, i_3) & \text{if } & i_1=agent \wedge i_2=free\\
	(free, targetagent, i_3) & \text{if } & i_1=agent \wedge i_2=target\\
	(target, agent, i_3) & \text{if } & i_1=targetagent \wedge i_2=free\\
	(target, targetagent, i_3) & \text{if } & i_1=targetagent \wedge i_2=target\\
% One state transitions
	(agent, i_2, i_3) & \text{if } & i_1=agent\\
	(targetagent, i_2, i_3) & \text{if } & i_1=targetagent\\
\end{array}\right.$$

\subsection{Goal encoding}
Encoding the goal state is very trivial. Just make sure all $target$ tiles are
$targetbox$ tiles.

\subsection{Example}
For example, take the toy screen shown as the first representation in
Listing~\ref{lst:toy}. When the screen is parsed the unreachable space is first
removed by detecting reachable space with the flood fill algorithm. This
results in the second representation in Listing~\ref{lst:toy}.

\lstinputlisting[label={lst:toy},caption={Example screen}]{toy.screen}

\subsubsection{Encoding}
To encode the screen the tiles are numbered from left to right from top to
bottom. Thus resulting in $i_1=agent, i_2=box, i_3=target$. When we translate
these numbers to sylvan-sane variables we get the following bdd shown in
Figure~\ref{fig:toy}. Variables $0, 2, 4$ represent $i_1$, $6, 8, 10$ represent
$i_2$ and lastly $12, 14, 16$ represents $i_3$.
\begin{figure}[p]
	\centering
	\includegraphics[width=\textwidth]{toy.png}
	\caption{Initial state encoding of the example~\label{fig:toy}}
\end{figure}

Encoding the goal state happens in a similar way. The algorithm basically
states that all $target$ positions should be $boxtarget$. This is results in
the BDD shown in Figure~\ref{fig:toy2}.

\begin{figure}[p]
	\centering
	\includegraphics[width=.5\textwidth]{toy2.png}
	\caption{Goal state encoding of the example~\label{fig:toy2}}
\end{figure}

Finally encoding the transitions already results in a long list of complicated
BDDs that each encode a possible move in all possible directions. In this
example there is only one move possible in the first state, thus all moves
except for the one move result in a relative product that is empty. For example
the sub-BDD that encodes the first position only looks is visualized in
Figure~\ref{fig:toy3}. The only satisfying assignment is that $0, 2, 4$ hold
the values $1, 0, 1$ thus encoding man and the variables $1, 3, 5$ holding the
values $0, 0, 1$ thus encoding free.

\begin{figure}[p]
	\centering
	\includegraphics[width=.8\textwidth]{toy3.png}
	\caption{Sub-BDD of a move~\label{fig:toy3}}
\end{figure}

\subsubsection{Results}
