\documentclass[12pt]{article}
\usepackage{a4wide}
\usepackage{latexsym}
\usepackage{amssymb}
\usepackage{epic}
\usepackage{graphicx}
\usepackage{gensymb}
\usepackage{listings}
\usepackage{tikz}
\usepackage{amsmath}
\usepackage{hyperref}
\usepackage{float}
%\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:}
\subsubsection*{(a)}

\subsubsection*{(b)}


\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:}
We generalize this problem to fitting $n \geq 1$ components on a chip with
dimensions $w_c \times h_c$. Of these components, the first $1 \leq m < n$
components are considered power components.
For all components with index $0 \leq i < n$, a corner (the bottom-left one
in a Cartesian space) is represented by $(x_i, y_i)$ and the dimensions are $w_i
\times h_i$. (Observe that $(x_i + w_i, y_i + h_i)$ represents the opposite
corner, for brevity we will write this as $(x'_i, y'_i)$.)

To limit each component $i$ to the chip area:
\begin{align}
\label{eq:chip1}
    \bigwedge_{i=0}^{n-1}
    x_i \geq 0 \land y_i \geq 0 \land
        x'_i \leq c_w \land y'_i \leq c_h
\end{align}

Each component has a given width $w'_i$ and height $h'_i$. To handle rotated
components, we also allow these values to be swapped:
\begin{align}
\label{eq:chip2}
    &\bigwedge_{i=0}^{n-1}
    (w_i = w'_i \land h_i = h'_i) \lor (w_i = h'_i \land h_i = w'_i) \\
    &= ((w_0 = 4 \land h_0 = 3) \lor
       (w_0 = 3 \land h_0 = 4)) \nonumber \\
    &\land ((w_1 = 4 \land h_1 = 3) \lor
       (w_1 = 3 \land h_1 = 4)) \nonumber \\
    &\land ((w_2 = 4 \land h_2 = 5) \lor
       (w_2 = 5 \land h_2 = 4)) \nonumber \\
    &\land \cdots \nonumber
\end{align}

To avoid an overlap between any pair of components $i$ and $j$ (with $i < j$),
we add the restriction that each other component $j$ must be located either
below, to the left, above or to the right of a component $i$. (Note the use of
$i < j$ is sufficient, $i \neq j$ would also have been correct, but due to
symmetry of the overlap check it would contain redundant parts.)
\begin{align}
\label{eq:chip3}
\bigwedge_{0 \leq i < n}
\bigwedge_{i < j < n}
y'_j \leq y_i \lor
x'_j \leq x_i \lor
y_j \geq y'_i \lor
x_j \geq x'_i
\end{align}

To ensure that a point on the edge of a power component matches with any of the
four sides of a regular component, they must have the same $x$ coordinates (for
the left and right sides) or the same $y$ coordinates (for the bottom and top
side).  Besides having a shared axis, there must actual be an overlap with the
$y$ or $x$ coordinates, respectively.

Let $0 \leq i < m$ be the power component and $m \leq j < n$ be the regular
component. Then each regular component $i$ must have a match with some power
component $j$ (for clarity one part of the formula is split off):
\begin{align}
\label{eq:chip4}
\bigwedge_{0 \leq i < m}
\bigvee_{m \leq j < n}
    (
        (y'_j = y_i \lor y_j = y'_i)
        \land hasOverlap_x(i, j)
    ) \lor \nonumber \\ (
        (x'_j = x_i \lor x_j = x'_i)
        \land hasOverlap_y(i, j)
    )
\end{align}

Now we define $hasOverlap_{axis}(i, j)$ which must detect the cases shown in
Figure~\ref{fig:overlapCases} (for regular component $i$ and power component
$j$).

\begin{figure}[H]
\centering
\begin{tikzpicture}
\draw[fill=red,red] (1,0) rectangle (3,.5);
\draw (1,0) -- (1,.6);
\draw (3,0) -- (3,.6);

\node at (-.5,1) {\small{1}};
\draw[dotted] (0,1) -- (.5,1);
\draw[fill=white] (0,1) circle (0.1);
\draw[fill=white] (.5,1) circle (0.1);

\draw[dotted] (4,1) -- (4.5,1);
\draw[fill=white] (4,1) circle (0.1);
\draw[fill=white] (4.5,1) circle (0.1);

\node at (-.5,1.5) {\small{2}};
\draw[dotted] (0,1.5) -- (1,1.5);
\draw (1,1.5) -- (2,1.5);
\draw[fill=white] (0,1.5) circle (0.1);
\draw[fill=black] (2,1.5) circle (0.1);

\node at (-.5,2) {\small{3}};
\draw (1.5,2) -- (2.5,2);
\draw[fill=black] (1.5,2) circle (0.1);
\draw[fill=black] (2.5,2) circle (0.1);

