JobScheduling: redo 3a

The report was too terse and incomplete. For example, the included code
was missing checks for the minimal time and the Java code contains a
strange check for the last constraint that seems wrong (did you mean
"or"?).

Just redo it, saves more time.

Also, the generate-jobscheduling.py scrypt contains dead code. I
originally planned to implement marking dependencies, but that is not
done.

3 files changed, 390 insertions, 38 deletions

diff --git a/job_scheduling/generate-jobscheduling.py b/job_scheduling/generate-jobscheduling.py
new file mode 100755
index 0000000..5cf9b04
--- /dev/null
+++ b/job_scheduling/generate-jobscheduling.py
@@ -0,0 +1,121 @@
+#!/usr/bin/env python
+# Usage for 3a (first argument is the deadline):
+#   $0 -1 | z3 -smt -in
+# Usage for 3b:
+#   $0 90 b | z3 -smt -in
+
+import sys
+
+# Deadline
+deadline = int(sys.argv[1])
+is_b = len(sys.argv) >= 3 and sys.argv[2] == 'b'
+
+
+# Number of jobs
+n = 12
+
+# For i: (j, ...), job i must not start before jobs j have ended.
+job_dependencies_ended = {
+    3:  (1, 2),
+    5:  (3, 4),
+    7:  (3, 4, 6),
+    9:  (5, 8),
+    11: (10,),
+    12: (9, 11),
+}
+
+job_dependencies_started = {
+    8: (5,),
+}
+
+job_durations = {
+    i: i + 5 for i in range(1, n + 1)
+}
+
+
+def fillin(cases, template_vars):
+    if type(cases) == str:
+        return cases.format(**template_vars)
+    return [template.format(**template_vars) for template in cases]
+
+literals = []
+preds = []
+
+# Start time of all jobs
+# and their duration
+for i in range(1, n + 1):
+    literals += fillin([
+        "t{i}",
+        "d{i}",
+    ], vars())
+    # times must be positive and
+    # all jobs must finish before the deadline.
+    preds += fillin([
+        "(>= t{i} 0)",
+        "(<= (+ t{i} d{i}) {deadline})",
+    ], vars())
+
+# Define duration
+for i, duration in job_durations.items():
+    preds += fillin([
+        "(= d{i} {duration})"
+    ], vars())
+
+# Job i may not start before job(s) j have *ended*. Or:
+# for all j: t_j + d_j <= t_i
+for i, deps in job_dependencies_ended.items():
+    for j in deps:
+        preds += fillin([
+            "(<= (+ t{j} d{j}) t{i})"
+        ], vars())
+
+# Job i may not start before job(s) j have *started*. Or:
+# for all j: t_j <= t_i
+for i, deps in job_dependencies_started.items():
+    for j in deps:
+        preds += fillin([
+            "(<= t{j} t{i})"
+        ], vars())
+
+# Jobs 5, 7 en 10 require a special equipment of which only one copy is
+# available, so no two of these jobs may run at the same time.
+# Or:
+# There must exist a pair of jobs (i, j) s.t. one starts after another ended:
+# t_i + d_i <= t_j
+jobs_max2_for_3 = (5, 7, 10)
+altpreds = []
+for i in jobs_max2_for_3:
+    for j in jobs_max2_for_3:
+        if i == j:
+            continue
+        altpreds += fillin([
+            "(<= (+ t{i} d{i}) t{j})"
+        ], vars())
+
+preds += ["(or %s)" % " ".join(altpreds)]
+
+# Begin generator
+s = """(benchmark test.smt
+:logic QF_UFLIA
+:extrafuns
+(
+"""
+s += "\n".join("(%s Int)" % x for x in literals)
+s += """
+)
+:formula
+(and
+"""
+s += "\n".join(preds)
+s += """
+))
+"""
+
+try:
+    import sys
+    print(s)
+    # Hack to avoid printing a ugly error in case stdin of next pipe is closed.
+    sys.stdout.flush()
+    sys.stdout.close()
+except BrokenPipeError:
+    pass
diff --git a/job_scheduling/jobschedule-to-latex.py b/job_scheduling/jobschedule-to-latex.py
new file mode 100755
index 0000000..057dc84
--- /dev/null
+++ b/job_scheduling/jobschedule-to-latex.py
@@ -0,0 +1,134 @@
+#!/usr/bin/env python3
+import re
+import sys
+
+job_dependencies_ended = {
+    3:  (1, 2),
+    5:  (3, 4),
+    7:  (3, 4, 6),
+    9:  (5, 8),
+    11: (10,),
+    12: (9, 11),
+}
+
+job_dependencies_started = {
+    8: (5,),
+}
+
+# Styling parameter: Sum of these must be smaller than 6, otherwise small
+# duration cannot be represented.
+leftSize, rightSize = 1, 1
+leftSize, rightSize = 0, 0  # set to 0 to disable this feature
+# Scale time to dimension
+timeScale = .2
+# Height of a row
+rowSize = .5
+# Margin on top and bottom of a row (twice this must be smaller than height)
+rowMargin = .1
+
+# Predefined colors from https://en.wikibooks.org/wiki/LaTeX/PGF/TikZ#Color
+colors = [
+'red',
+'green',
+'blue',
+'cyan',
+'magenta',
+#'yellow',
+#'black',
+'gray',
+'darkgray',
+'lightgray',
+'brown',
+#'lime',
+'olive',
+'orange',
+'pink',
+'purple',
+'teal',
+'violet',
+#'white',
+]
+
+
+# Map of job numbers to their start time and duration
+# To be sorted by start time and job number
+jobs = {}
+
+for line in sys.stdin:
+    line = line.strip()
+    if line == "unsat":
+        sys.exit('unsat!')
+    if line == "sat":
+        continue
+    m = re.match(r'([dt])(\d+) -> (\d+)', line)
+    what = m.group(1)
+    jobnr = int(m.group(2))
+    # start time if what=='t',
+    # duration if what=='d'
+    time = int(m.group(3))
+
+    if jobnr not in jobs:
+        jobs[jobnr] = [None] * 2
+    jobs[jobnr][0 if what == 't' else 1] = time
+
+def job_key_func(item):
+    jobnr, (startTime, duration) = item
+    # Assume max job nr below large number
+    return startTime * 10000 + jobnr
+
+
+def draw_box(rownr, x1, x2):
+    # Tikz draw in Cartesian space
+    lastRow = len(jobs)
+    y1 = (lastRow - rownr) * rowSize + rowMargin
+    y2 = (lastRow - rownr + 1) * rowSize - rowMargin
+
+    attrs = []
+    # Add color
+    attrs += ["draw=%s" % colors[i]]
+    attrs += ["fill=%s" % colors[i]]
+
+    attrs = ','.join(attrs)
+
+    tpl = r"\draw[{attrs}] ({x1}, {y1}) rectangle ({x2}, {y2});"
+    print(tpl.format(**vars()))
+
+for i, (jobnr, (startTime, duration)) in enumerate(sorted(jobs.items(), key=job_key_func)):
+    line = ""
+
+    # Scale
+    startTimeX = startTime * timeScale
+    durationX = duration * timeScale
+
+    middleX1 = startTimeX
+    if jobnr in job_dependencies_started:
+        middleX1 += leftSize
+
+    middleX2 = startTimeX + durationX
+    if jobnr in job_dependencies_ended:
+        middleX2 -= rightSize
+
+    if middleX1 != startTimeX:
+        draw_box(i, startTimeX, middleX1,
+                job_dependencies_started[jobnr])
+    draw_box(i, middleX1, middleX2)
+    if middleX2 != startTimeX + durationX:
+        draw_box(i, middleX2, startTimeX + durationX,
+                job_dependencies_ended[jobnr])
+    tpl = r"\draw[{attrs}] ({x1}, {y1}) rectangle ({x2}, {y2});"
+
+    texty = (len(jobs) - i) * rowSize + .2
+    # Print jobnr on the left side
+    print(r'\node[anchor=east] at (%f,%f) {%s};' % (-.1, texty, jobnr))
+    # Print start and duration on the right side
+    print(r'\node[anchor=west] at (%f,%f) {%s};' % (startTimeX + durationX + .1, texty,
+        "%d + %d = %d" % (startTime, duration, startTime + duration)))
+
+# Print jobs as follows:
+# a bar (width is duration, height is same for all jobs).
+#   color is unique
+#   y position depends on order (sort by start time, then job number)
+# display job number on the side
+# display dependencies on the right or:
+#   color left side with start dependency
+#   color right side with end dependency
diff --git a/part1.tex b/part1.tex
index b1242ce..c33fb6c 100644
--- a/part1.tex
+++ b/part1.tex
@@ -534,47 +534,144 @@ no two of these jobs may run at the same time.
 
 \subsection*{Solution:}
 \subsubsection*{(a)}
