report1/alex.tex

   1 \section{Coordinate based approach}
   2 Let $T = \{\_,@,.,\#,\$,*,+\}$. We model a sokoban field as a set $F = \{x_{i,j} | x_{i,j} \in T, \forall i,j \ni x_{i,j} \neq \perp \}$.\\
   3 We introduce a variable $m \in \{\text{up}, \text{down}, \text{left}, \text{right}\}$ which is picked up non-deterministically for each next step. The value of $m$ denotes the intended direction of movement of the actor. The values $x_{i,j} \in F$ are updated each step according the values of $m$ and the rules described in the subsection.
   4 \subsection{Changing the state}
   5 Let\\
   6 $\delta_{x}(x,m) =
   7   \begin{cases}
   8     (x+1) & \quad \text{if } m = left\\
   9     (x-1) & \quad \text{if } m = right\\
  10     x & \quad \text{otherwise}
  11   \end{cases}$\quad
  12 $\delta'_{x}(x,m) =
  13   \begin{cases}
  14     (x-1) & \quad \text{if } m = left\\
  15     (x+1) & \quad \text{if } m = right\\
  16     x & \quad \text{otherwise}
  17   \end{cases}$\\
  18 $\delta_{y}(y,m) =
  19   \begin{cases}
  20     (y+1) & \quad \text{if } m = up\\
  21     (y-1) & \quad \text{if } m = down\\
  22     y & \quad \text{otherwise}
  23   \end{cases}$\quad
  24 $\delta'_{y}(y,m) =
  25   \begin{cases}
  26     (y-1) & \quad \text{if } m = up\\
  27     (y+1) & \quad \text{if } m = down\\
  28     y & \quad \text{otherwise}
  29   \end{cases}$\\
  30   $\gamma_{x}(x,m) =
  31     \begin{cases}
  32       (x+2) & \quad \text{if } m = left\\
  33       (x-2) & \quad \text{if } m = right\\
  34       x & \quad \text{otherwise}
  35     \end{cases}$\quad
  36   $\gamma_{y}(y,m) =
  37     \begin{cases}
  38       (y+2) & \quad \text{if } m = up\\
  39       (y-2) & \quad \text{if } m = down\\
  40       y & \quad \text{otherwise}
  41     \end{cases}$
  42
  43 %    "    x" <+ x <+ "_" <+ y <+ " = BoxOnTarget & (x" <+ (checkX p x) <+ "_" <+ (checkY p x  (y+1)) <+ " = Agent | x"
  44 %                            <+ (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;",
  45 %                    "    x" <+ x <+ "_" <+ y <+ " = BoxOnTarget & (x" <+ (checkX p (x+1)) <+ "_" <+ (checkY p (x+1) y) <+ " = Agent | x"
  46 %                            <+ (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)) <+ "_"
  47 %                            <+ (checkY p (x-1) y) <+ " = Target) & move = Up: AgentOnTarget;",
  48 %                    "    x" <+ x <+ "_" <+ y <+ " = BoxOnTarget & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = Agent | x"
  49 %                            <+ (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;",
  50 %                    "    x" <+ x <+ "_" <+ y <+ " = BoxOnTarget & (x" <+ (checkX p (x-1)) <+ "_" <+ (checkY p (x-1) y) <+ " = Agent | x"
  51 %                            <+ (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)) <+ "_"
  52 %                            <+ (checkY p (x+1) y) <+ " = Target) & move = Down : AgentOnTarget;",
  53
  54
  55
  56 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\\
  57 $
  58 next(x_{i,j}) =
  59   \begin{cases}
  60     \# & \quad \text{if } x_{i,j} = \#\\
  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)} = +) \wedge x_{\delta_{x}(i,m),\delta_{y}(j,m)} \neq \perp\\
  62     @ & \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)} = +)\\
  63     & \quad \wedge (x_{\delta'_{x}(i,m),\delta'_{y}(j,m)} = \_ \vee x_{\delta'_{x}(i,m),\delta'_{y}(j,m)} = .)\\
  64     & \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\\
  65     \$ & \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\\
  66     \_ & \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)} = .)\\
  67     & \quad \vee ((x_{\delta_{x}(i,m),\delta_{y}(j,m)} = \$ \vee x_{\delta_{x}(i,m),\delta_{y}(j,m)} = *) \wedge \\
  68     & \quad (x_{\gamma_{x}(i,m),\gamma_{y}(j,m)} = \_ \vee x_{\gamma_{x}(i,m),\gamma_{y}(j,m)} = .)) \\
  69     & \quad x_{\delta_{x}(i,m),\delta_{y}(j,m)} \neq \perp \wedge x_{\gamma_{x}(i,m),\gamma_{y}(j,m)} \neq \perp\\
  70     + & \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\\
  71     + & \quad x_{i,j} = * \wedge (x_{\delta_{x}(i,m),\delta_{y}(j,m)} = @ \vee x_{\delta_{x}(i,m),\delta_{y}(j,m)} = +)\\
  72     & \quad \wedge (x_{\delta'_{x}(i,m),\delta'_{y}(j,m)} = \_ \vee x_{\delta'_{x}(i,m),\delta'_{y}(j,m)} = .)\\
  73     & \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\\
  74     * & \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)} = *)\\
  75     & \quad \wedge (x_{\gamma_{x}(i,m),\gamma_{y}(j,m)} = @ \vee x_{\gamma_{x}(i,m),\gamma_{y}(j,m)} = +)\\
  76     & \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\\
  77     . & \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\\
  78     x_{i,j} & \quad \text{otherwise}\\
  79   \end{cases}
  80 $
  81 \subsection{Goal}
  82 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$.
  83 In order to check a sokoban field for a possible solution, we introduce the following invariant:\\
  84 $$\neg \bigwedge_{x \in G} (x = *)$$