\node at (-.5,2.5) {\small{4}};
\draw (2,2.5) -- (3,2.5);
\draw[dotted] (3,2.5) -- (4,2.5);
\draw[fill=black] (2,2.5) circle (0.1);
\draw[fill=white] (4,2.5) circle (0.1);

\node at (-.5,3) {\small{5}};
\draw[dotted] (.5,3) -- (1,3);
\draw (1,3) -- (3,3);
\draw[dotted] (3,3) -- (3.5,3);
\draw[fill=white] (.5,3) circle (0.1);
\draw[fill=white] (3.5,3) circle (0.1);
\end{tikzpicture}
\caption{\label{fig:overlapCases}
Cases that are considered for overlap. The solid lines can be considered
matching while the dotted part are not. The red rectangle on the bottom can be
considered the power component while the lines on above represent the sides of
regular components.}
\end{figure}

We are interested in the assignments that result in an overlap (that is,
the cases having solid lines in the figure) and do a case distinction based on
Figure~\ref{fig:overlapCases} for $axis=x$ (the same analysis applies to
$axis=y$):
\begin{enumerate}
\item No overlap, the ends of the rectangle are not within any of the two lines.
\item Overlap, the left end of the rectangle is within the ends of the line:
    $x_i \leq x_j \land x_j \leq x'_i$.
\item Overlap, both ends of the line are within the rectangle. To account for
    this, it is sufficient to check just one end though. For the begin of the
    line: $x_j \leq x_i \land x_i \leq x'_j$.
\item Overlap, the right end of the rectangle is within the ends of the line:
    $x_i \leq x'_j \land x'_j \leq x'_i$.
\item Overlap, both the left and right ends of the rectangle are within the
    begin and end of the line. Either check from (2) or (4) can be used here.
\end{enumerate}

(Note that in our case, the third check will never be satisfied since no side of
a regular component is smaller than the smallest side power components and can
therefore be removed. To generalize the following definition of $hasOverlap$,
one should add this third condition to the conjunction though.)

