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