From: Alexander Fedotov <soyaxhoya@gmail.com>
Date: Thu, 21 Apr 2016 19:18:27 +0000 (+0200)
Subject: some updates
X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=5bfa4e26b72ceb05a859f612306484c19f2abf0c;p=mc1516pa.git

some updates
---

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\\