summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorKoen van der Heijden <koen.vd.heijden1@gmail.com>2016-12-12 00:46:59 +0100
committerKoen van der Heijden <koen.vd.heijden1@gmail.com>2016-12-12 00:46:59 +0100
commit467e4af49ecfaa280f88f3da10f64b25e038d866 (patch)
tree961b428e7e66a2cd2868415652fe6ac491f57bdc
parentb96e78d0bc84b07c6c727f9f1e4a8a14dcaf706e (diff)
download2IMF25-AR-467e4af49ecfaa280f88f3da10f64b25e038d866.tar.gz
tex file edit
-rw-r--r--integer_sum_from_neighbours/NeighbourSum.java7
-rw-r--r--integer_sum_from_neighbours/integer_sum_from_neighbours.z30
-rw-r--r--part1.tex39
3 files changed, 46 insertions, 0 deletions
diff --git a/integer_sum_from_neighbours/NeighbourSum.java b/integer_sum_from_neighbours/NeighbourSum.java
new file mode 100644
index 0000000..364a3dd
--- /dev/null
+++ b/integer_sum_from_neighbours/NeighbourSum.java
@@ -0,0 +1,7 @@
+package PACKAGE_NAME;
+
+/**
+ * Created by koen on 12/11/16.
+ */
+public class NeighbourSum {
+}
diff --git a/integer_sum_from_neighbours/integer_sum_from_neighbours.z3 b/integer_sum_from_neighbours/integer_sum_from_neighbours.z3
deleted file mode 100644
index e69de29..0000000
--- a/integer_sum_from_neighbours/integer_sum_from_neighbours.z3
+++ /dev/null
diff --git a/part1.tex b/part1.tex
index 5b2fc45..73e8b6b 100644
--- a/part1.tex
+++ b/part1.tex
@@ -5,6 +5,7 @@
\usepackage{epic}
\usepackage{graphicx}
\usepackage{gensymb}
+\usepackage{Listings}
%\pagestyle{empty}
\newcommand{\tr}{\mbox{\sf true}}
\newcommand{\fa}{\mbox{\sf false}}
@@ -39,11 +40,17 @@ be in the same truck.
% (a) Investigate what is the maximum number of pallets of prittles that can be delivered,
% and show how for that number all pallets may be divided over the eight trucks.
+% and show how for that number all pallets may be divided over the eight trucks.
% (b) Do the same, with the extra information that prittles and crottles are an explosive
% combination: they are not allowed to be put in the same truck.
\subsection*{Solution:}
+\begin{itemize}
+ \item[(a)]
+ \item[(b)]
+\end{itemize}
+
\section*{Problem: Chip design}
Give a chip design containing two power components and ten regular components satisfying the following constraints:
@@ -89,6 +96,38 @@ no two of these jobs may run at the same time.
% job 12 is running.
\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 \"unsat\".
+We also reformed all previously mentioned requirements into formula's that can be used in z3:
+
+\begin{lstlisting}
+(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}
+
+\subsubsection*{(b)}
+This solution was retrieved in the same way as answer a. This answer is $m = 65$.
+2 extra lines were added to ensure that job 6 lies withing job 12:
+
+\begin{lstlisting}
+(>= j6 j12)
+(<= (+ j6 11) (+ j12 17))
+\end{lstlisting}
\section*{Problem: Integer sum from neighbors}
Eight integer variables $a_1$, $a_2$, $a_3$, $a_4$, $a_5$, $a_6$, $a_7$, $a_8$