With the above analysis, we can define:
\begin{align*}
hasOverlap_x(i, j) &=
(x_i \leq x_j  \land x_j  \leq x'_i) \lor
(x_i \leq x'_j \land x'_j \leq x'_i) \\
hasOverlap_y(i, j) &=
(y_i \leq y_j  \land y_j  \leq y'_i) \lor
(y_i \leq y'_j \land y'_j \leq y'_i)
\end{align*}

Finally we must add a clause that ensures a difference of at least
$powerDistance$ between the centers of any pair of power components $i$, $j$
(with $i < j$). (Note that this is a horizontal or vertical difference, not
the Euclidean one.) Let the center for a power component $i$ be defined by:
\begin{align*}
cx_i &= x_i + \frac{1}{2}w_i &
cy_i &= y_i + \frac{1}{2}h_i
\end{align*}
then we have to check pairs that we have not seen yet:
\begin{align}
\label{eq:chip5}
\bigwedge_{0 \leq i < m}
\bigwedge_{i < j < m}
cx_i \geq& cx_j + powerDistance \lor
cx_j \geq cx_i + powerDistance \lor \\
cy_i \geq& cy_j + powerDistance \lor
cy_j \geq cy_i + powerDistance
\end{align}

We wrote a generator program that takes the conjunction of the above parts
(formulae \ref{eq:chip1}, \ref{eq:chip2}, \ref{eq:chip3}, \ref{eq:chip4},
\ref{eq:chip5}). Its annotated (partial) output is shown in
Listing~\ref{lst:chipDesign}. Evaluation of this output using
\texttt{python generate-chipdesign.py | z3 -smt -in} finished in 12 seconds.
The result is visualized in Figure~\ref{fig:chipDesign}.
Indeed, the requirements are satisfied.

\begin{lstlisting}[caption={Generated SMT output for
ChipDesign},label={lst:chipDesign},language=lisp,basicstyle=\scriptsize]
(benchmark test.smt
:logic QF_UFLIA
:extrafuns ((x0 Int) (y0 Int) (w0 Int) (h0 Int) ...
(x11 Int) (y11 Int) (w11 Int) (h11 Int))
:formula (and
; check requirement 1 (chip width and height)
(>= x0 0) (>= y0 0) (<= (+ x0 w0) 30) (<= (+ y0 h0) 30)
; check requirement 2 or 3 (component width)
(or (and (= w0 4) (= h0 3)) (and (= w0 3) (= h0 4)))
...
(>= x11 0) (>= y11 0) (<= (+ x11 w11) 30) (<= (+ y11 h11) 30)
(or (and (= w11 10) (= h11 20)) (and (= w11 20) (= h11 10)))
; check requirement 4 (no overlap, may be turned)
(or (<= (+ y1 h1) y0) (<= (+ x1 w1) x0)
    (>= y1 (+ y0 h0)) (>= x1 (+ x0 w0)))
...
(or (<= (+ y11 h11) y10) (<= (+ x11 w11) x10)
    (>= y11 (+ y10 h10)) (>= x11 (+ x10 w10)))
; check requirement 6 (minimum distance between power components)
(or (>= (+ x0 (/ w0 2)) (+ (+ x1 (/ w1 2)) 17))
    ...
)
; check requirement 5 (power for regular components)
(or (and
      (or (= (+ y0 h0) y2) (= y0 (+ y2 h2)))
      (or (and (<= x2 x0) (<= x0 (+ x2 w2)))
          (and (<= x2 (+ x0 w0)) (<= (+ x0 w0) (+ x2 w2)))
    ))
    ...
)...))
\end{lstlisting}

\begin{figure}
\centering
\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] (14.01, 5.01) rectangle (17.99, 7.99);
\node[align=center] at (16.000000,6.500000) {0\\(14,5)\\(4 x 3)};
\draw[draw=green,fill=red] (7.01, 22.01) rectangle (9.99, 25.99);
\node[align=center] at (8.500000,24.000000) {1\\(7,22)\\(3 x 4)};
\draw[draw=blue] (14.01, 0.01) rectangle (17.99, 4.99);
\node[align=center] at (16.000000,2.500000) {2\\(14,0)\\(4 x 5)};
\draw[draw=cyan] (14.01, 8.01) rectangle (17.99, 13.99);
\node[align=center] at (16.000000,11.000000) {3\\(14,8)\\(4 x 6)};
\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] (18.01, 1.01) rectangle (26.99, 6.99);
\node[align=center] at (22.500000,4.000000) {5\\(18,1)\\(9 x 6)};
\draw[draw=darkgray] (4.01, 6.01) rectangle (13.99, 11.99);
\node[align=center] at (9.000000,9.000000) {6\\(4,6)\\(10 x 6)};
\draw[draw=lightgray] (3.01, 0.01) rectangle (13.99, 5.99);
\node[align=center] at (8.500000,3.000000) {7\\(3,0)\\(11 x 6)};
\draw[draw=brown] (0.01, 22.01) rectangle (6.99, 29.99);
\node[align=center] at (3.500000,26.000000) {8\\(0,22)\\(7 x 8)};
\draw[draw=olive] (18.01, 7.01) rectangle (29.99, 13.99);
\node[align=center] at (24.000000,10.500000) {9\\(18,7)\\(12 x 7)};
\draw[draw=orange] (0.01, 12.01) rectangle (9.99, 21.99);
\node[align=center] at (5.000000,17.000000) {10\\(0,12)\\(10 x 10)};
\draw[draw=pink] (10.01, 14.01) rectangle (29.99, 23.99);
\node[align=center] at (20.000000,19.000000) {11\\(10,14)\\(20 x 10)};
\end{tikzpicture}
\caption{\label{fig:chipDesign}Visualization of chip design satisfying the
given requirements ($m=2$, $n=10$, $powerDistance=17$). The red boxes mark the
power components. The component index is given, followed by the coordinate
of the bottom-left corner and the dimension.}
\end{figure}

\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 \texttt{unsat}.
We also reformed all previously mentioned requirements into formulae that can be
used in z3 as shown in Listing~\ref{lst:jobScheduling}.

\begin{lstlisting}[caption={SMT for Job Scheduling},label={lst:jobScheduling},language=lisp,basicstyle=\scriptsize]
(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}

The complete scheduling output, where an integer represents the time at which a job was started is as follows:
\begin{lstlisting}
j1 -> 1
j2 -> 0
j3 -> 7
j4 -> 0
j5 -> 15
j6 -> 0
j7 -> 25
j8 -> 15
j9 -> 28
j10 -> 0
j11 -> 15
j12 -> 42
\end{lstlisting}

Note that $42 + 12 + 5$ is indeed equal to $59$.

\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 within job 12:

\begin{lstlisting}[language=lisp,basicstyle=\scriptsize]
(>= j6 j12)
(<= (+ j6 11) (+ j12 17))
\end{lstlisting}

With those 2 extra formula lines, the new schedule becomes:

\begin{lstlisting}
j1 -> 1
j2 -> 0
j3 -> 7
j4 -> 0
j5 -> 15
j6 -> 42
j7 -> 53
j8 -> 15
j9 -> 28
j10 -> 0
j11 -> 15
j12 -> 42
\end{lstlisting}
Note that $53 + 7 + 5$ is indeed equal to $65$.

\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}