report2/implementation.tex

   1 \section{Implementation}
   2 \subsection{Screen encoding}
   3 When parsed the sokoban screen is stripped of all walls and unreachable empty
   4 spaces are removed. Moreover, a screen is rejected if either there are no
   5 boxes, there is no agent or the number of boxes is not equal to the number of
   6 targets.
   7
   8 Let $T=\{free,box,target,agent,targetagent,targetbox\}$ be the set of possible
   9 states of a tile. Tiles are numbered and thus a sokoban screen is the set $F$
  10 containing a $x_i\in T$ for every tile. We introduce a function $ord(x, y)$
  11 that returns the tile number for a given $x$ and $y$ coordinate and a function
  12 $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:
  13
  14 $$encode(t)=\begin{cases}
  15         001 & \text{if }t=free\\
  16         010 & \text{if }t=box\\
  17         011 & \text{if }t=target\\
  18         100 & \text{if }t=targetbox\\
  19         101 & \text{if }t=agent\\
  20         110 & \text{if }t=agentbox
  21 \end{cases}$$
  22
  23 This means that the encoding of a screen takes $3*|F|$ variables.
  24
  25 \subsection{Transition encoding}
  26 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.
  27 $$\delta_{(x,y)}(m)=\begin{cases}
  28         (x-1, y) & \text{if } m = left\\
  29         (x+1, y) & \text{if } m = right\\
  30         (x, y+1) & \text{if } m = down\\
  31         (x, y-1) & \text{if } m = up\\
  32 \end{cases}\quad
  33 \gamma{(x,y)}(m)=\begin{cases}
  34         (x-2, y) & \text{if } m = left\\
  35         (x+2, y) & \text{if } m = right\\
  36         (x, y+2) & \text{if } m = down\\
  37         (x, y-2) & \text{if } m = up\\
  38 \end{cases}$$
  39
  40 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
  41 the agent and $i_2$ and $i_3$ are adjacent to it in some direction.
  42
  43 $$next'(i_1, i_2)=\left\{\begin{array}{lp{2pt}l}
  44         (agent) & \text{if } & i_1=agent\\
  45         (targetagent) & \text{if } & i_1=targetagent\\
  46 \end{array}\right.$$
  47
  48 $$next'(i_1, i_2)=\left\{\begin{array}{lp{2pt}l}
  49         (agent, free) & \text{if } & i_1=free \wedge i_2=agent\\
  50         (agent, target) & \text{if } & i_1=free \wedge i_2=targagent\\
  51         (targagent, free) & \text{if } & i_1=target \wedge i_2=agent\\
  52     (targagent, target) & \text{if } & i_1=target \wedge i_2=targagent\\
  53         (agent, box) & \text{if } & i_1=agent \wedge i_2=box\\
  54         (agent, targbox) & \text{if } & i_1=agent \wedge i_2=targbox\\
  55         (targagent, box) & \text{if } & i_1=targagent \wedge i_2=box\\
  56         (targagent, targbox) & \text{if } & i_1=targagent \wedge i_2=targbox\\
  57 \end{array}\right.$$
  58
  59 $$next''(i_1, i_2, i_3)=\left\{\begin{array}{lp{2pt}l}
  60         (agent, box, box) & \text{if } &
  61                 i_1=agent \wedge i_2=box \wedge i_3=box\\
  62         (agent, box, targbox) & \text{if } &
  63                 i_1=agent \wedge i_2=box \wedge i_3=targbox\\
  64         (targagent, box, box) & \text{if } &
  65                 i_1=targetagent \wedge i_2=box \wedge i_3=box\\
  66         (targagent, box, targbox) & \text{if } &
  67                 i_1=targagent \wedge i_2=box \wedge i_3=targbox\\
  68         (agent, box, free) & \text{if } &
  69                 i_1=free \wedge i_2=agent \wedge i_3=box\\
  70         (agent, targbox, free) & \text{if } &
  71                 i_1=free \wedge i_2=targagent \wedge i_3=box\\
  72         (agent, box, target) & \text{if } &
  73                 i_1=free \wedge i_2=agent \wedge i_3=targbox\\
  74         (agent, targbox, target) & \text{if } &
  75                 i_1=free \wedge i_2=targagent \wedge i_3=targbox\\
  76         (targagent, box, free) & \text{if } &
  77                 i_1=targetagent \wedge i_2=targetbox \wedge i_3=target\\
  78         (targagent, targbox, free) & \text{if } &
  79                 i_1=target \wedge i_2=targagent \wedge i_3=box\\
  80         (targagent, box, target) & \text{if } &
  81                 i_1=target \wedge i_2=agent \wedge i_3=targbox\\
  82         (targagent, targbox, target) & \text{if } &
  83                 i_1=target \wedge i_2=targagent \wedge i_3=targbox\\
  84 \end{array}\right.$$
  85
  86 \subsection{Goal encoding}
  87 Encoding the goal state is very trivial. Just make sure all $target$ tiles are
  88 $targetbox$ tiles.
  89
  90 \subsection{Algorithm}
  91 We use the standard optimized reachability algorithm to solve a screen but
  92 added a goal condition that breaks the loop. When the loop breaks prematurely
  93 it means a solution is found. If the full loop continues until the entire state
  94 space is searched and the break condition is not met it means there is no
  95 solution.
  96
  97 \begin{algorithm}[H]
  98         \KwIn{I, Initial state BDD}
  99         \KwIn{$R_i$, List of transition BDDs}
 100         \KwIn{G, Goal BDD}
 101         $V_{old}\leftarrow BDDempty$\;
 102         $V_{new}\leftarrow I$\;
 103         \While{$V_{new}\neq V_{old}$}{
 104                 $V_{old}\leftarrow V_{new}$\;
 105                 \ForEach{$R_i$}{
 106                         $V_{new}\leftarrow BDDapply(\vee, V_{new}, BDDrelprod(V_{new}, R_i)$\;
 107                 }
 108                 \lIf{$BDDsatcount(BDDand(G, V_{new}))>0$}{$break$}
 109         }
 110 \end{algorithm}
 111
 112 \subsection{Example}
 113 For example, take the toy screen shown as the first representation in
 114 Listing~\ref{lst:toy}. When the screen is parsed the unreachable space is first
 115 removed by detecting reachable space with the flood fill algorithm. This
 116 results in the second representation in Listing~\ref{lst:toy}.
 117
 118 \lstinputlisting[label={lst:toy},caption={Example screen}]{toy.screen}
 119
 120 \subsubsection{Encoding}
 121 To encode the screen the tiles are numbered from left to right from top to
 122 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
 123 Figure~\ref{fig:toy}. Variables $0, 2, 4$ represent $i_1$, $6, 8, 10$ represent
 124 $i_2$ and lastly $12, 14, 16$ represents $i_3$.
 125 \begin{figure}[p]
 126         \centering
 127         \includegraphics[width=\textwidth]{toy.png}
 128         \caption{Initial state encoding of the example~\label{fig:toy}}
 129 \end{figure}
 130
 131 Encoding the goal state happens in a similar way. The algorithm basically
 132 states that all $target$ positions should be $boxtarget$. This is results in
 133 the BDD shown in Figure~\ref{fig:toy2}.
 134
 135 \begin{figure}[p]
 136         \centering
 137         \includegraphics[width=.5\textwidth]{toy2.png}
 138         \caption{Goal state encoding of the example~\label{fig:toy2}}
 139 \end{figure}
 140
 141 Finally encoding the transitions already results in a long list of complicated
 142 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
 143 example there is only one move possible in the first state, thus all moves
 144 except for the one move result in a relative product that is empty. For example
 145 the sub-BDD that encodes the first position only looks is visualized in
 146 Figure~\ref{fig:toy3}. The only satisfying assignment is that $0, 2, 4$ hold
 147 the values $1, 0, 1$ thus encoding man and the variables $1, 3, 5$ holding the
 148 values $0, 0, 1$ thus encoding free.
 149
 150 \begin{figure}[p]
 151         \centering
 152         \includegraphics[width=.8\textwidth]{toy3.png}
 153         \caption{Sub-BDD of a move~\label{fig:toy3}}
 154 \end{figure}
 155
 156 \subsubsection{Results}