From 5bfa4e26b72ceb05a859f612306484c19f2abf0c Mon Sep 17 00:00:00 2001 From: Alexander Fedotov Date: Thu, 21 Apr 2016 21:18:27 +0200 Subject: [PATCH] some updates --- report2/implementation.tex | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/report2/implementation.tex b/report2/implementation.tex index c69d4a1..539f5a6 100644 --- a/report2/implementation.tex +++ b/report2/implementation.tex @@ -23,11 +23,12 @@ $$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$ variable which represent the change in coordinate value -respectively for the next position and the position next to the next postition. +\{\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. $$\delta_{(x,y)}(m)=\begin{cases} (x-1, y) & \text{if } m = left\\ (x+1, y) & \text{if } m = right\\ @@ -45,9 +46,9 @@ We define the tile update function $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 } & + (free, agent, box) & \text{if } & i_1=agent \wedge i_2=box \wedge i_3=free\\ - (target, agent, box) & \text{if } & + (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\\ -- 2.20.1