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}\}$. Tiles
  27 %
  28 %Let\\
  29 %$\delta_{x}(x,m) =
  30 %  \begin{cases}
  31 %    (x+1) & \quad \text{if } m = left\\
  32 %    (x-1) & \quad \text{if } m = right\\
  33 %    x & \quad \text{otherwise}
  34 %  \end{cases}$\quad
  35 %$\delta'_{x}(x,m) =
  36 %  \begin{cases}
  37 %    (x-1) & \quad \text{if } m = left\\
  38 %    (x+1) & \quad \text{if } m = right\\
  39 %    x & \quad \text{otherwise}
  40 %  \end{cases}$\\
  41 %$\delta_{y}(y,m) =
  42 %  \begin{cases}
  43 %    (y+1) & \quad \text{if } m = up\\
  44 %    (y-1) & \quad \text{if } m = down\\
  45 %    y & \quad \text{otherwise}
  46 %  \end{cases}$\quad
  47 %$\delta'_{y}(y,m) =
  48 %  \begin{cases}
  49 %    (y-1) & \quad \text{if } m = up\\
  50 %    (y+1) & \quad \text{if } m = down\\
  51 %    y & \quad \text{otherwise}
  52 %  \end{cases}$\\
  53 %  $\gamma_{x}(x,m) =
  54 %    \begin{cases}
  55 %      (x+2) & \quad \text{if } m = left\\
  56 %      (x-2) & \quad \text{if } m = right\\
  57 %      x & \quad \text{otherwise}
  58 %    \end{cases}$\quad
  59 %  $\gamma_{y}(y,m) =
  60 %    \begin{cases}
  61 %      (y+2) & \quad \text{if } m = up\\
  62 %      (y-2) & \quad \text{if } m = down\\
  63 %      y & \quad \text{otherwise}
  64 %    \end{cases}$
  65 %
  66 %%    "    x" <+ x <+ "_" <+ y <+ " = BoxOnTarget & (x" <+ (checkX p x) <+ "_" <+ (checkY p x  (y+1)) <+ " = Agent | x"
  67 %%                            <+ (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;",
  68 %%                    "    x" <+ x <+ "_" <+ y <+ " = BoxOnTarget & (x" <+ (checkX p (x+1)) <+ "_" <+ (checkY p (x+1) y) <+ " = Agent | x"
  69 %%                            <+ (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)) <+ "_"
  70 %%                            <+ (checkY p (x-1) y) <+ " = Target) & move = Up: AgentOnTarget;",
  71 %%                    "    x" <+ x <+ "_" <+ y <+ " = BoxOnTarget & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = Agent | x"
  72 %%                            <+ (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;",
  73 %%                    "    x" <+ x <+ "_" <+ y <+ " = BoxOnTarget & (x" <+ (checkX p (x-1)) <+ "_" <+ (checkY p (x-1) y) <+ " = Agent | x"
  74 %%                            <+ (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)) <+ "_"
  75 %%                            <+ (checkY p (x+1) y) <+ " = Target) & move = Down : AgentOnTarget;",
  76 %
  77 %
  78 %
  79 %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\\
  80 %$
  81 %next(x_{i,j}) =
  82 %  \begin{cases}
  83 %    \# & \quad \text{if } x_{i,j} = \#\\
  84 %    @ & \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\\
  85 %    @ & \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)} = +)\\
  86 %    & \quad \wedge (x_{\delta'_{x}(i,m),\delta'_{y}(j,m)} = \_ \vee x_{\delta'_{x}(i,m),\delta'_{y}(j,m)} = .)\\
  87 %    & \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\\
  88 %    \$ & \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\\
  89 %    \_ & \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)} = .)\\
  90 %    & \quad \vee ((x_{\delta_{x}(i,m),\delta_{y}(j,m)} = \$ \vee x_{\delta_{x}(i,m),\delta_{y}(j,m)} = *) \wedge \\
  91 %    & \quad (x_{\gamma_{x}(i,m),\gamma_{y}(j,m)} = \_ \vee x_{\gamma_{x}(i,m),\gamma_{y}(j,m)} = .)) \\
  92 %    & \quad x_{\delta_{x}(i,m),\delta_{y}(j,m)} \neq \perp \wedge x_{\gamma_{x}(i,m),\gamma_{y}(j,m)} \neq \perp\\
  93 %    + & \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\\
  94 %    + & \quad x_{i,j} = * \wedge (x_{\delta_{x}(i,m),\delta_{y}(j,m)} = @ \vee x_{\delta_{x}(i,m),\delta_{y}(j,m)} = +)\\
  95 %    & \quad \wedge (x_{\delta'_{x}(i,m),\delta'_{y}(j,m)} = \_ \vee x_{\delta'_{x}(i,m),\delta'_{y}(j,m)} = .)\\
  96 %    & \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\\
  97 %    * & \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)} = *)\\
  98 %    & \quad \wedge (x_{\gamma_{x}(i,m),\gamma_{y}(j,m)} = @ \vee x_{\gamma_{x}(i,m),\gamma_{y}(j,m)} = +)\\
  99 %    & \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\\
 100 %    . & \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\\
 101 %    x_{i,j} & \quad \text{otherwise}\\
 102 %  \end{cases}
 103 %$
 104 %\subsection{Goal}
 105 %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$.
 106 %In order to check a sokoban field for a possible solution, we introduce the following invariant:\\
 107 %$$\neg \bigwedge_{x \in G} (x = *)$$