From 079f4e83761c34ada419e0fd3d4642ba5b922d3c Mon Sep 17 00:00:00 2001 From: Peter Wu Date: Wed, 14 Dec 2016 22:28:59 +0100 Subject: 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. --- job_scheduling/generate-jobscheduling.py | 121 +++++++++++++++++++++ job_scheduling/jobschedule-to-latex.py | 134 ++++++++++++++++++++++++ part1.tex | 173 ++++++++++++++++++++++++------- 3 files changed, 390 insertions(+), 38 deletions(-) create mode 100755 job_scheduling/generate-jobscheduling.py create mode 100755 job_scheduling/jobschedule-to-latex.py 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$. -- cgit v1.2.1