JobScheduling: finish 3b

Previous answer was correct, but rewriting it to fit the variables used
in part (a). Also adding a picture.

2 files changed, 60 insertions, 23 deletions

diff --git a/job_scheduling/generate-jobscheduling.py b/job_scheduling/generate-jobscheduling.py
index 5cf9b04..e387c48 100755
--- a/job_scheduling/generate-jobscheduling.py
+++ b/job_scheduling/generate-jobscheduling.py
@@ -94,6 +94,12 @@ for i in jobs_max2_for_3:
 
 preds += ["(or %s)" % " ".join(altpreds)]
 
+# Job 6 may only run when job 12 is running.
+if is_b:
+    preds += [
+        "(and (<= t12 t6) (<= (+ t6 d6) (+ t12 d12)))"
+    ]
+
 # Begin generator
 s = """(benchmark test.smt
 :logic QF_UFLIA
diff --git a/part1.tex b/part1.tex
index c33fb6c..b4763cc 100644
--- a/part1.tex
+++ b/part1.tex
@@ -674,31 +674,62 @@ milliseconds.
 
 
 \subsubsection*{(b)}
-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:
+The extra constraint states that job 6 may only be run when it fits within the
+scheduled time of job 12:
+\begin{align}
+\label{eq:sched6}
+t_{12} \leq t_6 \land t_6 + d_6 \leq t_{12} + d_{12}
+\end{align}
 
-\begin{lstlisting}[language=lisp,basicstyle=\scriptsize]
-(>= j6 j12)
-(<= (+ j6 11) (+ j12 17))
-\end{lstlisting}
+After modifying the program from (a) by adding \texttt{(and (<= t12 t6) (<= (+
+t6 d6) (+ t12 d12)))} to the formula, a satisfying assignment was found for
+$D=65$ in 50 milliseconds (shown in Figure~\ref{fig:jobSchedulingB}). For
+$D=64$, ``unsat'' was output (in 50ms).
 
-With those 2 extra formula lines, the new schedule becomes:
-
-\begin{lstlisting}
-j1 -> 1
-j2 -> 0
-j3 -> 7
-j4 -> 0
-j5 -> 15
-j6 -> 42
-j7 -> 53
-j8 -> 15
-j9 -> 28
-j10 -> 0
-j11 -> 15
-j12 -> 42
-\end{lstlisting}
-Note that $53 + 7 + 5$ is indeed equal to $65$.
+\begin{figure}[H]
+\centering
+\begin{tikzpicture}
+%
+\draw[draw=red,fill=red] (0.0, 6.1) rectangle (1.4000000000000001, 6.4);
+\node[anchor=east] at (-0.100000,6.200000) {2};
+\node[anchor=west] at (1.500000,6.200000) {0 + 7 = 7};
+\draw[draw=green,fill=green] (0.0, 5.6) rectangle (1.8, 5.9);
+\node[anchor=east] at (-0.100000,5.700000) {4};
+\node[anchor=west] at (1.900000,5.700000) {0 + 9 = 9};
+\draw[draw=blue,fill=blue] (0.0, 5.1) rectangle (3.0, 5.4);
+\node[anchor=east] at (-0.100000,5.200000) {10};
+\node[anchor=west] at (3.100000,5.200000) {0 + 15 = 15};
+\draw[draw=cyan,fill=cyan] (0.2, 4.6) rectangle (1.4000000000000001, 4.9);
+\node[anchor=east] at (-0.100000,4.700000) {1};
+\node[anchor=west] at (1.500000,4.700000) {1 + 6 = 7};
+\draw[draw=magenta,fill=magenta] (1.4000000000000001, 4.1) rectangle (3.0, 4.4);
+\node[anchor=east] at (-0.100000,4.200000) {3};
+\node[anchor=west] at (3.100000,4.200000) {7 + 8 = 15};
+\draw[draw=gray,fill=gray] (3.0, 3.6) rectangle (5.0, 3.9);
+\node[anchor=east] at (-0.100000,3.700000) {5};
+\node[anchor=west] at (5.100000,3.700000) {15 + 10 = 25};
+\draw[draw=darkgray,fill=darkgray] (3.0, 3.1) rectangle (5.6, 3.4);
+\node[anchor=east] at (-0.100000,3.200000) {8};
+\node[anchor=west] at (5.700000,3.200000) {15 + 13 = 28};
+\draw[draw=lightgray,fill=lightgray] (3.0, 2.6) rectangle (6.2, 2.9);
+\node[anchor=east] at (-0.100000,2.700000) {11};
+\node[anchor=west] at (6.300000,2.700000) {15 + 16 = 31};
+\draw[draw=brown,fill=brown] (5.6000000000000005, 2.1) rectangle (8.4, 2.4);
+\node[anchor=east] at (-0.100000,2.200000) {9};
+\node[anchor=west] at (8.500000,2.200000) {28 + 14 = 42};
+\draw[draw=olive,fill=olive] (8.4, 1.6) rectangle (10.600000000000001, 1.9);
+\node[anchor=east] at (-0.100000,1.700000) {6};
+\node[anchor=west] at (10.700000,1.700000) {42 + 11 = 53};
+\draw[draw=orange,fill=orange] (8.4, 1.1) rectangle (11.8, 1.4);
+\node[anchor=east] at (-0.100000,1.200000) {12};
+\node[anchor=west] at (11.900000,1.200000) {42 + 17 = 59};
+\draw[draw=pink,fill=pink] (10.600000000000001, 0.6) rectangle (13.000000000000002, 0.9);
+\node[anchor=east] at (-0.100000,0.700000) {7};
+\node[anchor=west] at (13.100000,0.700000) {53 + 12 = 65};
+%
+\end{tikzpicture}
+\caption{\label{fig:jobSchedulingB}Result of job scheduling for (b).}
+\end{figure}
 
 \section*{Problem: Integer sum from neighbors}
 Eight integer variables $a_1$, $a_2$, $a_3$, $a_4$, $a_5$, $a_6$, $a_7$, $a_8$