report2/implementation.tex

   1 \section{Implementation}
   2 \subsection{Screen encoding}
   3 When parsed the sokoban screen is stripped of all walls and unreachable empty
   4 spaces are removed.
   5
   6 Let $T=\{free,box,target,agent,targetagent,targetbox\}$ be the set of possible
   7 states of a tile. Tiles are numbered and thus a sokoban screen is the set $F$
   8 containing a $x_i\in T$ for every tile. We introduce a function $ord(x, y)$
   9 that returns the tile number for a given $x$ and $y$ coordinate. To encode the
  10 state we introduce an encoding function that encodes a state in three boolean
  11 variables:
  12 $$encode(t)=\begin{cases}
  13         000 & \text{if }t=wall\\
  14         001 & \text{if }t=free\\
  15         010 & \text{if }t=box\\
  16         011 & \text{if }t=target\\
  17         100 & \text{if }t=targetbox\\
  18         101 & \text{if }t=agent\\
  19         110 & \text{if }t=agentbox
  20 \end{cases}$$
  21
  22 This means that the encoding of a screen takes $3*|F|$ variables.
  23
  24 \subsection{Transition encoding}
  25 We introduce a variable denoting the intended direction of movement $m \in
  26 \{\text{up}, \text{down}, \text{left}, \text{right}\}$. Per move we define a
  27 $\delta$ and $\gamma$ variable which represent the change in coordinate value
  28 respectively for the next position and the position next to the next postition.
  29 \\
  30 $\delta_{(x,y)}(m)=\begin{cases}
  31         (x-1, y) & \text{if } m = left\\
  32         (x+1, y) & \text{if } m = right\\
  33         (x, y+1) & \text{if } m = down\\
  34         (x, y-1) & \text{if } m = up\\
  35 \end{cases}\quad
  36 \gamma{(x,y)}(m)=\begin{cases}
  37         (x-2, y) & \text{if } m = left\\
  38         (x+2, y) & \text{if } m = right\\
  39         (x, y+2) & \text{if } m = down\\
  40         (x, y-2) & \text{if } m = up\\
  41 \end{cases} $
  42
  43 %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\\
  44 %$
  45 %next(x_{i,j}) =
  46 %  \begin{cases}
  47 %    \# & \quad \text{if } x_{i,j} = \#\\
  48 %    @ & \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\\
  49 %    @ & \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)} = +)\\
  50 %    & \quad \wedge (x_{\delta'_{x}(i,m),\delta'_{y}(j,m)} = \_ \vee x_{\delta'_{x}(i,m),\delta'_{y}(j,m)} = .)\\
  51 %    & \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\\
  52 %    \$ & \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\\
  53 %    \_ & \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)} = .)\\
  54 %    & \quad \vee ((x_{\delta_{x}(i,m),\delta_{y}(j,m)} = \$ \vee x_{\delta_{x}(i,m),\delta_{y}(j,m)} = *) \wedge \\
  55 %    & \quad (x_{\gamma_{x}(i,m),\gamma_{y}(j,m)} = \_ \vee x_{\gamma_{x}(i,m),\gamma_{y}(j,m)} = .)) \\
  56 %    & \quad x_{\delta_{x}(i,m),\delta_{y}(j,m)} \neq \perp \wedge x_{\gamma_{x}(i,m),\gamma_{y}(j,m)} \neq \perp\\
  57 %    + & \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\\
  58 %    + & \quad x_{i,j} = * \wedge (x_{\delta_{x}(i,m),\delta_{y}(j,m)} = @ \vee x_{\delta_{x}(i,m),\delta_{y}(j,m)} = +)\\
  59 %    & \quad \wedge (x_{\delta'_{x}(i,m),\delta'_{y}(j,m)} = \_ \vee x_{\delta'_{x}(i,m),\delta'_{y}(j,m)} = .)\\
  60 %    & \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\\
  61 %    * & \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)} = *)\\
  62 %    & \quad \wedge (x_{\gamma_{x}(i,m),\gamma_{y}(j,m)} = @ \vee x_{\gamma_{x}(i,m),\gamma_{y}(j,m)} = +)\\
  63 %    & \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\\
  64 %    . & \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\\
  65 %    x_{i,j} & \quad \text{otherwise}\\
  66 %  \end{cases}
  67 %$
  68 %\subsection{Goal}
  69 %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$.
  70 %In order to check a sokoban field for a possible solution, we introduce the following invariant:\\
  71 %$$\neg \bigwedge_{x \in G} (x = *)$$