finished 1-3
authorMart Lubbers <mart@martlubbers.net>
Thu, 22 Oct 2015 19:31:25 +0000 (21:31 +0200)
committerMart Lubbers <mart@martlubbers.net>
Thu, 22 Oct 2015 19:31:25 +0000 (21:31 +0200)
18 files changed:
ar/assignments/1.tex
ar/assignments/2.tex
ar/assignments/3.tex
ar/assignments/4.tex
ar/assignments/a.tex
ar/assignments/preamble.tex
ar/assignments/s3.png [new file with mode: 0644]
ar/assignments/src/1.model [deleted file]
ar/assignments/src/2.model [deleted file]
ar/assignments/src/4.model [deleted file]
ar/assignments/src/a1.bash [new file with mode: 0644]
ar/assignments/src/a1.smt [moved from ar/assignments/src/1.smt with 100% similarity]
ar/assignments/src/a2.bash [new file with mode: 0644]
ar/assignments/src/a2.py [moved from ar/assignments/src/2.py with 100% similarity]
ar/assignments/src/a3.bash [new file with mode: 0644]
ar/assignments/src/a3.py [new file with mode: 0644]
ar/assignments/src/a4.bash [new file with mode: 0644]
ar/assignments/src/a4.py [moved from ar/assignments/src/4.py with 100% similarity]

index 317ae58..8506da9 100644 (file)
@@ -22,46 +22,48 @@ delivered, and show how for that number all pallets may be divided over the six
 trucks.
 }
 
+\newpage
 \subsection{Formal definition}
-For every truck $t_i$ for $i\in T$ where $T=[1\ldots6]$ in combination with
+For every truck $t_i$ for $i\in T$ where $T=\{1,\ldots,6\}$ in combination with
 every nuzzle $n$, prittle $p$, skipple $s$, crottle $c$ and dupple $d$ we
-declare a variable that holds the amount of that type of building block.
-We group all pallets $r$ for $r\in P$ where $P=[n,p,s,c,d]$. We also define
-function $w(r)$ that defines the weight of the pallet and $n(r)$ that defines
-the number of pallets needed. Then the following combination of subformulas
-describes the problem.
+declare a variable that holds the amount of that type of building block in that
+truck. We group all pallets $r\in P$ where $P=\{n,p,s,c,d\}$. We also
+define function $w(r)$ that defines the weight of the pallet and $n(r)$ that
+defines the number of pallets needed.
+
+This leads to the following formalization where we maximize $n(p)$.
 
 \begin{align}
        \bigwedge^{T}_{i=1}\Biggl(
-       & \bigwedge_{r\in P}t_ir\geq0\\
-       & \wedge \sum_{r\in P}t_ir\leq8\\
-       & \wedge \left(\sum_{r\in P}t_ir*w(r)\right)\leq7800)\\
-       & \wedge (t_ip=0\vee t_ic=0)\\
-       & \wedge t_id\leq1\\
-       & \wedge (t_i=t_1 \vee t_i=t_2 \vee t_is=0)\Biggr)\wedge\\
+       & \bigwedge_{r\in P}t_{i}r\geq0\\
+       & \wedge \sum_{r\in P}t_{i}r\leq8\\
+       & \wedge \left(\sum_{r\in P}t_{i}r\cdot w(r)\right)\leq7800)\\
+       & \wedge (t_{i}p=0\vee t_{i}c=0)\\
+       & \wedge t_{i}d\leq1\\
+       & \wedge (t_{i}=t_{1} \vee t_{i}=t_{2} \vee t_{i}s=0)\Biggr)\wedge\\
        \bigwedge_{r\in P}\Biggl(
-       & r=p\vee\left(\sum^{T}_{i=1}t_ir\right)=n(r)\Biggr)
+       & \left(\sum^{T}_{i=1}t_{i}r\right)=n(r)\Biggr)
 \end{align}
 
