states of a tile. Tiles are numbered and thus a sokoban screen is the set $F$
containing a $x_i\in T$ for every tile. We introduce a function $ord(x, y)$
that returns the tile number for a given $x$ and $y$ coordinate and a function
-$iord(i)$ that does the reverse. To encode the
-state we introduce an encoding function that encodes a state in three boolean
-variables:
+$iord(i)$ that does the reverse. To encode the state we introduce an encoding function that encodes each screen tile as a unique combination of boolean variables:
+
$$encode(t)=\begin{cases}
001 & \text{if }t=free\\
010 & \text{if }t=box\\
This means that the encoding of a screen takes $3*|F|$ variables.
-Regarding the BDD representation, we use sylvan cubes. For state state variables we use odd variables in sylvan cubes.
-
-
\subsection{Transition encoding}
-We introduce a variable denoting the intended direction of movement $m \in
-\{\text{up}, \text{down}, \text{left}, \text{right}\}$. Per move we define a $\delta$ and $\gamma$ variables which represent the change in coordinate values respectively for the next position and the position next to the next postition.
+We generate transition relations for four possible move directions of an agent, for all screen tiles. There are three type of transition relations, namely: a one-tile relation (changes only one tile), a two-tile relation (changes only two tiles) and a three-tile relation (transforms three tiles per transition simultaneously). In order to generate transition relations, we iterate through a screen and for each tile we check neighbouring space with the purpose of generating only the relevant relations. For example, if we concider a tile in the top-left corner, there is no need to generate one or two-tiled transition relations which can transform tiles to the left or to the right of that given tile. For each possible direction of agent movement, we define a $\delta$ and a $\gamma$ variables which represent the change in coordinate values respectively for the next position and the position next to the next postition.
$$\delta_{(x,y)}(m)=\begin{cases}
(x-1, y) & \text{if } m = left\\
(x+1, y) & \text{if } m = right\\
(x, y-2) & \text{if } m = up\\
\end{cases}$$
-We define the tile update function $next(i_1, i_2, i_3)$ where $i_1$ contains
+We define the following tile update functions: $next(i_1)$, $next'(i_1,i_2)$ $next''(i_1, i_2, i_3)$ where $i_1$ contains
the agent and $i_2$ and $i_3$ are adjacent to it in some direction.
-$$next(i_1, i_2, i_3)=\left\{\begin{array}{lp{2pt}l}
-% Three state transitions
- (free, agent, box) & \text{if } &
- i_1=agent \wedge i_2=box \wedge i_3=free\\
- (target, agent, box) & \text{if } &
- i_1=targetagent \wedge i_2=box \wedge i_3=free\\
- (free, targetagent, box) & \text{if } &
- i_1=agent \wedge i_2=targetbox \wedge i_3=free\\
- (free, agent, targetbox) & \text{if } &
- i_1=agent \wedge i_2=box \wedge i_3=targetbox\\
- (target, targetagent, box) & \text{if } &
- i_1=targetagent \wedge i_2=targetbox \wedge i_3=free\\
- (target, agent, targetbox) & \text{if } &
- i_1=targetagent \wedge i_2=box \wedge i_3=target\\
- (free, targetagent, targetbox) & \text{if } &
- i_1=agent \wedge i_2=targetbox \wedge i_3=target\\
- (target, targetagent, targetbox) & \text{if } &
+
+$$next'(i_1, i_2)=\left\{\begin{array}{lp{2pt}l}
+ (agent) & \text{if } & i_1=agent\\
+ (targetagent) & \text{if } & i_1=targetagent\\
+\end{array}\right.$$
+
+$$next'(i_1, i_2)=\left\{\begin{array}{lp{2pt}l}
+ (agent, free) & \text{if } & i_1=free \wedge i_2=agent\\
+ (agent, target) & \text{if } & i_1=free \wedge i_2=targagent\\
+ (targagent, free) & \text{if } & i_1=target \wedge i_2=agent\\
+ (targagent, target) & \text{if } & i_1=target \wedge i_2=targagent\\
+ (agent, box) & \text{if } & i_1=agent \wedge i_2=box\\
+ (agent, targbox) & \text{if } & i_1=agent \wedge i_2=targbox\\
+ (targagent, box) & \text{if } & i_1=targagent \wedge i_2=box\\
+ (targagent, targbox) & \text{if } & i_1=targagent \wedge i_2=targbox\\
+\end{array}\right.$$
+
+$$next''(i_1, i_2, i_3)=\left\{\begin{array}{lp{2pt}l}
+ (agent, box, box) & \text{if } &
+ i_1=agent \wedge i_2=box \wedge i_3=box\\
+ (agent, box, targbox) & \text{if } &
+ i_1=agent \wedge i_2=box \wedge i_3=targbox\\
+ (targagent, box, box) & \text{if } &
+ i_1=targetagent \wedge i_2=box \wedge i_3=box\\
+ (targagent, box, targbox) & \text{if } &
+ i_1=targagent \wedge i_2=box \wedge i_3=targbox\\
+ (agent, box, free) & \text{if } &
+ i_1=free \wedge i_2=agent \wedge i_3=box\\
+ (agent, targbox, free) & \text{if } &
+ i_1=free \wedge i_2=targagent \wedge i_3=box\\
+ (agent, box, target) & \text{if } &
+ i_1=free \wedge i_2=agent \wedge i_3=targbox\\
+ (agent, targbox, target) & \text{if } &
+ i_1=free \wedge i_2=targagent \wedge i_3=targbox\\
+ (targagent, box, free) & \text{if } &
i_1=targetagent \wedge i_2=targetbox \wedge i_3=target\\
-% Two state transitions
- (free, agent, i_3) & \text{if } & i_1=agent \wedge i_2=free\\
- (free, targetagent, i_3) & \text{if } & i_1=agent \wedge i_2=target\\
- (target, agent, i_3) & \text{if } & i_1=targetagent \wedge i_2=free\\
- (target, targetagent, i_3) & \text{if } & i_1=targetagent \wedge i_2=target\\
-% One state transitions
- (agent, i_2, i_3) & \text{if } & i_1=agent\\
- (targetagent, i_2, i_3) & \text{if } & i_1=targetagent\\
+ (targagent, targbox, free) & \text{if } &
+ i_1=target \wedge i_2=targagent \wedge i_3=box\\
+ (targagent, box, target) & \text{if } &
+ i_1=target \wedge i_2=agent \wedge i_3=targbox\\
+ (targagent, targbox, target) & \text{if } &
+ i_1=target \wedge i_2=targagent \wedge i_3=targbox\\
\end{array}\right.$$
\subsection{Goal encoding}
We use the standard optimized reachability algorithm to solve a screen but
added a goal condition that breaks the loop. When the loop breaks prematurely
it means a solution is found. If the full loop continues until the entire state
-space is search and the break condition is not met it means there is no
+space is searched and the break condition is not met it means there is no
solution.
\begin{algorithm}[H]
\subsubsection{Encoding}
To encode the screen the tiles are numbered from left to right from top to
-bottom. Thus resulting in $i_1=agent, i_2=box, i_3=target$. When we translate
-these numbers to sylvan-sane variables we get the following bdd shown in
+bottom (in a convenient coordinate-like manner). In order to translate the initial screen into BDD representation, we iterate through a screen's tiles. We use even BDD variable identifiers to represent states (screens). For convenient BDD creation, we use sylvan cubes.As an example we can consider the following bdd shown in
Figure~\ref{fig:toy}. Variables $0, 2, 4$ represent $i_1$, $6, 8, 10$ represent
$i_2$ and lastly $12, 14, 16$ represents $i_3$.
\begin{figure}[p]
\end{figure}
Finally encoding the transitions already results in a long list of complicated
-BDDs that each encode a possible move in all possible directions. In this
+BDDs that each encode a possible move in all possible directions. In transition relations, even BDD variable identifiers act as state filters, whereas even variable identifiers act as new values. Each transition changes only a limited subset of the screen variables. In this
example there is only one move possible in the first state, thus all moves
except for the one move result in a relative product that is empty. For example
the sub-BDD that encodes the first position only looks is visualized in