-We can see the list of jobs as an array containing integers that represent the time at which a job starts. 
-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 \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}[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)))
-(>= j8 j5)
-(and (>= j9 (+ j5 10)) (>= j9 (+ j8 13)))
-(>= j11 (+ j10 15))
-(and (>= j12 (+ j9 14)) (>= j12 (+ j11 16)))
-(=> (<= j5 j7) (<= (+ j5 10) j7))
-(=> (<= j5 j10) (<= (+ j5 10) j10))
-(=> (<= j7 j5) (<= (+ j7 12) j5))
-(=> (<= j7 j10) (<= (+ j7 12) j10))
-(=> (<= j10 j5) (<= (+ j10 15) j5))
-(=> (<= j10 j7) (<= (+ j10 15) j7))
-\end{lstlisting}
+The problem can be generalized to scheduling of $n$ jobs $J$, where each job $i
+\in J$ has a start time $t_i$ and a duration $d_i$. Job dependencies can also be
+described in an abstract manner:
+\begin{itemize}
+\item Let $E$ be the set of jobs that requires other jobs to be finished before
+    it can start. Let $E_i$ be the required jobs for a job $i \in E$.
+\item Let $S$ be the set of jobs that requires other jobs to be started before
+    it can start. Let $S_i$ be the required jobs for a job $i \in S$.
+\end{itemize}
+The goal is to find the minimal total running time, that is, deadline $D$.
 
