Update report

[mc1516pa.git] / report2 / implementation.tex

diff --git a/report2/implementation.tex b/report2/implementation.tex
index b4a1d77..c69d4a1 100644 (file)
--- a/report2/implementation.tex
+++ b/report2/implementation.tex
@@ -75,8 +75,27 @@ $$next(i_1, i_2, i_3)=\left\{\begin{array}{lp{2pt}l}
 Encoding the goal state is very trivial. Just make sure all $target$ tiles are
 $targetbox$ tiles.
 
-\subsection{Lurd extraction}
-%TODO
+\subsection{Algorithm}
+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
+solution.
+
+\begin{algorithm}[H]
+       \KwIn{I, Initial state BDD}
+       \KwIn{$R_i$, List of transition BDDs}
+       \KwIn{G, Goal BDD}
+       $V_{old}\leftarrow BDDempty$\;
+       $V_{new}\leftarrow I$\;
+       \While{$V_{new}\neq V_{old}$}{
+               $V_{old}\leftarrow V_{new}$\;
+               \ForEach{$R_i$}{
+                       $V_{new}\leftarrow BDDapply(\vee, V_{new}, BDDrelprod(V_{new}, R_i)$\;
+               }
+               \lIf{$BDDsatcount(BDDand(G, new))>0$}{$break$}
+       }
+\end{algorithm}
 
 \subsection{Example}
 For example, take the toy screen shown as the first representation in