a1/3.tex

   1 \section{Problem 2}
   2 {\em
   3 Twelve jobs numbered from 1 to 12 have to be executed satisfying the following
   4 requirements:
   5 \begin{itemize}
   6         \item The running time of job $i$ is $i$, for $i=1,\ldots,12$
   7         \item All jobs run without interrupt.
   8         \item Job 3 may only start if jobs 1 and 2 have been finished.
   9         \item Job 5 may only start if jobs 3 and 4 have been finished.
  10         \item Job 7 may only start if jobs 3, 4 and 6 have been finished.
  11         \item Job 9 may only start if jobs 5 and 8 have been finished
  12         \item Job 11 may only start if job 10 has been finished.
  13         \item Job 12 may only start if jobs 9 and 11 have been finished.
  14         \item Jobs 5,7 en 10 require a special equipment of which only one copy
  15                 is available, so no two of these jobs may run at the same time.
  16 \end{itemize}
  17
  18 Find a solution of this scheduling problem for which the total running time is
  19 minimal.
  20 }
  21
  22 \subsection{Formal definition}
  23 For every job $j_{i}$ for $i\in J$ where $J=\{1,\ldots,12\}$ we define variable
  24 $j_{i}s$ for starting time. All jobs that have a shared resource we group as
  25 $J'=\{5,7,10\}$ and we define a function $p(i)$ that returns a set of all
  26 dependencies of job $i$. The total time it takes for all jobs to finish is $T$.
  27
  28 This leads to the following formalization where we minimize $T$.
  29 \begin{align}
  30         \bigwedge_{i\in J}\Biggl(
  31                 & j_{i}>0\wedge j_{i}+i<T\\
  32                 & \wedge \bigwedge_{k\in p(i)} j_{i}>j_{k}+k\Biggr)\\
  33                 & \wedge \bigwedge_{i\in J'}\bigwedge_{k\in J'}
  34                 i=j\vee j_{i}>j_{k}+k \vee j_{i}+i<j_{k}
  35 \end{align}
  36
  37 Every numbered subformula describes a group of constraints from the problem
  38 definition.
  39 \begin{itemize}
  40         \setcounter{enumi}{12}
  41         \item Makes sure that starting times are positive and that all jobs
  42                 finish before $T$.
  43         \item Makes sure that job may not start before all their dependencies
  44                 are finished by stating that they start strictly after their
  45                 dependency.
  46         \item Makes sure that never two more jobs use the shared resource by
  47                 stating that they either ends strictly before the other or
  48                 start strictly after the other.
  49 \end{itemize}
  50
  51 \subsection{SMT format solution}
  52 The formula is easily convertable via a script to SMT format by literal
  53 conversion. The script optimizes a little bit from the original formula by
  54 leaving out the shared resource checking for the same jobs. The minimization is
  55 done by incrementing variable $T$ every time the current $T$ yields unsat with
  56 a bash script shown in Listing~\ref{listing:3.bash}.
  57
  58 \lstinputlisting[language=bash,firstline=46,
  59         caption={Iteratively find the shortest solution for problem 3},
  60         label={listing:3.bash}]{src/a3.bash}
  61
  62 \subsection{Solution}
  63 The bash script finds and shows the minimal solution in which all jobs are
  64 finished in $37$ time units. Finding this solution takes less then $0.42$
  65 seconds and is shown in Table~\ref{tab:s3}.
  66
  67 The bold items represent the jobs using shared resources.
  68
  69 \begin{table}[H]
  70         \centering
  71         \input{a3.tex}
  72 \label{tab:s3}
  73         \caption{Solution visualization for problem 3}
  74 \end{table}