From 21c2841183f92fffd08e68ea6b09fd42aa92b7c6 Mon Sep 17 00:00:00 2001 From: Alexander Fedotov Date: Thu, 21 Apr 2016 22:18:59 +0200 Subject: [PATCH] implementation update --- report2/implementation.tex | 86 +++++++++++++++++++++----------------- 1 file changed, 48 insertions(+), 38 deletions(-) diff --git a/report2/implementation.tex b/report2/implementation.tex index 0f84b72..3f4ee6a 100644 --- a/report2/implementation.tex +++ b/report2/implementation.tex @@ -9,9 +9,8 @@ Let $T=\{free,box,target,agent,targetagent,targetbox\}$ be the set of possible 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\\ @@ -23,12 +22,8 @@ $$encode(t)=\begin{cases} 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\\ @@ -42,34 +37,50 @@ $$\delta_{(x,y)}(m)=\begin{cases} (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} @@ -80,7 +91,7 @@ $targetbox$ tiles. 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] @@ -108,8 +119,7 @@ results in the second representation in Listing~\ref{lst:toy}. \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] @@ -129,7 +139,7 @@ the BDD shown in Figure~\ref{fig:toy2}. \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 -- 2.20.1