diff options
Diffstat (limited to 'part1.tex')
| -rw-r--r-- | part1.tex | 173 |
1 files changed, 135 insertions, 38 deletions
@@ -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$. |