-All the subformulas describe a constraint from the problem description and we
-can separate two groups. Subformulas going over all trucks and subformulas over
-all pallets.
+Every numbered subformula describes a constraint from the problem description.
+We can separated the subformulas in formulas going over all trucks and formulas
+going over all pallets.
+
 \begin{itemize}
        \item \textbf{Trucks}
        \begin{enumerate}
-               \item Makes sure you can not have a negative number of pallets.
-                       by stating that all pallets numbers per truck are
-                       bigger then $0$.
+               \item Makes sure you can not have a negative number of pallets
+                       in a truck by stating that the number of pallets in a
+                       truck is not smaller then $0$.
                \item Makes sure you can not have more then $8$ pallets in a
                        truck by stating that the sum of all pallets in a truck
                        is not bigger then $8$.
-               \item Makes sure the weight will never go over the maximum by
-                       stating that all the pallets times their weight in a
-                       truck may not go over $7800$kg.
+               \item Makes sure the weight will never go over the maximum
+                       weight per truck by stating that all the pallets times
+                       their weight in a truck will not go over $7800$kg.
                \item Makes sure prittles and crottles are never together in a
                        truck by stating that either the number of prittles is
-                       zero or the number of crottles is zero. Note that they
-                       therefore also can both be zero.
+                       zero or the number of crottles is zero in a truck.
                \item Makes sure that skipples are only in the first two cooled
                        trucks by stating that if the truck number not one or
                        two the number of skipples is zero.
@@ -71,39 +73,31 @@ all pallets.
                \setcounter{enumi}{6}
                \item Makes sure that all mandatory pallets are transported by
                        summing over all trucks and assuring the number of the
-                       pallets of that type is exactly $n(r)$. Note that this
-                       should hold or that the current pallet is a prittle
-                       pallet since we do not have a limit on prittles.
+                       pallets of that type is exactly $n(r)$.
        \end{enumerate}
 \end{itemize}
 
 \subsection{SMT format solution}
 The formula is easily convertable to SMT format and is listed in
-Listing~\ref{listing:a1.smt}. A final condition is added with a special
-variable named \texttt{<REP>} that we increment to find the maximum amount of
-prittles transportable. When running the script in Listing~\ref{listing:1bash}
-the loop terminates after it echoed $20$ meaning that the maximum number of
-prittles is 20. This iterative solution takes less then $0.1$ seconds to
-calculate.
+Listing~\ref{listing:a1.smt}. The maximization is done by incrementing a
+special variable called \texttt{<REP>} which is an instantiation of $n(p)$.
+When the iteration yields unsat we know that the current number minus one is
+the maximum amount of prittles the trucks can carry. The maximization is done
+with a bash script shown in Listing~\ref{listing:1.bash}.
 
-\begin{lstlisting}[language=bash,
-       caption={Iteratively find the largest solution},label={listing:1bash}]
-i=1
-while [ $(sed "s/<REP>/$i/g" a1.smt | yices-smt) = "sat" ]
-do
-       echo $((++i));
-done
-\end{lstlisting}
+\lstinputlisting[language=bash,
+       caption={Iteratively find the largest solution for problem 1},
+       label={listing:1.bash}]{src/a1.bash}
 
 \subsection{Solution}
-The iterative solution terminates with $i=18$ so the maximum number of prittles
-to be deliverd is $18$. When we rerun the solution with $18$ prittles and the
-\texttt{-m} flag we can see the solution as in Table~\ref{tab:s1}.
+The bash script finds and shows the maximal solution of $18$ prittles. Finding
+this solution takes less then $0.12$ seconds and is shown in Table~\ref{tab:s1}.
 
 \begin{table}[H]
        \begin{tabular}{|l|lllll|l|l|}
                \hline
-               Truck & Nuzzles & Prittles & Skipples & Crottles & Dupples & Weight & Pallets\\
+               Truck & Nuzzles & Prittles & Skipples & Crottles & Dupples &
+                       Weight & Pallets\\
                \hline
                1 & 0 & 0 & 4 & 2 & 1 & 7100 & 7\\
                2 & 0 & 3 & 4 & 0 & 1 & 6500 & 8\\
