From: Mart Lubbers Date: Thu, 29 Oct 2015 18:18:37 +0000 (+0100) Subject: update X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=f2338a155560cdda53e8f621aa2a8a97c459cd20;p=ar1516.git update --- diff --git a/1.tex b/1.tex index ff39c58..0202521 100644 --- a/1.tex +++ b/1.tex @@ -78,13 +78,12 @@ going over all pallets. \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{} 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{} +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}, diff --git a/2.tex b/2.tex index d266aad..0d2b463 100644 --- a/2.tex +++ b/2.tex @@ -97,16 +97,9 @@ power components and only regular components. \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 diff --git a/3.tex b/3.tex index 9f24095..25de903 100644 --- a/3.tex +++ b/3.tex @@ -51,12 +51,10 @@ definition. \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}, diff --git a/4.tex b/4.tex index f2a929c..07cd2df 100644 --- a/4.tex +++ b/4.tex @@ -46,14 +46,12 @@ postcondition. \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}, diff --git a/a.tex b/a.tex deleted file mode 100644 index c5d9ce1..0000000 --- a/a.tex +++ /dev/null @@ -1,30 +0,0 @@ -\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} diff --git a/ar.tex b/ar.tex index f650658..7b5d21e 100644 --- a/ar.tex +++ b/ar.tex @@ -11,9 +11,8 @@ and therefore all problems have an accompanying bash script contains a function 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 @@ -36,7 +35,4 @@ Bash: 4.3.30(1) \newpage \input{4.tex} -\newpage -\input{a.tex} - \end{document}