JobScheduling: formatting

1 files changed, 5 insertions, 4 deletions

diff --git a/part1.tex b/part1.tex
index f92fb70..6944205 100644
--- a/part1.tex
+++ b/part1.tex
@@ -352,10 +352,11 @@ We can see the list of jobs as an array containing integers that represent the t
 We first created a rule for every job $j(i)$ that states that $j$ has to end before a decision variable $m$. 
 This can be written as $j(i) + i + 5 < m$.
 We initialized this variable as $m \gets 50$. From there on, we worked towards the smallest value for which the formula was satisfiable.
-We found this value to be $m = 59$. For $m = 58$, z3 returned \"unsat\".
-We also reformed all previously mentioned requirements into formula's that can be used in z3:
+We found this value to be $m = 59$. For $m = 58$, z3 returned \texttt{unsat}.
+We also reformed all previously mentioned requirements into formulae that can be
+used in z3 as shown in Listing~\ref{lst:jobScheduling}.
 
-\begin{lstlisting}
+\begin{lstlisting}[caption={SMT for Job Scheduling},label={lst:jobScheduling},language=lisp,basicstyle=\scriptsize]
 (and (>= j3 (+ j1 6)) (>= j3 (+ j2 7)))
 (and (>= j5 (+ j3 8)) (>= j5 (+ j4 9)))
 (and (>= j7 (+ j3 8)) (>= j7 (+ j4 9)) (>= j7 (+ j6 11)))
@@ -393,7 +394,7 @@ Note that $42 + 12 + 5$ is indeed equal to $59$.
 This solution was retrieved in the same way as answer a. This answer is $m = 65$.
 2 extra lines were added to ensure that job 6 lies within job 12:
 
-\begin{lstlisting}
+\begin{lstlisting}[language=lisp,basicstyle=\scriptsize]
 (>= j6 j12)
 (<= (+ j6 11) (+ j12 17))
 \end{lstlisting}