From 7269acd9fbc6c20d4961ce6a5851bfee3a41cb4a Mon Sep 17 00:00:00 2001 From: Peter Wu Date: Tue, 13 Dec 2016 01:30:36 +0100 Subject: JobScheduling: formatting --- part1.tex | 9 +++++---- 1 file 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} -- cgit v1.2.1