From 467e4af49ecfaa280f88f3da10f64b25e038d866 Mon Sep 17 00:00:00 2001
From: Koen van der Heijden <koen.vd.heijden1@gmail.com>
Date: Mon, 12 Dec 2016 00:46:59 +0100
Subject: tex file edit

---
 integer_sum_from_neighbours/NeighbourSum.java      |  7 ++++
 .../integer_sum_from_neighbours.z3                 |  0
 part1.tex                                          | 39 ++++++++++++++++++++++
 3 files changed, 46 insertions(+)
 create mode 100644 integer_sum_from_neighbours/NeighbourSum.java
 delete mode 100644 integer_sum_from_neighbours/integer_sum_from_neighbours.z3

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
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$
-- 
cgit v1.2.1