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.
\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\\
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}
\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}
+\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}
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$
\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}
\usepackage{graphicx}
\usepackage{amsmath}
\usepackage{listings}
+\usepackage{nicefrac}
-\everymath{\displaystyle}
+\everymath{\displaystyle\allowdisplaybreaks}
\lstset{%
basicstyle=\scriptsize,
+++ /dev/null
-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)
-
+++ /dev/null
-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)
-
+++ /dev/null
-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)
-
--- /dev/null
+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
--- /dev/null
+python3 a2.py | yices-smt -m
--- /dev/null
+i=1
+while [ $(python3 a3.py $i | yices-smt) = "unsat" ]; do
+ i=$((i+1))
+done
+python3 a3.py $i | yices-smt -m
--- /dev/null
+#!/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("))")
--- /dev/null
+i=1
+while [ $(python3 a4.py $i | yices-smt) = "unsat" ]; do
+ i=$((i+1))
+done
+python3 a3.py $((i-1)) | yices-smt -m
repositories / master.git / commitdiff
