some updates

diff --git a/report2/implementation.tex b/report2/implementation.tex
index c69d4a1..539f5a6 100644 (file)
--- 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\\