@@ -115,6 +109,6 @@ to be deliverd is $18$. When we rerun the solution with $18$ prittles and the
                total & 4 & 18 & 8 & 10 & 5 & &\\
                \hline
        \end{tabular}
-       \caption{Solution table for problem 1}
-       \label{tab:s1}
+       \caption{Solution visualization for problem 1}
+\label{tab:s1}
 \end{table}
index f4789d8..7fd4047 100644 (file)
@@ -6,97 +6,116 @@ components satisfying the following constraints:
 \begin{itemize}
        \item The width of the chip is 29 and the height is 22.
        \item All power components have width 4 and height 2.
-       \item The sizes of the eight regular components are $9\times7$, $12\times6,$
-               $10\times7,$ $18\times5,$ $20\times4,$ $10\times6,$ $8\times6$ and
-               $10\times8$ respectively.
+       \item The sizes of the eight regular components are $9\times7$,
+               $12\times6,$ $10\times7,$ $18\times5,$ $20\times4,$
+               $10\times6,$ $8\times6$ and $10\times8$ respectively.
        \item All components may be turned 90, but may not overlap.
        \item In order to get power, all regular components should directly be
-               connected to a power component, that is, an edge of the component should
-               have at least one point in common with an edge of the power component.
-       \item Due to limits on heat production the power components should be not too
-               close: their centres should differ at least $17$ in either the $x$
-               direction or the $y$ direction (or both).
+               connected to a power component, that is, an edge of the
+               component should have at least one point in common with an edge
+               of the power component.
+       \item Due to limits on heat production the power components should be
+               not too close: their centres should differ at least $17$ in
+               either the $x$ direction or the $y$ direction (or both).
 \end{itemize}
 }
 
+\newpage
 \subsection{Formal definition}
