\section{Implementation}
\subsection{Screen encoding}
When parsed the sokoban screen is stripped of all walls and unreachable empty
spaces are removed.

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. To encode the state we
introduce an encoding function that encodes a state in three boolean variables:
$$encode(t)=\begin{cases}
	000 & \text{if }t=wall\\
	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}\}$. 
%
%Let\\
%$\delta_{x}(x,m) =
%  \begin{cases}
%    (x+1) & \quad \text{if } m = left\\
%    (x-1) & \quad \text{if } m = right\\
%    x & \quad \text{otherwise}
%  \end{cases}$\quad
%$\delta'_{x}(x,m) =
%  \begin{cases}
%    (x-1) & \quad \text{if } m = left\\
%    (x+1) & \quad \text{if } m = right\\
%    x & \quad \text{otherwise}
%  \end{cases}$\\
%$\delta_{y}(y,m) =
%  \begin{cases}
%    (y+1) & \quad \text{if } m = up\\
%    (y-1) & \quad \text{if } m = down\\
%    y & \quad \text{otherwise}
%  \end{cases}$\quad
%$\delta'_{y}(y,m) =
%  \begin{cases}
%    (y-1) & \quad \text{if } m = up\\
%    (y+1) & \quad \text{if } m = down\\
%    y & \quad \text{otherwise}
%  \end{cases}$\\
%  $\gamma_{x}(x,m) =
%    \begin{cases}
%      (x+2) & \quad \text{if } m = left\\
%      (x-2) & \quad \text{if } m = right\\
%      x & \quad \text{otherwise}
%    \end{cases}$\quad
%  $\gamma_{y}(y,m) =
%    \begin{cases}
%      (y+2) & \quad \text{if } m = up\\
%      (y-2) & \quad \text{if } m = down\\
%      y & \quad \text{otherwise}
%    \end{cases}$
%
%%    "    x" <+ x <+ "_" <+ y <+ " = BoxOnTarget & (x" <+ (checkX p x) <+ "_" <+ (checkY p x  (y+1)) <+ " = Agent | x"
%%                            <+ (checkX p x) <+ "_" <+ (checkY p x  (y+1)) <+ " = AgentOnTarget) & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = Free | x" <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = Target) & move = Left: AgentOnTarget;",
%%                    "    x" <+ x <+ "_" <+ y <+ " = BoxOnTarget & (x" <+ (checkX p (x+1)) <+ "_" <+ (checkY p (x+1) y) <+ " = Agent | x"
%%                            <+ (checkX p (x+1)) <+ "_" <+ (checkY p (x+1) y) <+ " = AgentOnTarget) & (x" <+ (checkX p (x-1)) <+ "_" <+ (checkY p (x-1) y) <+ " = Free | x" <+ (checkX p (x-1)) <+ "_"
%%                            <+ (checkY p (x-1) y) <+ " = Target) & move = Up: AgentOnTarget;",
%%                    "    x" <+ x <+ "_" <+ y <+ " = BoxOnTarget & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = Agent | x"
%%                            <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = AgentOnTarget) & (x" <+ (checkX p x) <+ "_" <+ (checkY p x  (y+1)) <+ " = Free | x" <+ x <+ "_" <+ (checkY p x  (y+1)) <+ " = Target) & move = Right : AgentOnTarget;",
%%                    "    x" <+ x <+ "_" <+ y <+ " = BoxOnTarget & (x" <+ (checkX p (x-1)) <+ "_" <+ (checkY p (x-1) y) <+ " = Agent | x"
%%                            <+ (checkX p (x-1)) <+ "_" <+ (checkY p (x-1) y) <+ " = AgentOnTarget) & (x" <+ (checkX p (x+1)) <+ "_" <+ (checkY p (x+1) y) <+ " = Free | x" <+ (checkX p (x+1)) <+ "_"
%%                            <+ (checkY p (x+1) y) <+ " = Target) & move = Down : AgentOnTarget;",
%
%
%
%We define the tile update function $next(x_{i,j}), x_{i,j} \in F, \forall i,j \text{ s.t.} x_{i,j} \neq \perp$ as\\
%$
%next(x_{i,j}) =
%  \begin{cases}
%    \# & \quad \text{if } x_{i,j} = \#\\
%    @ & \quad \text{if } x_{i,j} = \_ \wedge (x_{\delta_{x}(i,m),\delta_{y}(j,m)} = @ \vee x_{\delta_{x}(i,m),\delta_{y}(j,m)} = +) \wedge x_{\delta_{x}(i,m),\delta_{y}(j,m)} \neq \perp\\
%    @ & \quad \text{if } x_{i,j} = \$ \wedge (x_{\delta_{x}(i,m),\delta_{y}(j,m)} = @ \vee x_{\delta_{x}(i,m),\delta_{y}(j,m)} = +)\\
%    & \quad \wedge (x_{\delta'_{x}(i,m),\delta'_{y}(j,m)} = \_ \vee x_{\delta'_{x}(i,m),\delta'_{y}(j,m)} = .)\\
%    & \quad \wedge x_{\delta_{x}(i,m),\delta_{y}(j,m)} \neq \perp \wedge x_{\delta'_{x}(i,m),\delta'_{y}(j,m)} \neq \perp\\
%    \$ & \quad \text{if } x_{i,j} = \_ \wedge (x_{\delta_{x}(i,m),\delta_{y}(j,m)} = \$ \vee x_{\delta_{x}(i,m),\delta_{y}(j,m)} = *)\\ & \quad \wedge (x_{\gamma_{x}(i,m),\gamma_{y}(j,m)} = @ \vee x_{\gamma_{x}(i,m),\gamma_{y}(j,m)} = +) \wedge x_{\delta_{x}(i,m),\delta_{y}(j,m)} \neq \perp \wedge x_{\gamma_{x}(i,m),\gamma_{y}(j,m)} \neq \perp\\
%    \_ & \quad \text{if } x_{i,j} = @ \wedge (x_{\delta_{x}(i,m),\delta_{y}(j,m)} = \_ \vee x_{\delta_{x}(i,m),\delta_{y}(j,m)} = .)\\
%    & \quad \vee ((x_{\delta_{x}(i,m),\delta_{y}(j,m)} = \$ \vee x_{\delta_{x}(i,m),\delta_{y}(j,m)} = *) \wedge \\
%    & \quad (x_{\gamma_{x}(i,m),\gamma_{y}(j,m)} = \_ \vee x_{\gamma_{x}(i,m),\gamma_{y}(j,m)} = .)) \\
%    & \quad x_{\delta_{x}(i,m),\delta_{y}(j,m)} \neq \perp \wedge x_{\gamma_{x}(i,m),\gamma_{y}(j,m)} \neq \perp\\
%    + & \quad x_{i,j} = . \wedge (x_{\delta_{x}(i,m),\delta_{y}(j,m)} = @ \vee x_{\delta_{x}(i,m),\delta_{y}(j,m)} = +) \wedge x_{\delta_{x}(i,m),\delta_{y}(j,m)} \neq \perp\\
%    + & \quad x_{i,j} = * \wedge (x_{\delta_{x}(i,m),\delta_{y}(j,m)} = @ \vee x_{\delta_{x}(i,m),\delta_{y}(j,m)} = +)\\
%    & \quad \wedge (x_{\delta'_{x}(i,m),\delta'_{y}(j,m)} = \_ \vee x_{\delta'_{x}(i,m),\delta'_{y}(j,m)} = .)\\
%    & \quad \wedge x_{\delta_{x}(i,m),\delta_{y}(j,m)} \neq \perp \wedge x_{\delta'_{x}(i,m),\delta'_{y}(j,m)} \neq \perp\\
%    * & \quad \text{if } x_{i,j} = . \wedge (x_{\delta_{x}(i,m),\delta_{y}(j,m)} = \$ \vee x_{\delta_{x}(i,m),\delta_{y}(j,m)} = *)\\
%    & \quad \wedge (x_{\gamma_{x}(i,m),\gamma_{y}(j,m)} = @ \vee x_{\gamma_{x}(i,m),\gamma_{y}(j,m)} = +)\\
%    & \quad \wedge x_{\delta_{x}(i,m),\delta_{y}(j,m)} \neq \perp \wedge x_{\gamma_{x}(i,m),\gamma_{y}(j,m)} \neq \perp\\
%    . & \quad x_{i,j} = + \wedge (x_{\delta_{x}(i,m),\delta_{y}(j,m)} = \_ \vee x_{\delta_{x}(i,m),\delta_{y}(j,m)} = .) \wedge x_{\delta_{x}(i,m),\delta_{y}(j,m)} \neq \perp\\
%    x_{i,j} & \quad \text{otherwise}\\
%  \end{cases}
%$
%\subsection{Goal}
%Let $G = \{z_{i,j} | z_{i,j} \in F, \forall i,j \text{ s.t.} z_{i,j} \in \{.,*\}\}$ be a subset of $F$.
%In order to check a sokoban field for a possible solution, we introduce the following invariant:\\
%$$\neg \bigwedge_{x \in G} (x = *)$$