-The complete scheduling output, where an integer represents the time at which a job was started is as follows:
-\begin{lstlisting}
-j1 -> 1
-j2 -> 0
-j3 -> 7
-j4 -> 0
-j5 -> 15
-j6 -> 0
-j7 -> 25
-j8 -> 15
-j9 -> 28
-j10 -> 0
-j11 -> 15
-j12 -> 42
+Now we can start listing the ingredients. First a sanity check, we assume that
+the time starts counting from zero to make calculations easier:
+\begin{align}
+\label{eq:sched1}
+\bigwedge_{i=1}^n t_i \geq 0
+\end{align}
+
+Job $i$ may not start before jobs $E_i$ have finished:
+\begin{align}
+\label{eq:sched2}
+\bigwedge_{i \in E}
+\bigwedge_{j \in E_i}
+t_j + d_j \leq t_i
+\end{align}
+
+Job $i$ may not start before jobs $S_i$ have started:
+\begin{align}
+\label{eq:sched3}
+\bigwedge_{i \in S}
+\bigwedge_{j \in S_i}
+t_j \leq t_i
+\end{align}
+
+Let $RL \subseteq J$ be the set of three resource limited jobs. The constraint
+that at most two jobs of this set can run in parallel can alternatively be
+described as: any of the three jobs must not start before another of the three
+has finished. When this holds, then for sure we have at most two concurrent
+jobs. This can be expressed as:
+\begin{align}
+\label{eq:sched4}
+\bigvee_{i,j \in RL, i \neq j}
+t_i + d_i \leq t_j
+\end{align}
+
+To establish whether the resulting job scheduling is indeed minimal, we add an
+additional constraint to check whether all jobs complete before the deadline:
+\begin{align}
+\label{eq:sched5}
+\bigwedge_{i=1}^n t_i + d_i \geq D
+\end{align}
+
+The conjunction of the above ingredients \ref{eq:sched1}, \ref{eq:sched2},
+\ref{eq:sched3}, \ref{eq:sched4} and \ref{eq:sched5} are put in a generator
+script which outputs a SMT program (shown in Listing~\ref{lst:jobScheduling}. We
+run it with \texttt{python generate-jobscheduling.py | z3 -smt -in} which
+completes in 40 milliseconds. Its result is shown in
+Figure~\ref{fig:jobScheduling}. To confirm that this job schedule is indeed
+minimal, we set $D=58$ and observe that the program outputs ``unsat'' within 40
+milliseconds.
+
+\begin{figure}[H]
+\centering
+\begin{tikzpicture}
+%
+\draw[draw=red,fill=red] (0.0, 6.1) rectangle (1.2000000000000002, 6.4);
+\node[anchor=east] at (-0.100000,6.200000) {1};
+\node[anchor=west] at (1.300000,6.200000) {0 + 6 = 6};
+\draw[draw=green,fill=green] (0.0, 5.6) rectangle (1.4000000000000001, 5.9);
+\node[anchor=east] at (-0.100000,5.700000) {2};
+\node[anchor=west] at (1.500000,5.700000) {0 + 7 = 7};
+\draw[draw=blue,fill=blue] (0.0, 5.1) rectangle (1.8, 5.4);
+\node[anchor=east] at (-0.100000,5.200000) {4};
+\node[anchor=west] at (1.900000,5.200000) {0 + 9 = 9};
+\draw[draw=cyan,fill=cyan] (0.0, 4.6) rectangle (2.2, 4.9);
+\node[anchor=east] at (-0.100000,4.700000) {6};
+\node[anchor=west] at (2.300000,4.700000) {0 + 11 = 11};
+\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] (2.2, 3.6) rectangle (5.2, 3.9);
+\node[anchor=east] at (-0.100000,3.700000) {10};
+\node[anchor=west] at (5.300000,3.700000) {11 + 15 = 26};
+\draw[draw=darkgray,fill=darkgray] (3.0, 3.1) rectangle (5.0, 3.4);
+\node[anchor=east] at (-0.100000,3.200000) {5};
+\node[anchor=west] at (5.100000,3.200000) {15 + 10 = 25};
+\draw[draw=lightgray,fill=lightgray] (3.0, 2.6) rectangle (5.6, 2.9);
+\node[anchor=east] at (-0.100000,2.700000) {8};
+\node[anchor=west] at (5.700000,2.700000) {15 + 13 = 28};
+\draw[draw=brown,fill=brown] (5.0, 2.1) rectangle (7.4, 2.4);
+\node[anchor=east] at (-0.100000,2.200000) {7};
+\node[anchor=west] at (7.500000,2.200000) {25 + 12 = 37};
+\draw[draw=olive,fill=olive] (5.2, 1.6) rectangle (8.4, 1.9);
+\node[anchor=east] at (-0.100000,1.700000) {11};
+\node[anchor=west] at (8.500000,1.700000) {26 + 16 = 42};
+\draw[draw=orange,fill=orange] (5.6000000000000005, 1.1) rectangle (8.4, 1.4);
+\node[anchor=east] at (-0.100000,1.200000) {9};
+\node[anchor=west] at (8.500000,1.200000) {28 + 14 = 42};
+\draw[draw=pink,fill=pink] (8.4, 0.6) rectangle (11.8, 0.9);
+\node[anchor=east] at (-0.100000,0.700000) {12};
+\node[anchor=west] at (11.900000,0.700000) {42 + 17 = 59};
+%
+\end{tikzpicture}
+\caption{\label{fig:jobScheduling}Result of job scheduling for (a).}
+\end{figure}
+
+\begin{lstlisting}[
+    caption={Generated SMT program for job scheduling problem (a).},
+    label={lst:jobScheduling},basicstyle=\scriptsize
+]
+(benchmark test.smt
+:logic QF_UFLIA
+:extrafuns (
+(t1 Int) (d1 Int) (t2 Int) (d2 Int) (t3 Int) (d3 Int)
+(t4 Int) (d4 Int) (t5 Int) (d5 Int) (t6 Int) (d6 Int)
+(t7 Int) (d7 Int) (t8 Int) (d8 Int) (t9 Int) (d9 Int)
+(t10 Int) (d10 Int) (t11 Int) (d11 Int) (t12 Int) (d12 Int)
+)
+:formula (and
+(>= t1 0) (<= (+ t1 d1) 59) (>= t2 0) (<= (+ t2 d2) 59)
+(>= t3 0) (<= (+ t3 d3) 59) (>= t4 0) (<= (+ t4 d4) 59)
+(>= t5 0) (<= (+ t5 d5) 59) (>= t6 0) (<= (+ t6 d6) 59)
+(>= t7 0) (<= (+ t7 d7) 59) (>= t8 0) (<= (+ t8 d8) 59)
+(>= t9 0) (<= (+ t9 d9) 59) (>= t10 0) (<= (+ t10 d10) 59)
+(>= t11 0) (<= (+ t11 d11) 59) (>= t12 0) (<= (+ t12 d12) 59)
+(= d1 6) (= d2 7) (= d3 8) (= d4 9)
+(= d5 10) (= d6 11) (= d7 12) (= d8 13)
+(= d9 14) (= d10 15) (= d11 16) (= d12 17)
+(<= (+ t1 d1) t3) (<= (+ t2 d2) t3) (<= (+ t3 d3) t5)
+(<= (+ t4 d4) t5) (<= (+ t3 d3) t7) (<= (+ t4 d4) t7)
+(<= (+ t6 d6) t7) (<= (+ t5 d5) t9) (<= (+ t8 d8) t9)
+(<= (+ t10 d10) t11) (<= (+ t9 d9) t12) (<= (+ t11 d11) t12)
+(<= t5 t8)
+(or (<= (+ t5 d5) t7) (<= (+ t5 d5) t10) (<= (+ t7 d7) t5)
+    (<= (+ t7 d7) t10) (<= (+ t10 d10) t5) (<= (+ t10 d10) t7))
+))
 \end{lstlisting}
 
-Note that $42 + 12 + 5$ is indeed equal to $59$.
 
 \subsubsection*{(b)}
 This solution was retrieved in the same way as answer a. This answer is $m = 65$.