-For every component $c$ for $i\in PC\cup RC$ where $PC=[01,02,03]$ and
-$RC=[04,05,06,07,08,09,10,11]$ we define a width, a height variable, an x and a
-y variable. $c_iw$, $c_ih$, $c_ix$ and $c_iy$. Although we call the height and
-width they represent just the sides since the components can be rotated. To
-represent this we introduce functions $h(c)$ and $w(c)$ that return the
-specified width and height.
+For every component $c_{i}$ for $i\in PC\cup RC$ where $PC=\{1,\ldots,3\}$ and
+$RC=\{4,\ldots,11\}$ we define a width, a height, an $x$ and a $y$ variables
+$c_{i}w$, $c_{i}h$, $c_{i}x$ and $c_{i}y$. $c_ih$ does not necessarily have the
+specified height of the components since the components may be rotated. For the
+specified width and height we introduce the functions $h(c)$ and $w(c)$ that
+return the specified width and height.
+
+This leads to the following formalization.
 
 \begin{align}
        \bigwedge_{i\in PC\cup RC}\Biggl(
-         & (c_ih=h(i)\vee c_ih=w(i))\wedge(c_iw=w(i)\vee c_iw=h(i))\\
-               & \wedge 29-c_iw\geq c_ix>0\wedge 22-c_ih\geq c_iy>0\\
-               & \wedge \bigwedge_{j\in PC\cup RC}\Bigl(\\
-               \nonumber & \qquad\qquad\qquad j\geq i\\
-               \nonumber & \qquad\qquad\qquad \vee c_ix>c_jx+c_jw\\
-               \nonumber & \qquad\qquad\qquad \vee c_ix+c_jw<c_jx\\
-               \nonumber & \qquad\qquad\qquad \vee c_iy>c_jy+c_jh\\
-               \nonumber & \qquad\qquad\qquad \vee c_iy+c_jh<c_jh\Bigr)\Biggr)\wedge\\
+         & (c_{i}h=h(i)\vee c_{i}h=w(i))\wedge(c_{i}w=w(i)\vee c_{i}w=h(i))\\
+               & \wedge 29-c_{i}w\geq c_{i}x>0\wedge 22-c_{i}h\geq c_{i}y>0\\
+               & \wedge \bigwedge_{j\in PC\cup RC}\Bigl(j\geq i\\
+               \nonumber & \qquad\qquad\qquad \vee c_{i}x>c_{j}x+c_{j}w\\
+               \nonumber & \qquad\qquad\qquad \vee c_{i}x+c_{j}w<c_{j}x\\
+               \nonumber & \qquad\qquad\qquad \vee c_{i}y>c_{j}y+c_{j}h\\
+               \nonumber & \qquad\qquad\qquad 
+                       \vee c_{i}y+c_{j}h<c_{j}h\Bigr)\Biggr)\wedge\\
        \bigwedge_{i\in PC}\bigwedge_{j\in PC}\Biggl( & i=j\\
-               \nonumber & \vee c_ix+\frac{c_iw}{2}-c_jx+\frac{c_jw}{2}>17\\
-               \nonumber & \vee c_jx+\frac{c_jw}{2}-c_ix+\frac{c_iw}{2}>17\\
-               \nonumber & \vee c_iy+\frac{c_ih}{2}-c_jy+\frac{c_jh}{2}>17\\
-               \nonumber & \vee c_jy+\frac{c_jh}{2}-c_iy+\frac{c_ih}{2}>17\Biggr)\wedge\\
+               \nonumber & \vee c_{i}x+\nicefrac{c_{i}w}{2}-
+                       c_{j}x+\nicefrac{c_{j}w}{2}>17\\
+               \nonumber & \vee c_{j}x+\nicefrac{c_{j}w}{2}-
+                       c_{i}x+\nicefrac{c_{i}w}{2}>17\\
+               \nonumber & \vee c_{i}y+\nicefrac{c_{i}h}{2}-
+                       c_{j}y+\nicefrac{c_{j}h}{2}>17\\
+               \nonumber & \vee c_{j}y+\nicefrac{c_{j}h}{2}-
+                       c_{i}y+\nicefrac{c_{i}h}{2}>17\Biggr)\wedge\\
        \bigwedge_{i\in RC}\bigvee_{j\in PC}\neg\Biggl(
-               & (c_ix-1>c_jx+c_jw\\
-               \nonumber & \vee c_ix+1+c_jw<c_jx\\
-               \nonumber & \vee c_iy-1>c_jy+c_jh\\
-               \nonumber & \vee c_iy+1+c_jh<c_jh\Biggr)
+               & (c_{i}x-1>c_{j}x+c_{j}w\\
+               \nonumber & \vee c_{i}x+1+c_{j}w<c_{j}x\\
+               \nonumber & \vee c_{i}y-1>c_{j}y+c_{j}h\\
+               \nonumber & \vee c_{i}y+1+c_{j}h<c_{j}h\Biggr)
 \end{align}
 
-All subformulas describe a constraint from the problem description and can be
-separated in three groups. Subformulas going over all components, only power
-components and only regular components.
+Every numbered subformula describes a constraint from the problem description.
+We can separated the subformulas in formulas going over all components, only
+power components and only regular components.
 \begin{itemize}
        \item\textbf{All}
                \begin{enumerate}
-                               \setcounter{enumi}{7}
-                       \item Describes that the width and the height of the component can be
-                               swapped(in case of rotation).
-                       \item Constrains location of the components in regard to the size of
-                               the chip.
-                       \item Makes sure the components do not overlap by defining for all
-                               pairs of components that they either are strictly right, strictly
-                               left, strictly above or strictly below the other.
+                       \setcounter{enumi}{7}
+                       \item Makes sure the width and the height of the
+                               component can be swapped thus allowing a
+                               rotation.
+                       \item Makes sure the components are placed on the
+                               chip by stating that the $x$ and $y$
+                               coordinates are bigger then $0$ and the $x$ and
+                               $y$ plus their width or height does not exceed
+                               the specified width and height of the chip.
+                       \item Makes sure the components do not overlap by
+                               defining for all pairs of components that they
+                               either are strictly right, strictly left,
+                               strictly above or strictly below the other.
                \end{enumerate}
        \item\textbf{Power only}
                \begin{enumerate}
-                               \setcounter{enumi}{10}
-                               \item Power components must be at least $17$ block away from
-                                       other power components. This is defined by saying that the
-                                       difference between the center of each pair of components is
-                                       bigger then $17$.
+                       \setcounter{enumi}{10}
+                       \item Makes sure power components are at least $17$
+                               block away from other power components by
+                               stating that the difference between the center
+                               of each pair of components is bigger then $17$.
                \end{enumerate}
        \item\textbf{Regular only}
                \begin{enumerate}
-                               \setcounter{enumi}{11}
-                               \item Regular components must be connected to a power
-                                               components. This is described using the method from the
-                                               overalap calculation in a negated way. Every regular
-                                               component must have overlap with a power component that
-                                               has been enlarged by $1$.
+                       \setcounter{enumi}{11}
+                       \item Makes sure regular components are connected to a
+                               power component by stating, using the same
+                               method as in the overlay, that it has overlap
+                               with a power component that has had its size
+                               increased by $1$.
                \end{enumerate}
 \end{itemize}
 
 \subsection{SMT format solution}
 The formula is easily convertable via a Python script to SMT format and said
-script is listed in Listing~\ref{listing:2.py}. The Python script optimizes a
+script is listed in Listing~\ref{listing:a2.py}. The Python script optimizes a
 little bit from the original formula by leaving out the overlap checking
-between the same components. When we run the file a solution is found within
-$30$ seconds.
+between the same components. The solution is calculated using the command shown
+in Listing~\ref{listing:2.bash}
+
+\lstinputlisting[language=bash,
+       caption={Find the shortest solution for problem 3},
+       label={listing:2.bash}]{src/a2.bash}
 
 \subsection{Solution}
-Figure~\ref{fig:s2} shows the configuration found by the solver. Light gray
-components are regular components and darker gray components are power
-components.
+Finding this solution takes less then $35$ seconds and is shown in
+Figure~\ref{fig:s2}.
+
+Light gray blocks represent regular components and the darker gray
+blocks represent power components.
 
 \begin{figure}[H]
-       \includegraphics[scale=0.75]{s2.png}
-       \label{fig:s2}
+       \includegraphics[scale=0.70]{s2.png}
+\label{fig:s2}
        \caption{Solution visualization for problem 2}
 \end{figure}
index e69de29..471f3e1 100644 (file)
@@ -0,0 +1,76 @@
+\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 Python script to SMT format and said
+script is listed in Listing~\ref{listing:a3.py}. The Python 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,
+       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]
+       \includegraphics[width=\linewidth]{s3.png}
+\label{fig:s3}
+       \caption{Solution visualization for problem 3}
+\end{figure}
index dd52191..6a827cb 100644 (file)
@@ -9,6 +9,7 @@ a number of steps a number $\ge 50$ occurs at least twice in $a_1; a_2; a_3;
 a_4; a_5; a_6; a_7$.
 }
 
