\section{Problem 2}
{\em
Twelve jobs numbered from 1 to 12 have to be executed satisfying the following
requirements:
\begin{itemize}
	\item The running time of job $i$ is $i$, for $i=1,\ldots,12$
	\item All jobs run without interrupt.
	\item Job 3 may only start if jobs 1 and 2 have been finished.
	\item Job 5 may only start if jobs 3 and 4 have been finished.
	\item Job 7 may only start if jobs 3, 4 and 6 have been finished.
	\item Job 9 may only start if jobs 5 and 8 have been finished
	\item Job 11 may only start if job 10 has been finished.
	\item Job 12 may only start if jobs 9 and 11 have been finished.
	\item 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.
\end{itemize}

Find a solution of this scheduling problem for which the total running time is
minimal.
}

\newpage
\subsection{Formal definition}
For every job $j_{i}$ for $i\in J$ where $J=\{1,\ldots,12\}$ we define variable
$j_{i}s$ for starting time. All jobs that have a shared resource we group as
$J'=\{5,7,10\}$ and we define a function $p(i)$ that returns a set of all
dependencies of job $i$. The total time it takes for all jobs to finish is $T$.

This leads to the following formalization where we minimize $T$.
\begin{align}
	\bigwedge_{i\in J}\Biggl( 
		& j_{i}>0\wedge j_{i}+i<T\\
		& \wedge \bigwedge_{k\in p(i)} j_{i}>j_{k}+k\Biggr)\\
		& \wedge \bigwedge_{i\in J'}\bigwedge_{k\in J'}
		i=j\vee j_{i}>j_{k}+k \vee j_{i}+i<j_{k}
\end{align}

Every numbered subformula describes a group of constraints from the problem
definition.
\begin{itemize}
	\setcounter{enumi}{12}
	\item Makes sure that starting times are positive and that all jobs
		finish before $T$.
	\item Makes sure that job may not start before all their dependencies
		are finished by stating that they start strictly after their
		dependency.
	\item Makes sure that never two more jobs use the shared resource by
		stating that they either ends strictly before the other or
		start strictly after the other.
\end{itemize}

\subsection{SMT format solution}
The formula is easily convertable via a script to SMT format by literal
conversion and said script is listed in Listing~\ref{listing:a3.bash}. The
script optimizes a little bit from the original formula by leaving out the
shared resource checking for the same jobs. The minimization is done by
incrementing variable $T$ every time the current $T$ yields unsat with a bash
script shown in Listing~\ref{listing:3.bash}.

\lstinputlisting[language=bash,firstline=46,
	caption={Iteratively find the shortest solution for problem 3},
	label={listing:3.bash}]{src/a3.bash}

\subsection{Solution}
The bash script finds and shows the minimal solution in which all jobs are
finished in $37$ time units. Finding this solution takes less then $0.85$
seconds and is shown in Figure~\ref{fig:s3}. 

Light gray blocks represent normal tasks and the darker gray blocks represent
tasks from $J'$.

\begin{figure}[H]
	\centering
	\includegraphics[width=\linewidth]{s3.png}
\label{fig:s3}
	\caption{Solution visualization for problem 3}
\end{figure}
