\end{itemize}
\subsection{SMT format solution}
-The formula is easily convertable to SMT format by literal conversion and is
-listed in Listing~\ref{listing:a1.bash}. The maximization is done by
-incrementing a special variable called \texttt{<REP>} which is an instantiation
-of $n(p)$. When the iteration yields unsat we know that the current number
-minus one is the maximum amount of prittles the trucks can carry. The
-maximization is done with a bash script shown in Listing~\ref{listing:1.bash}
-and visualized with the python script shown in Listing~\ref{listing:a1.py}
+The formula is easily convertable to SMT format by literal conversion. The
+maximization is done by incrementing a special variable called \texttt{<REP>}
+which is an instantiation of $n(p)$. When the iteration yields unsat we know
+that the current number minus one is the maximum amount of prittles the trucks
+can carry. The maximization is done with a bash script shown in
+Listing~\ref{listing:1.bash} and visualized with the python script.
\lstinputlisting[language=bash,firstline=66,
caption={Iteratively find the largest solution for problem 1},
\end{itemize}
\subsection{SMT format solution}
-The formula is easily convertable via a Python script to SMT format by literal
-conversion and said script is listed in Listing~\ref{listing:a2.bash}. The
-script optimizes a little bit from the original formula by leaving out the
-overlap checking between the same components. The solution is calculated using
-the command shown in Listing~\ref{listing:2.bash} and visualized with the
-python script shown in Listing~\ref{listing:a2.py}
-
-\lstinputlisting[language=bash,
- caption={Find the shortest solution for problem 3},
- label={listing:2.bash}]{src/a2.bash}
+The formula is easily convertable via a script to SMT format by literal
+conversion. The script optimizes a little bit from the original formula by
+leaving out the overlap checking between the same components.
\subsection{Solution}
Finding this solution takes less then $35$ seconds and is shown in
\subsection{SMT format solution}
The formula is easily convertable via a script to SMT format by literal
-conversion and said script is listed in Listing~\ref{listing:a3.bash}. The
-script optimizes a little bit from the original formula by leaving out the
-shared resource checking for the same jobs. The minimization is done by
-incrementing variable $T$ every time the current $T$ yields unsat with a bash
-script shown in Listing~\ref{listing:3.bash} and visualized with the python
-script shown in Listing~\ref{listing:a3.py}.
+conversion. The script optimizes a little bit from the original formula by
+leaving out the shared resource checking for the same jobs. The minimization is
+done by incrementing variable $T$ every time the current $T$ yields unsat with
+a bash script shown in Listing~\ref{listing:3.bash}.
\lstinputlisting[language=bash,firstline=46,
caption={Iteratively find the shortest solution for problem 3},
\subsection{SMT format solution}
The formula is easily convertable via a Python script to SMT format by literal
-conversion and said script is listed in Listing~\ref{listing:a4.bash}. The
-script optimizes a little bit from the original formula by leaving out the
-$i=j$ comparison in subformula 17 and 18 by removing them from the set looped
-over. The script also optimizes by not checking variables $a_0^n$ and $a_I^n$
-since they always stay the same anyways. The minimization is done by
-incrementing variable $N$ every time the current $N$ yields unsat with a bash
-script shown in Listing~\ref{listing:4.bash} and visualized with the python
-script shown in Listing~\ref{listing:a4.py}.
+conversion. The script optimizes a little bit from the original formula by
+leaving out the $i=j$ comparison in subformula 17 and 18 by removing them from
+the set looped over. The script also optimizes by not checking variables
+$a_0^n$ and $a_I^n$ since they always stay the same anyways. The minimization
+is done by incrementing variable $N$ every time the current $N$ yields unsat
+with a bash script shown in Listing~\ref{listing:4.bash}.
\lstinputlisting[language=bash,firstline=58,
caption={Iteratively find the shortest solution for problem 4},
+++ /dev/null
-\section{Appendix}\label{sec:appendix}
-\begin{lstlisting}[caption={Benchmark system}]
-OS: Linux 3.16.0-4-amd64 #1 SMP Debian 3.16 x86_64 GNU/Linux
-CPU: 3600MHz AMD FX(tm)-4100 Quad-Core Processor
-RAM: 8GB
-\end{lstlisting}
-
-\newpage
-\lstinputlisting[language=bash,caption={a1.bash},
- label={listing:a1.bash}]{src/a1.bash}
-\lstinputlisting[language=python,caption={a1.py},
- label={listing:a1.py}]{src/a1.py}
-
-\newpage
-\lstinputlisting[language=bash,caption={a2.bash},
- label={listing:a2.bash}]{src/a2.bash}
-\lstinputlisting[language=python,caption={a2.py},
- label={listing:a2.py}]{src/a2.py}
-
-\newpage
-\lstinputlisting[language=bash,caption={a3.bash},
- label={listing:a3.bash}]{src/a3.bash}
-\lstinputlisting[language=python,caption={a3.py},
- label={listing:a3.py}]{src/a3.py}
-
-\newpage
-\lstinputlisting[language=bash,caption={a4.bash},
- label={listing:a4.bash}]{src/a4.bash}
-\lstinputlisting[language=python,caption={a4.py},
- label={listing:a4.py}]{src/a4.py}
SMT-Lib format to yices after which the output is feeded to a Python script
that visualizes the solution. This means that for all problems $p$ for $p\in
\{1,\ldots, 4\}$ there exist $2$ files. \texttt{ap.bash} that generates the
-solution and \texttt{ap.py} that visualizes the solution. Both files are
-present in the Section~\ref{sec:appendix}. All solving is done on the benchmark
-system listed in Listing~\ref{listing:benchmark}.
+solution and \texttt{ap.py} that visualizes the solution. All solving is done
+on the benchmark system listed in Listing~\ref{listing:benchmark}.
\begin{lstlisting}[caption={Benchmark system},label={listing:benchmark}]
CPU: 3600MHz AMD FX(tm)-4100 Quad-Core Processor
\newpage
\input{4.tex}
-\newpage
-\input{a.tex}
-
\end{document}
repositories / ar1516.git / commitdiff