\section{Results \& How-to}
\subsection{Results}
This approach is not very efficient yet. While it is a bit faster than the
previous \textsc{NuSMV} approach it is not capable of handling bigger screens.

\begin{tabular}{lll}
	\toprule
	Screen no. & \textsc{NuSMV} & This program\\
	\midrule
	$2000$ & $n$ & $n$\\
	\bottomrule
\end{tabular}

\subsection{How-to}
The program can be built by running \texttt{make}. \texttt{make} 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  LURD verification strategy
    -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}
