\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 each screen tile as a unique combination of 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 generate transition relations for four possible move directions of an agent,
for all screen tiles. There are three type of transition relations, namely: a
one-tile relation (changes only one tile), a two-tile relation (changes only
two tiles) and a three-tile relation (transforms three tiles per transition
simultaneously). In order to generate transition relations, we iterate through
a screen and for each tile we check neighbouring space with the purpose of
generating only the relevant relations. For example, if we consider a tile in
the top-left corner, there is no need to generate one or two-tiled transition
relations which can transform tiles to the left or to the right of that given
tile. For each possible direction of agent movement, we define a $\delta$ and a
$\gamma$ variables which represent the change in coordinate values respectively
for the next position and the position next to the next position.
$$\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 following tile update functions: $next(i_1)$, $next'(i_1,i_2)$
$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)=\left\{\begin{array}{lp{2pt}l}
	(agent) & \text{if } & i_1=agent\\
	(targetagent) & \text{if } & i_1=targetagent\\
\end{array}\right.$$

$$next'(i_1, i_2)=\left\{\begin{array}{lp{2pt}l}
	(agent, free) & \text{if } & i_1=free \wedge i_2=agent\\
	(agent, target) & \text{if } & i_1=free \wedge i_2=targagent\\
	(targagent, free) & \text{if } & i_1=target \wedge i_2=agent\\
    (targagent, target) & \text{if } & i_1=target \wedge i_2=targagent\\
	(agent, box) & \text{if } & i_1=agent \wedge i_2=box\\
	(agent, targbox) & \text{if } & i_1=agent \wedge i_2=targbox\\
	(targagent, box) & \text{if } & i_1=targagent \wedge i_2=box\\
	(targagent, targbox) & \text{if } & i_1=targagent \wedge i_2=targbox\\
\end{array}\right.$$

$$next''(i_1, i_2, i_3)=\left\{\begin{array}{lp{2pt}l}
	(agent, box, box) & \text{if } &
		i_1=agent \wedge i_2=box \wedge i_3=box\\
	(agent, box, targbox) & \text{if } &
		i_1=agent \wedge i_2=box \wedge i_3=targbox\\
	(targagent, box, box) & \text{if } &
		i_1=targetagent \wedge i_2=box \wedge i_3=box\\
	(targagent, box, targbox) & \text{if } &
		i_1=targagent \wedge i_2=box \wedge i_3=targbox\\
	(agent, box, free) & \text{if } &
		i_1=free \wedge i_2=agent \wedge i_3=box\\
	(agent, targbox, free) & \text{if } &
		i_1=free \wedge i_2=targagent \wedge i_3=box\\
	(agent, box, target) & \text{if } &
		i_1=free \wedge i_2=agent \wedge i_3=targbox\\
	(agent, targbox, target) & \text{if } &
		i_1=free \wedge i_2=targagent \wedge i_3=targbox\\
	(targagent, box, free) & \text{if } &
		i_1=targetagent \wedge i_2=targetbox \wedge i_3=target\\
	(targagent, targbox, free) & \text{if } &
		i_1=target \wedge i_2=targagent \wedge i_3=box\\
	(targagent, box, target) & \text{if } &
		i_1=target \wedge i_2=agent \wedge i_3=targbox\\
	(targagent, targbox, target) & \text{if } &
		i_1=target \wedge i_2=targagent \wedge i_3=targbox\\
\end{array}\right.$$

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

\subsection{Algorithm}
We use the standard optimized reachability algorithm to solve a screen but
added a goal condition that breaks the loop. When the loop breaks prematurely
it means a solution is found. If the full loop continues until the entire state
space is searched and the break condition is not met it means there is no
solution.

\begin{algorithm}[H]
	\KwIn{I, Initial state BDD}
	\KwIn{$R_i$, List of transition BDDs}
	\KwIn{G, Goal BDD}
	$V_{old}\leftarrow BDDempty$\;
	$V_{new}\leftarrow I$\;
	\While{$V_{new}\neq V_{old}$}{
		$V_{old}\leftarrow V_{new}$\;
		\ForEach{$R_i$}{
			$V_{new}\leftarrow BDDapply(\vee, V_{new}, BDDrelprod(V_{new}, R_i)$\;
		}
		\lIf{$BDDsatcount(BDDand(G, V_{new}))>0$}{$break$}
	}
\end{algorithm}

\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}

To encode the screen the tiles are numbered from left to right from top to
bottom (in a convenient coordinate-like manner). In order to translate the
initial screen into BDD representation, we iterate through a screen's tiles. We
use even BDD variable identifiers to represent states (screens). For convenient
BDD creation, we use sylvan cubes.As an example we can consider 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 transition
relations, even BDD variable identifiers act as state filters, whereas even
variable identifiers act as new values. Each transition changes only a limited
subset of the screen variables. 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}
