path: root/part1.tex

\documentclass[12pt]{article}
\usepackage{a4wide}
\usepackage{latexsym}
\usepackage{amssymb}
\usepackage{epic}
\usepackage{graphicx}
\usepackage{gensymb}
\usepackage{listings}
\usepackage{tikz}
%\pagestyle{empty}
\newcommand{\tr}{\mbox{\sf true}}
\newcommand{\fa}{\mbox{\sf false}}
\newcommand{\bimp}{\leftrightarrow}     % bi-implication

\title{Assignment part 1 for Automated Reasoning 2IMF25}
\author{Koen van der Heijden (0807929), Peter Wu (0783206)}
\date{\today}

\begin{document}
\maketitle

\section*{Problem: Packing pallets in trucks}

Eight trucks have to deliver pallets of obscure building blocks to a magic factory. Every
truck has a capacity of 8000 kg and can carry at most eight pallets. In total, the
following has to be delivered:

\begin{itemize}
\item Four pallets of nuzzles, each of weight 700 kg.
\item A number of pallets of prittles, each of weight 400 kg.
\item Eight pallets of skipples, each of weight 1000 kg.
\item Ten pallets of crottles, each of weight 2500 kg.
\item Twenty pallets of dupples, each of weight 200 kg.
\end{itemize}

Skipples need to be cooled; only three of the eight trucks have facility for cooling
skipples.

Nuzzles are very valuable: to distribute the risk of loss no two pallets of nuzzles may
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:

\begin{itemize}
\item Both the width and the height of the chip is 30.
\item The power components have width 4 and height 3.
\item The sizes of the ten regular components are $4 \times 5$, $4 \times 6$,
    $5 \times 20$, $6 \times 9$, $6 \times 10$, $6 \times 11$, $7 \times 8$,
    $7 \times 12$, $10 \times 10$, $10 \times 20$, respectively.
\item All components may be turned $90\degree$, 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).
\end{itemize}

\subsection*{Solution:}

\begin{tikzpicture}[scale=0.5]
%\draw[step=1,gray,very thin] (0, 0) grid (30, 30);
\draw[red,thick] (-.5, -.5) rectangle (30.5, 30.5);

\draw[draw=red,fill=red] (27.01, 20.01) rectangle (29.99, 23.99);
\node[align=center] at (28.500000,22.000000) {0\\(27,20)\\(3 x 4)};
\draw[draw=green,fill=red] (7.01, 11.01) rectangle (9.99, 14.99);
\node[align=center] at (8.500000,13.000000) {1\\(7,11)\\(3 x 4)};
\draw[draw=blue] (10.01, 11.01) rectangle (14.99, 14.99);
\node[align=center] at (12.500000,13.000000) {2\\(10,11)\\(5 x 4)};
\draw[draw=cyan] (21.01, 21.01) rectangle (26.99, 24.99);
\node[align=center] at (24.000000,23.000000) {3\\(21,21)\\(6 x 4)};
\draw[draw=magenta] (10.01, 25.01) rectangle (29.99, 29.99);
\node[align=center] at (20.000000,27.500000) {4\\(10,25)\\(20 x 5)};
\draw[draw=gray] (7.01, 15.01) rectangle (12.99, 23.99);
\node[align=center] at (10.000000,19.500000) {5\\(7,15)\\(6 x 9)};
\draw[draw=darkgray] (0.01, 24.01) rectangle (9.99, 29.99);
\node[align=center] at (5.000000,27.000000) {6\\(0,24)\\(10 x 6)};
\draw[draw=lightgray] (12.01, 0.01) rectangle (17.99, 10.99);
\node[align=center] at (15.000000,5.500000) {7\\(12,0)\\(6 x 11)};
\draw[draw=brown] (13.01, 15.01) rectangle (19.99, 22.99);
\node[align=center] at (16.500000,19.000000) {8\\(13,15)\\(7 x 8)};
\draw[draw=olive] (0.01, 11.01) rectangle (6.99, 22.99);
\node[align=center] at (3.500000,17.000000) {9\\(0,11)\\(7 x 12)};
\draw[draw=orange] (2.01, 1.01) rectangle (11.99, 10.99);
\node[align=center] at (7.000000,6.000000) {10\\(2,1)\\(10 x 10)};
\draw[draw=pink] (20.01, 0.01) rectangle (29.99, 19.99);
\node[align=center] at (25.000000,10.000000) {11\\(20,0)\\(10 x 20)};
\end{tikzpicture}

\section*{Problem: Job scheduling}
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 + 5$, for $i = 1, 2, \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 8 may not start earlier than job 5.
\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}

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

% (b) Do the same with the extra requirement that job 6 and job 12 need a resource of
% limited availability, by which job 6 may only run during the 17 time units in which
% 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$
are given, for which the initial value of
$a_i$ is $i$ for $i = 1$, \ldots, 8. The following steps are defined: choose $i$
with $1 < i < 8$ and execute
\[
    a_i := a_{i-1} + a_i+1,
\]
that is, $a_i$ gets the sum of the values of its neighbors and all other values remain
unchanged.

% (a) Show how it is possible that $a_3 = a_7$ after a number of steps.

% (b) Show how it is possible that $a_3 = a_5 = a_7$ after a number of steps.
% For this problem both try to use an SMT solver and NuSMV, and discuss how they perform.

\subsection*{Solution:}

\end{document}