+\newpage
 \subsection{Formal definition}
 \paragraph{Precondition}
 Say we have $I$ $a$'s denoted as $a_i$ and we have $N$ iterations. $i_na_i$
index 8ac130a..e0ac8a3 100644 (file)
@@ -6,10 +6,17 @@ RAM: 8GB
 \end{lstlisting}
 
 \newpage
-\lstinputlisting[language=lisp,caption={a1.smt},label={listing:a1.smt}]{src/1.smt}
+\lstinputlisting[language=lisp,caption={a1.smt},
+       label={listing:a1.smt}]{src/a1.smt}
 
 \newpage
-\lstinputlisting[language=python,caption={a2.py},label={listing:2.py}]{src/2.py}
+\lstinputlisting[language=python,caption={a2.py},
+       label={listing:a2.py}]{src/a2.py}
 
 \newpage
-\lstinputlisting[language=python,caption={a4.py},label={listing:4.py}]{src/4.py}
+\lstinputlisting[language=python,caption={a3.py},
+       label={listing:a3.py}]{src/a3.py}
+
+\newpage
+\lstinputlisting[language=python,caption={a4.py},
+       label={listing:a4.py}]{src/a4.py}
index 93b06ec..a401ca6 100644 (file)
@@ -7,8 +7,9 @@
 \usepackage{graphicx}
 \usepackage{amsmath}
 \usepackage{listings}
