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
   7 possible states of a tile. Tiles are numbered and thus a sokoban screen is the
   8 set $F$ containing a $x_i\in T$ for every tile. To encode the state we
   9 introduce an encoding function that encodes a state in three boolean variables:
  10 $$encode(t)=\begin{cases}
  11         000 & \text{if }t=wall\\
  12         001 & \text{if }t=free\\
  13         010 & \text{if }t=box\\
  14         011 & \text{if }t=target\\
  15         100 & \text{if }t=targetbox\\
  16         101 & \text{if }t=agent\\
  17         110 & \text{if }t=agentbox
  18 \end{cases}$$
  19
  20 This means that the encoding of a screen takes $3*|F|$ variables.
  21
  22 \subsection{Transition encoding}
  23 We introduce a variable denoting the intended direction of movement $m \in
  24 \{\text{up}, \text{down}, \text{left}, \text{right}\}$.
  25 %
  26 %Let\\
  27 %$\delta_{x}(x,m) =
  28 %  \begin{cases}
  29 %    (x+1) & \quad \text{if } m = left\\
  30 %    (x-1) & \quad \text{if } m = right\\
  31 %    x & \quad \text{otherwise}
  32 %  \end{cases}$\quad
  33 %$\delta'_{x}(x,m) =
  34 %  \begin{cases}
  35 %    (x-1) & \quad \text{if } m = left\\
  36 %    (x+1) & \quad \text{if } m = right\\
  37 %    x & \quad \text{otherwise}
  38 %  \end{cases}$\\
  39 %$\delta_{y}(y,m) =
  40 %  \begin{cases}
  41 %    (y+1) & \quad \text{if } m = up\\
  42 %    (y-1) & \quad \text{if } m = down\\
  43 %    y & \quad \text{otherwise}
  44 %  \end{cases}$\quad
  45 %$\delta'_{y}(y,m) =
  46 %  \begin{cases}
  47 %    (y-1) & \quad \text{if } m = up\\
  48 %    (y+1) & \quad \text{if } m = down\\
  49 %    y & \quad \text{otherwise}
  50 %  \end{cases}$\\
  51 %  $\gamma_{x}(x,m) =
  52 %    \begin{cases}
  53 %      (x+2) & \quad \text{if } m = left\\
  54 %      (x-2) & \quad \text{if } m = right\\
  55 %      x & \quad \text{otherwise}
  56 %    \end{cases}$\quad
  57 %  $\gamma_{y}(y,m) =
  58 %    \begin{cases}
  59 %      (y+2) & \quad \text{if } m = up\\
  60 %      (y-2) & \quad \text{if } m = down\\
  61 %      y & \quad \text{otherwise}
  62 %    \end{cases}$
  63 %
  64 %%    "    x" <+ x <+ "_" <+ y <+ " = BoxOnTarget & (x" <+ (checkX p x) <+ "_" <+ (checkY p x  (y+1)) <+ " = Agent | x"
  65 %%                            <+ (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;",
  66 %%                    "    x" <+ x <+ "_" <+ y <+ " = BoxOnTarget & (x" <+ (checkX p (x+1)) <+ "_" <+ (checkY p (x+1) y) <+ " = Agent | x"
  67 %%                            <+ (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)) <+ "_"
  68 %%                            <+ (checkY p (x-1) y) <+ " = Target) & move = Up: AgentOnTarget;",
  69 %%                    "    x" <+ x <+ "_" <+ y <+ " = BoxOnTarget & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = Agent | x"
  70 %%                            <+ (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;",
  71 %%                    "    x" <+ x <+ "_" <+ y <+ " = BoxOnTarget & (x" <+ (checkX p (x-1)) <+ "_" <+ (checkY p (x-1) y) <+ " = Agent | x"
  72 %%                            <+ (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)) <+ "_"
  73 %%                            <+ (checkY p (x+1) y) <+ " = Target) & move = Down : AgentOnTarget;",
  74 %
  75 %
  76 %
  77 %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\\
  78 %$
  79 %next(x_{i,j}) =
  80 %  \begin{cases}
  81 %    \# & \quad \text{if } x_{i,j} = \#\\
  82 %    @ & \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\\
  83 %    @ & \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)} = +)\\
  84 %    & \quad \wedge (x_{\delta'_{x}(i,m),\delta'_{y}(j,m)} = \_ \vee x_{\delta'_{x}(i,m),\delta'_{y}(j,m)} = .)\\
  85 %    & \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\\
  86 %    \$ & \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\\
  87 %    \_ & \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)} = .)\\
  88 %    & \quad \vee ((x_{\delta_{x}(i,m),\delta_{y}(j,m)} = \$ \vee x_{\delta_{x}(i,m),\delta_{y}(j,m)} = *) \wedge \\
  89 %    & \quad (x_{\gamma_{x}(i,m),\gamma_{y}(j,m)} = \_ \vee x_{\gamma_{x}(i,m),\gamma_{y}(j,m)} = .)) \\
  90 %    & \quad x_{\delta_{x}(i,m),\delta_{y}(j,m)} \neq \perp \wedge x_{\gamma_{x}(i,m),\gamma_{y}(j,m)} \neq \perp\\
  91 %    + & \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\\
  92 %    + & \quad x_{i,j} = * \wedge (x_{\delta_{x}(i,m),\delta_{y}(j,m)} = @ \vee x_{\delta_{x}(i,m),\delta_{y}(j,m)} = +)\\
  93 %    & \quad \wedge (x_{\delta'_{x}(i,m),\delta'_{y}(j,m)} = \_ \vee x_{\delta'_{x}(i,m),\delta'_{y}(j,m)} = .)\\
  94 %    & \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\\
  95 %    * & \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)} = *)\\
  96 %    & \quad \wedge (x_{\gamma_{x}(i,m),\gamma_{y}(j,m)} = @ \vee x_{\gamma_{x}(i,m),\gamma_{y}(j,m)} = +)\\
  97 %    & \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\\
  98 %    . & \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\\
  99 %    x_{i,j} & \quad \text{otherwise}\\
 100 %  \end{cases}
 101 %$
 102 %\subsection{Goal}
 103 %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$.
 104 %In order to check a sokoban field for a possible solution, we introduce the following invariant:\\
 105 %$$\neg \bigwedge_{x \in G} (x = *)$$