final ar

[master.git] / ar / assignment1 / 4.tex

diff --git a/ar/assignment1/4.tex b/ar/assignment1/4.tex
index 153cfec..68b3242 100644 (file)
--- a/ar/assignment1/4.tex
+++ b/ar/assignment1/4.tex
@@ -46,21 +46,21 @@ 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.py}. The Python
-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
+conversion and said script is listed in Listing~\ref{listing:a4.bash}. The
+Python 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,
+\lstinputlisting[language=bash,firstline=58,
        caption={Iteratively find the shortest solution for problem 4},
        label={listing:4.bash}]{src/a4.bash}
 
 \subsection{Solution}
 The bash script finds and shows the minimal solution in which the postcondition
-is satisfied for $N=11$. Finding this solution takes less then $75$ seconds and
+is satisfied for $N=10$. Finding this solution takes less then $75$ seconds and
 is shown in Table~\ref{tab:s4}.
 
 Every line in the table represents the iteration and the bold items represent