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 each screen tile as a unique combination of 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.
\subsection{Transition encoding}
-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.
+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 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.
+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)=\left\{\begin{array}{lp{2pt}l}
+$$next(i_1)=\left\{\begin{array}{lp{2pt}l}
(agent) & \text{if } & i_1=agent\\
(targetagent) & \text{if } & i_1=targetagent\\
\end{array}\right.$$
\lstinputlisting[label={lst:toy},caption={Example screen}]{toy.screen}
-\subsubsection{Encoding}
To encode the screen the tiles are numbered from left to right from top to
-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
+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 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
-Figure~\ref{fig:toy3}. The only satisfying assignment is that $0, 2, 4$ hold
-the values $1, 0, 1$ thus encoding man and the variables $1, 3, 5$ holding the
-values $0, 0, 1$ thus encoding free.
+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 Figure~\ref{fig:toy3}. The only satisfying
+assignment is that $0, 2, 4$ hold the values $1, 0, 1$ thus encoding man and
+the variables $1, 3, 5$ holding the values $0, 0, 1$ thus encoding free.
\begin{figure}[p]
\centering
\includegraphics[width=.8\textwidth]{toy3.png}
\caption{Sub-BDD of a move~\label{fig:toy3}}
\end{figure}
-
-\subsubsection{Results}
repositories / mc1516pa.git / commitdiff