1 \section{Implementation
}
2 \subsection{Screen encoding
}
3 When parsed the sokoban screen is stripped of all walls and unreachable empty
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
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
22 This means that the encoding of a screen takes $
3*|F|$ variables.
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.
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\\
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\\
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\\
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}\\
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 = *)$$