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
}
8 (x+
1) &
\quad \text{if
} m = left\\
9 (x-
1) &
\quad \text{if
} m = right\\
10 x &
\quad \text{otherwise
}
14 (x-
1) &
\quad \text{if
} m = left\\
15 (x+
1) &
\quad \text{if
} m = right\\
16 x &
\quad \text{otherwise
}
20 (y+
1) &
\quad \text{if
} m = up\\
21 (y-
1) &
\quad \text{if
} m = down\\
22 y &
\quad \text{otherwise
}
26 (y-
1) &
\quad \text{if
} m = up\\
27 (y+
1) &
\quad \text{if
} m = down\\
28 y &
\quad \text{otherwise
}
32 (x+
2) &
\quad \text{if
} m = left\\
33 (x-
2) &
\quad \text{if
} m = right\\
34 x &
\quad \text{otherwise
}
38 (y+
2) &
\quad \text{if
} m = up\\
39 (y-
2) &
\quad \text{if
} m = down\\
40 y &
\quad \text{otherwise
}
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;",
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\\
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
}\\
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 = *)$$