+\usepackage{nicefrac}
 
-\everymath{\displaystyle}
+\everymath{\displaystyle\allowdisplaybreaks}
 
 \lstset{%
   basicstyle=\scriptsize,
diff --git a/ar/assignments/s3.png b/ar/assignments/s3.png
new file mode 100644 (file)
index 0000000..46e9e75
Binary files /dev/null and b/ar/assignments/s3.png differ
diff --git a/ar/assignments/src/1.model b/ar/assignments/src/1.model
deleted file mode 100644 (file)
index cf9ab8f..0000000
+++ /dev/null
@@ -1,33 +0,0 @@
-sat
-
-(= t5n 0)
-(= t1p 0)
-(= t1c 2)
-(= t3c 0)
-(= t2p 3)
-(= t1d 1)
-(= t4c 0)
-(= t4d 1)
-(= t5c 5)
-(= t3s 0)
-(= t3d 0)
-(= t5p 0)
-(= t2s 4)
-(= t5s 0)
-(= t6d 1)
-(= t1s 4)
-(= t6n 4)
-(= t2d 1)
-(= t3n 0)
-(= t4p 7)
-(= t6s 0)
-(= t4s 0)
-(= t4n 0)
-(= t1n 0)
-(= t6c 3)
-(= t5d 1)
-(= t2n 0)
-(= t2c 0)
-(= t6p 0)
-(= t3p 8)
-
diff --git a/ar/assignments/src/2.model b/ar/assignments/src/2.model
deleted file mode 100644 (file)
index b334a86..0000000
+++ /dev/null
@@ -1,47 +0,0 @@
-sat
-
-(= c06y 16)
-(= c10h 5)
-(= c01h 3)
-(= c11w 7)
-(= c11h 9)
-(= c02y 2)
-(= c02x 9)
-(= c05w 11)
-(= c04x 21)
-(= c06x 11)
-(= c09x 1)
-(= c06w 9)
-(= c09h 9)
-(= c03y 21)
-(= c03h 1)
-(= c05y 6)
-(= c08x 8)
-(= c07x 11)
-(= c07y 1)
-(= c10y 6)
-(= c09y 11)
-(= c09w 5)
-(= c01x 28)
-(= c04y 16)
-(= c05h 5)
-(= c06h 6)
-(= c04w 8)
-(= c10x 21)
-(= c02h 3)
-(= c08y 12)
-(= c08w 19)
-(= c11y 1)
-(= c01w 1)
-(= c07w 17)
-(= c07h 4)
-(= c10w 7)
-(= c04h 6)
-(= c08h 3)
-(= c05x 9)
-(= c01y 12)
-(= c11x 1)
-(= c02w 1)
-(= c03x 7)
-(= c03w 3)
-
diff --git a/ar/assignments/src/4.model b/ar/assignments/src/4.model
deleted file mode 100644 (file)
index ffccc8a..0000000
+++ /dev/null
@@ -1,71 +0,0 @@
-sat
-
-(= i3a3 3)
-(= i6a3 3)
-(= i8a5 47)
-(= i0a3 3)
-(= i6a6 30)
-(= c6 6)
-(= i0a5 5)
-(= i8a3 3)
-(= i0a4 4)
-(= i2a6 6)
-(= i8a4 50)
-(= i1a6 6)
-(= i10a6 54)
-(= i7a2 4)
-(= i3a2 4)
-(= i10a5 47)
-(= i5a2 4)
-(= i3a4 8)
-(= i8a2 4)
-(= i7a5 47)
-(= i5a5 23)
-(= c8 4)
-(= i1a3 3)
-(= i1a5 5)
-(= i10a2 4)
-(= i2a5 5)
-(= i4a4 17)
-(= i3a6 6)
-(= c3 5)
-(= c5 5)
-(= i5a3 3)
-(= i9a4 50)
-(= i5a4 17)
-(= i9a6 30)
-(= i9a2 4)
-(= a1 1)
-(= c1 2)
-(= c7 5)
-(= c2 4)
-(= i9a3 54)
-(= i10a3 54)
-(= i3a5 14)
-(= i7a3 3)
-(= c10 6)
-(= i2a2 4)
-(= i5a6 6)
-(= c0 0)
-(= c9 3)
-(= i4a5 14)
-(= i4a6 6)
-(= i7a4 17)
-(= i6a5 23)
-(= i10a4 50)
-(= i0a2 2)
-(= i4a2 4)
-(= i4a3 3)
-(= i6a2 4)
-(= i2a3 3)
-(= i7a6 30)
-(= c4 4)
-(= i2a4 8)
-(= a7 7)
-(= i6a4 17)
-(= i8a6 30)
-(= i9a5 47)
-(= i0a6 6)
-(= i1a2 4)
-(= i1a4 4)
-
diff --git a/ar/assignments/src/a1.bash b/ar/assignments/src/a1.bash
new file mode 100644 (file)
index 0000000..847616c
--- /dev/null
@@ -0,0 +1,5 @@
+i=1
+while [ $(sed "s/<REP>/$i/g" a1.smt | yices-smt) = "sat" ]; do
+       i=$((i+1))
+done
+sed "s/<REP>/$((i-1))/g" a1.smt | yices-smt -m
diff --git a/ar/assignments/src/a2.bash b/ar/assignments/src/a2.bash
new file mode 100644 (file)
index 0000000..5462573
--- /dev/null
@@ -0,0 +1 @@
+python3 a2.py | yices-smt -m
diff --git a/ar/assignments/src/a3.bash b/ar/assignments/src/a3.bash
new file mode 100644 (file)
index 0000000..115f1fd
--- /dev/null
@@ -0,0 +1,5 @@
+i=1
+while [ $(python3 a3.py $i | yices-smt) = "unsat" ]; do
+       i=$((i+1))
+done
+python3 a3.py $i | yices-smt -m
diff --git a/ar/assignments/src/a3.py b/ar/assignments/src/a3.py
new file mode 100644 (file)
index 0000000..a295c8d
--- /dev/null
@@ -0,0 +1,47 @@
+#!/usr/bin/env python3
+import sys
+
+if len(sys.argv) != 2:
+    print("usage: {} maxjobstart".format(sys.argv[0]))
+    exit()
+
+maxjobstart = sys.argv[1]
+jobs = 12
+J = range(1, jobs+1)
+Jprime = {5, 7, 10}
+pi = {
+    3: {1,2},
+    5: {3,4},
+    7: {3,4,6},
+    9: {5,8},
+    11: {10},
+    12: {9,11}
+}
+
+# Print preamble
+print("(benchmark a4.smt")
+print(":logic QF_UFLIA")
+
+# Print variables
+print(":extrafuns (")
+for i in J:
+    print("(j{} Int)".format(i), end=' ')
+print("\n)")
+
+print(":formula")
+print("(and")
+for i in J:
+    # Make sure the times are positive and within the bound
+    print("(> j{0} 0) (<= (+ j{0} {0}) {1})".format(i, maxjobstart))
+    # Make sure the dependencies are done when a task is scheduled
+    for k in pi.get(i, {}):
+        print("(>= j{0} (+ j{1} {1}))".format(i, k))
+# Make sure the shared resources are not used by two tasks at once
+for i in Jprime:
+    for k in Jprime:
+        if i != k:
+            print("(or (>= j{0} (+ j{1} {1}))".format(i,k), end=' ')
+            print("(<= (+ j{0} {0}) j{1}))".format(i,k))
+
+# Close the and,benchmark parenthesis
+print("))")
diff --git a/ar/assignments/src/a4.bash b/ar/assignments/src/a4.bash
new file mode 100644 (file)
index 0000000..7a5211d
--- /dev/null
@@ -0,0 +1,5 @@
+i=1
+while [ $(python3 a4.py $i | yices-smt) = "unsat" ]; do
+       i=$((i+1))
+done
+python3 a3.py $((i-1)) | yices-smt -m