\section{Results \& How-to}
\subsection{Results}
This approach is not very efficient yet. Below are some execution times for
several screens:

\begin{tabular}{llll}
	\toprule
	Screen no. & Boxes & Size & Time\\
	\midrule
	$2000$ & $1$ & $12$ & $0.05s$\\
	$107$ & $3$ & $16$ & $1.19s$\\
	$101$ & $3$ & $20$ & $1.49s$\\
	$102$ & & $0.66s$\\
	$103$ & & $1.02s$\\
	$104$ & & $1.39s$\\
	$105$ & & $1.70s$\\
	\bottomrule
\end{tabular}

\subsection{How-to}
The latest version of the modelchecker can be obtained by cloning the
repository, building sylvan and building the modelchecker with the following
commands:

\begin{lstlisting}
$ git clone --recursive https://github.com/dopefishh/mc1516pa.git
$ cd mc1516pa/modelchecker/sylvan
$ cmake .
$ make
$ cd ..
$ make
\end{lstlisting}

The makefile of the modelchecker expects the sylvan headers to be located in
\texttt{./sylvan/src} and the library archive in
\texttt{./sylvan/src/libsylvan.a}. If this is not the case one can adapt the
makefile or set the appropriate \texttt{CFLAGS} and \texttt{LDFLAGS}.

When the main program is executed with the \texttt{-h} flag the help is shown.
Note that the program is very silent when the \texttt{-v} flag is not set.
\begin{lstlisting}
Usage:
    ./main [opts] [FILE]

Options:
    -l LURD  initial LURD
    -v       enable verbose output
    -h       show this help

Positional arguments:
    FILE     zero or one sokoban screens
             when no file is specified stdin will be used
\end{lstlisting}

\subsection{Extra 1: Initial LURD}
Using the \texttt{-l} option the user can give a initial LURD to the program.
LURD stands for Left, Up, Right, Down sequence and is a string consisting only
of $l,u,r,d$ characters and it specifies the initial moves to be taken by the
agent. To achieve this we simple for every character in the LURD update the
initial state with the relative product of the transitions belonging to the
correct direction. After that the problem is solved as usual and thus notifying
the user whether the LURD leads to a solvable state. Note that when the LURD is
empty the program behaves like there was no LURD given.

\subsection{Evaluation}
The assignment was a very interesting and challenging assignment. However, we
feel that we could not get the most out of it due to several reasons.

First of all it was a hassle to get to know sylvan and to be able to use the
package. The most problematic was to understand how can we work with state
transitions efficiently. The way it works with sylvan was not evident neither
from the introductory lectures, nor from the available documentation. Also,
there were some trivial errors in the sylvan package that made debugging a lot
harder. One of those errors was malformed dot output for printing BDDs. In the
meantime we have made a pullrequest to fix that.

Secondly, due to the relatively short introduction to BDDs the gap between our
knowledge and the knowledge required to build such a solver is quite big. This
lead to startup problems (which we managed to solve, but lost too much time to it).

Finally, we feel a bit frustrated that we only finished and tested the
reachability of a goal state checking, but did not finish the extraction of
solving sequences. We have a solution for that problem, which shows potential,
but still contains bugs.

\subsubsection{Division of work}
The work was divided evenly in the beginning of the project. When we noticed
that we did not have enough time to implement two solutions or even a hybrid
approach we decided to go through with the solution that seemed the most
doable. In the next phase of the project Alexander did more of the programming
and Mart more on the report. Cumulatively we spent a lot of time on it.
