\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{%
    Peter Wu (0783206)\\
    \texttt{s.p.wu@student.tue.nl}
\and
    Koen van der Heijden (0807929)\\
    \texttt{k.p.l.v.d.heijden@student.tue.nl}
}
\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.

\begin{itemize}
\item[(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.
\item[(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.
\end{itemize}

\subsection*{Solution:}
\subsubsection*{(a)}
We generalize this problem to fitting $m$ different types of pallets into $n$
trucks. Let $B$ be the set of pallet types (with building blocks).
Each type of a building block $b \in B$ has a corresponding weight $W_b$ and a
total number $C_b$ that must be spread over all trucks.
We introduce $m \times n$ different variables that describe how many
pallets of each type are assigned to each truck. For every truck $1 \leq j \leq
n$ and every $b \in B$, we define variable $b_j$ as the number of pallets of
type $b$ assigned to truck $j$.

In our scenario, $B = \{ N, P, S, C, D \}$ (denoting Nuzzles, Prittles,
Skipples, Crottles and Dupples respectively).
We have maximum weight capacity $W_{truck}=8000$ and maximum pallet capacity
$C_{truck}=8$.

First a sanity check, the number of assigned pallets must be positive:
\begin{align}
\label{eq:truck1}
\bigwedge_{b \in B}
\bigwedge_{i=1}^n
b_i \geq 0
\end{align}

Next, we require that all pallets are indeed distributed over the trucks:
\begin{align}
\label{eq:truck2}
\bigwedge_{b \in B}
C_b =
\sum_{i=1}^n
b_i
\end{align}

Each truck has a maximum pallet and weight capacity that must not be exceeded:
\begin{align}
\label{eq:truck3}
\bigwedge_{i=1}^n
(
    (\sum_{b \in B} b_i)
    \leq
    C_{truck}
) \land (
    (\sum_{b \in B} b_i \cdot w_i)
    \leq
    W_{truck}
)
\end{align}

The above ingredients describe the basic capacity requirements. Next, additional
requirements are incorporated. These may make some of the above requirements
partially unnecessary, but we choose to keep these for easier understanding.
Optimizations (like subsumption) can be easily handled by the SAT solvers.

At most three trucks can store Skipples. This can be expressed as each triple of
trucks having the sum equal to $C_S$ (the total number of skipples).
Or alternatively, all trucks other than these triple must carry zero Skipples.
We tried to implement both, but for some reason the second comparison was faster
(probably because the first one was expressed as a conjunction with small
disjunctions while the latter one is expressed as one big disjunction). The
alternative is expressed as:
\begin{align}
\label{eq:truck4}
\bigvee_{1 \leq x,y,z \leq n, x \neq y, y \neq z, x \neq z}
\bigwedge_{1 \leq i \leq n, i \not\in\{x,y,z\}}^n
S_i = 0
\end{align}

Finally the limitation that trucks can carry only one pallet of Nuzzles:
\begin{align}
\label{eq:truck5}
\bigwedge_{i=1}^n
N_i \leq 1
\end{align}

We wrote a generator program that takes the conjunction of the above parts
(ingredients \ref{eq:truck1}, \ref{eq:truck2}, \ref{eq:truck3}, \ref{eq:truck4}
and \ref{eq:truck5}). At first, $C_P$ was unknown, so we removed clauses that
relied on this. The initial evaluation with z3 finished within a second and
allowed us to make a better educated guess at the actual (maximum) value of
$C_P$. It turns out that with 22 pallets were unassigned, so we used this in the
next evaluation.

Evaluation of the generated output (shown in Listing~\ref{lst:palletsInTrucks})
using the command \texttt{python generate-packingpallets.py 22 | z3 -smt -in}
finished in 100 milliseconds. The result is shown in
Table~\ref{tbl:palletsInTrucks}. It happens that all trucks can be filled,
including 22 Prittles. As mentioned before, the alternative check for
Ingredient~\ref{eq:truck4} takes more time (200ms).

\begin{table}[H]
\centering
\begin{tabular}{r|rrrrr|rr}
   &     N &     P &     S &     C &     D & weight & \#pallets \\
\hline
 1 &     1 &     5 &     0 &     2 &     0 &  7700 & 8 \\
 2 &     1 &     1 &     0 &     2 &     4 &  6900 & 8 \\
 3 &     0 &     3 &     0 &     2 &     3 &  6800 & 8 \\
 4 &     0 &     0 &     8 &     0 &     0 &  8000 & 8 \\
 5 &     1 &     7 &     0 &     0 &     0 &  3500 & 8 \\
 6 &     1 &     0 &     0 &     2 &     5 &  6700 & 8 \\
 7 &     0 &     6 &     0 &     2 &     0 &  7400 & 8 \\
 8 &     0 &     0 &     0 &     0 &     8 &  1600 & 8 \\
\hline
   &     4 &    22 &     8 &    10 &    20
\end{tabular}
\caption{\label{tbl:palletsInTrucks}The assignment of pallets to trucks. The
    rows of the table body describe the contents of a truck. The last row shows
    the total number of one pallet type as distributed over all trucks.}
\end{table}

\begin{lstlisting}[
    caption={Generated SMT for pallet fitting problem.},
    label={lst:palletsInTrucks},language=lisp,basicstyle=\scriptsize
]
(benchmark test.smt
:logic QF_UFLIA
:extrafuns (
(N1 Int) (P1 Int) (S1 Int) (C1 Int) (D1 Int)
...
(N8 Int) (P8 Int) (S8 Int) (C8 Int) (D8 Int)
)
:formula (and
(>= N1 0) (>= P1 0) (>= S1 0) (>= C1 0) (>= D1 0)
...
(>= N8 0) (>= P8 0) (>= S8 0) (>= C8 0) (>= D8 0)
(= 4 (+ N1 N2 N3 N4 N5 N6 N7 N8))
(= 22 (+ P1 P2 P3 P4 P5 P6 P7 P8))
(= 8 (+ S1 S2 S3 S4 S5 S6 S7 S8))
(= 10 (+ C1 C2 C3 C4 C5 C6 C7 C8))
(= 20 (+ D1 D2 D3 D4 D5 D6 D7 D8))
(>= 8 (+ N1 P1 S1 C1 D1))
(>= 8000 (+ (* N1 700) (* P1 400) (* S1 1000) (* C1 2500) (* D1 200)))
...
(>= 8 (+ N8 P8 S8 C8 D8))
(>= 8000 (+ (* N8 700) (* P8 400) (* S8 1000) (* C8 2500) (* D8 200)))
(or (= 0 S4) (= 0 S5) (= 0 S6) (= 0 S7) (= 0 S8))
(or (= 0 S3) (= 0 S5) (= 0 S6) (= 0 S7) (= 0 S8))
...
(or (= 0 S1) (= 0 S2) (= 0 S3) (= 0 S4) (= 0 S6))
(or (= 0 S1) (= 0 S2) (= 0 S3) (= 0 S4) (= 0 S5))
(>= 1 N1) (>= 1 N2) (>= 1 N3) (>= 1 N4) (>= 1 N5) (>= 1 N6) (>= 1 N7) (>= 1 N8)
))
\end{lstlisting}


\subsubsection*{(b)}
The constraint that Prittles and Crottles cannot be transported together can be
expressed as either one of them being zero:
\begin{align}
\label{eq:truckB}
\bigwedge_{i=1}^n
P_i = 0 \lor C_i = 0
\end{align}

The command \texttt{python generate-packingpallets.py 22 b | z3 -smt -in} does
the same as (a), but with the additional restriction above added to the
conjunction. After 40 seconds, it output ``unsat'' for $C_P=22$.

For $C_P=21$, a satisfying assignment was found within 100 milliseconds. Its
assignment is shown in Table~\ref{tbl:palletsInTrucksB}.


\begin{table}[H]
\centering
\begin{tabular}{r|rrrrr|rr}
   &     N &     P &     S &     C &     D & weight & \#pallets \\
\hline
 1 &     0 &     0 &     2 &     2 &     4 &  7800 & 8 \\
 2 &     1 &     7 &     0 &     0 &     0 &  3500 & 8 \\
 3 &     1 &     0 &     0 &     2 &     4 &  6500 & 7 \\
 4 &     1 &     7 &     0 &     0 &     0 &  3500 & 8 \\
 5 &     0 &     0 &     2 &     2 &     4 &  7800 & 8 \\
 6 &     1 &     7 &     0 &     0 &     0 &  3500 & 8 \\
 7 &     0 &     0 &     2 &     2 &     4 &  7800 & 8 \\
 8 &     0 &     0 &     2 &     2 &     4 &  7800 & 8 \\
\hline
   &     4 &    21 &     8 &    10 &    20
\end{tabular}
\caption{\label{tbl:palletsInTrucksB}The assignment of pallets to trucks with
    an additional restriction on Prittles and Crottles. The rows of the table
    body describe the contents of a truck. The last row shows the total number
    of one pallet type as distributed over all trucks.}
\end{table}

\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 \nonumber \\
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
(ingredients \ref{eq:chip1}, \ref{eq:chip2}, \ref{eq:chip3}, \ref{eq:chip4} and
\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}[H]
\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}

\begin{itemize}
\item[(a)] Find a solution of this scheduling problem for which the total
    running time is minimal.
\item[(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.
\end{itemize}

\subsection*{Solution:}
\subsubsection*{(a)}
The problem can be generalized to scheduling of $n$ jobs $J$, where each job $i
\in J$ has a start time $t_i$ and a duration $d_i$. Job dependencies can also be
described in an abstract manner:
\begin{itemize}
\item Let $E$ be the set of jobs that requires other jobs to be finished before
    it can start. Let $E_i$ be the required jobs for a job $i \in E$.
\item Let $S$ be the set of jobs that requires other jobs to be started before
    it can start. Let $S_i$ be the required jobs for a job $i \in S$.
\end{itemize}
The goal is to find the minimal total running time, that is, deadline $D$.

Now we can start listing the ingredients. First a sanity check, we assume that
the time starts counting from zero to make calculations easier:
\begin{align}
\label{eq:sched1}
\bigwedge_{i=1}^n t_i \geq 0
\end{align}

Job $i$ may not start before jobs $E_i$ have finished:
\begin{align}
\label{eq:sched2}
\bigwedge_{i \in E}
\bigwedge_{j \in E_i}
t_j + d_j \leq t_i
\end{align}

Job $i$ may not start before jobs $S_i$ have started:
\begin{align}
\label{eq:sched3}
\bigwedge_{i \in S}
\bigwedge_{j \in S_i}
t_j \leq t_i
\end{align}

Let $RL \subseteq J$ be the set of three resource limited jobs. The constraint
that at most two jobs of this set can run in parallel can alternatively be
described as: any of the three jobs must not start before another of the three
has finished. When this holds, then for sure we have at most two concurrent
jobs. This can be expressed as:
\begin{align}
\label{eq:sched4}
\bigvee_{i,j \in RL, i \neq j}
t_i + d_i \leq t_j
\end{align}

To establish whether the resulting job scheduling is indeed minimal, we add an
additional constraint to check whether all jobs complete before the deadline:
\begin{align}
\label{eq:sched5}
\bigwedge_{i=1}^n t_i + d_i \geq D
\end{align}

The conjunction of the above ingredients \ref{eq:sched1}, \ref{eq:sched2},
\ref{eq:sched3}, \ref{eq:sched4} and \ref{eq:sched5} are put in a generator
script which outputs a SMT program (shown in Listing~\ref{lst:jobScheduling}. We
run it with \texttt{python generate-jobscheduling.py | z3 -smt -in} which
completes in 40 milliseconds. Its result is shown in
Figure~\ref{fig:jobScheduling}. To confirm that this job schedule is indeed
minimal, we set $D=58$ and observe that the program outputs ``unsat'' within 40
milliseconds.

\begin{figure}[H]
\centering
\begin{tikzpicture}
%
\draw[draw=red,fill=red] (0.0, 6.1) rectangle (1.2000000000000002, 6.4);
\node[anchor=east] at (-0.100000,6.200000) {1};
\node[anchor=west] at (1.300000,6.200000) {0 + 6 = 6};
\draw[draw=green,fill=green] (0.0, 5.6) rectangle (1.4000000000000001, 5.9);
\node[anchor=east] at (-0.100000,5.700000) {2};
\node[anchor=west] at (1.500000,5.700000) {0 + 7 = 7};
\draw[draw=blue,fill=blue] (0.0, 5.1) rectangle (1.8, 5.4);
\node[anchor=east] at (-0.100000,5.200000) {4};
\node[anchor=west] at (1.900000,5.200000) {0 + 9 = 9};
\draw[draw=cyan,fill=cyan] (0.0, 4.6) rectangle (2.2, 4.9);
\node[anchor=east] at (-0.100000,4.700000) {6};
\node[anchor=west] at (2.300000,4.700000) {0 + 11 = 11};
\draw[draw=magenta,fill=magenta] (1.4000000000000001, 4.1) rectangle (3.0, 4.4);
\node[anchor=east] at (-0.100000,4.200000) {3};
\node[anchor=west] at (3.100000,4.200000) {7 + 8 = 15};
\draw[draw=gray,fill=gray] (2.2, 3.6) rectangle (5.2, 3.9);
\node[anchor=east] at (-0.100000,3.700000) {10};
\node[anchor=west] at (5.300000,3.700000) {11 + 15 = 26};
\draw[draw=darkgray,fill=darkgray] (3.0, 3.1) rectangle (5.0, 3.4);
\node[anchor=east] at (-0.100000,3.200000) {5};
\node[anchor=west] at (5.100000,3.200000) {15 + 10 = 25};
\draw[draw=lightgray,fill=lightgray] (3.0, 2.6) rectangle (5.6, 2.9);
\node[anchor=east] at (-0.100000,2.700000) {8};
\node[anchor=west] at (5.700000,2.700000) {15 + 13 = 28};
\draw[draw=brown,fill=brown] (5.0, 2.1) rectangle (7.4, 2.4);
\node[anchor=east] at (-0.100000,2.200000) {7};
\node[anchor=west] at (7.500000,2.200000) {25 + 12 = 37};
\draw[draw=olive,fill=olive] (5.2, 1.6) rectangle (8.4, 1.9);
\node[anchor=east] at (-0.100000,1.700000) {11};
\node[anchor=west] at (8.500000,1.700000) {26 + 16 = 42};
\draw[draw=orange,fill=orange] (5.6000000000000005, 1.1) rectangle (8.4, 1.4);
\node[anchor=east] at (-0.100000,1.200000) {9};
\node[anchor=west] at (8.500000,1.200000) {28 + 14 = 42};
\draw[draw=pink,fill=pink] (8.4, 0.6) rectangle (11.8, 0.9);
\node[anchor=east] at (-0.100000,0.700000) {12};
\node[anchor=west] at (11.900000,0.700000) {42 + 17 = 59};
%
\end{tikzpicture}
\caption{\label{fig:jobScheduling}Result of job scheduling for (a).}
\end{figure}

\begin{lstlisting}[
    caption={Generated SMT program for job scheduling problem (a).},
    label={lst:jobScheduling},basicstyle=\scriptsize
]
(benchmark test.smt
:logic QF_UFLIA
:extrafuns (
(t1 Int) (d1 Int) (t2 Int) (d2 Int) (t3 Int) (d3 Int)
(t4 Int) (d4 Int) (t5 Int) (d5 Int) (t6 Int) (d6 Int)
(t7 Int) (d7 Int) (t8 Int) (d8 Int) (t9 Int) (d9 Int)
(t10 Int) (d10 Int) (t11 Int) (d11 Int) (t12 Int) (d12 Int)
)
:formula (and
(>= t1 0) (<= (+ t1 d1) 59) (>= t2 0) (<= (+ t2 d2) 59)
(>= t3 0) (<= (+ t3 d3) 59) (>= t4 0) (<= (+ t4 d4) 59)
(>= t5 0) (<= (+ t5 d5) 59) (>= t6 0) (<= (+ t6 d6) 59)
(>= t7 0) (<= (+ t7 d7) 59) (>= t8 0) (<= (+ t8 d8) 59)
(>= t9 0) (<= (+ t9 d9) 59) (>= t10 0) (<= (+ t10 d10) 59)
(>= t11 0) (<= (+ t11 d11) 59) (>= t12 0) (<= (+ t12 d12) 59)
(= d1 6) (= d2 7) (= d3 8) (= d4 9)
(= d5 10) (= d6 11) (= d7 12) (= d8 13)
(= d9 14) (= d10 15) (= d11 16) (= d12 17)
(<= (+ t1 d1) t3) (<= (+ t2 d2) t3) (<= (+ t3 d3) t5)
(<= (+ t4 d4) t5) (<= (+ t3 d3) t7) (<= (+ t4 d4) t7)
(<= (+ t6 d6) t7) (<= (+ t5 d5) t9) (<= (+ t8 d8) t9)
(<= (+ t10 d10) t11) (<= (+ t9 d9) t12) (<= (+ t11 d11) t12)
(<= t5 t8)
(or (<= (+ t5 d5) t7) (<= (+ t5 d5) t10) (<= (+ t7 d7) t5)
    (<= (+ t7 d7) t10) (<= (+ t10 d10) t5) (<= (+ t10 d10) t7))
))
\end{lstlisting}


\subsubsection*{(b)}
The extra constraint states that job 6 may only be run when it fits within the
scheduled time of job 12:
\begin{align}
\label{eq:sched6}
t_{12} \leq t_6 \land t_6 + d_6 \leq t_{12} + d_{12}
\end{align}

After modifying the program from (a) by adding \texttt{(and (<= t12 t6) (<= (+
t6 d6) (+ t12 d12)))} to the formula, a satisfying assignment was found for
$D=65$ in 50 milliseconds (shown in Figure~\ref{fig:jobSchedulingB}). For
$D=64$, ``unsat'' was output (in 50ms).

\begin{figure}[H]
\centering
\begin{tikzpicture}
%
\draw[draw=red,fill=red] (0.0, 6.1) rectangle (1.4000000000000001, 6.4);
\node[anchor=east] at (-0.100000,6.200000) {2};
\node[anchor=west] at (1.500000,6.200000) {0 + 7 = 7};
\draw[draw=green,fill=green] (0.0, 5.6) rectangle (1.8, 5.9);
\node[anchor=east] at (-0.100000,5.700000) {4};
\node[anchor=west] at (1.900000,5.700000) {0 + 9 = 9};
\draw[draw=blue,fill=blue] (0.0, 5.1) rectangle (3.0, 5.4);
\node[anchor=east] at (-0.100000,5.200000) {10};
\node[anchor=west] at (3.100000,5.200000) {0 + 15 = 15};
\draw[draw=cyan,fill=cyan] (0.2, 4.6) rectangle (1.4000000000000001, 4.9);
\node[anchor=east] at (-0.100000,4.700000) {1};
\node[anchor=west] at (1.500000,4.700000) {1 + 6 = 7};
\draw[draw=magenta,fill=magenta] (1.4000000000000001, 4.1) rectangle (3.0, 4.4);
\node[anchor=east] at (-0.100000,4.200000) {3};
\node[anchor=west] at (3.100000,4.200000) {7 + 8 = 15};
\draw[draw=gray,fill=gray] (3.0, 3.6) rectangle (5.0, 3.9);
\node[anchor=east] at (-0.100000,3.700000) {5};
\node[anchor=west] at (5.100000,3.700000) {15 + 10 = 25};
\draw[draw=darkgray,fill=darkgray] (3.0, 3.1) rectangle (5.6, 3.4);
\node[anchor=east] at (-0.100000,3.200000) {8};
\node[anchor=west] at (5.700000,3.200000) {15 + 13 = 28};
\draw[draw=lightgray,fill=lightgray] (3.0, 2.6) rectangle (6.2, 2.9);
\node[anchor=east] at (-0.100000,2.700000) {11};
\node[anchor=west] at (6.300000,2.700000) {15 + 16 = 31};
\draw[draw=brown,fill=brown] (5.6000000000000005, 2.1) rectangle (8.4, 2.4);
\node[anchor=east] at (-0.100000,2.200000) {9};
\node[anchor=west] at (8.500000,2.200000) {28 + 14 = 42};
\draw[draw=olive,fill=olive] (8.4, 1.6) rectangle (10.600000000000001, 1.9);
\node[anchor=east] at (-0.100000,1.700000) {6};
\node[anchor=west] at (10.700000,1.700000) {42 + 11 = 53};
\draw[draw=orange,fill=orange] (8.4, 1.1) rectangle (11.8, 1.4);
\node[anchor=east] at (-0.100000,1.200000) {12};
\node[anchor=west] at (11.900000,1.200000) {42 + 17 = 59};
\draw[draw=pink,fill=pink] (10.600000000000001, 0.6) rectangle (13.000000000000002, 0.9);
\node[anchor=east] at (-0.100000,0.700000) {7};
\node[anchor=west] at (13.100000,0.700000) {53 + 12 = 65};
%
\end{tikzpicture}
\caption{\label{fig:jobSchedulingB}Result of job scheduling for (b).}
\end{figure}

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

\begin{itemize}
\item[(a)] Show how it is possible that $a_3 = a_7$ after a number of steps.
\item[(b)] Show how it is possible that $a_3 = a_5 = a_7$ after a number of steps.
\end{itemize}
For this problem both try to use an SMT solver and NuSMV, and discuss how they perform.

\subsection*{Solution:}
\subsubsection*{(a)}
We generalize this problem to $n$ variables $a_1, a_2, \ldots, a_n$. Let
$a_{i,0}$ denote the variables $a_i$ in the initial state.
Let $m$ denote the number of steps we need to reach the desired configuration
(this is the value we have to find out).
Let $a_{i,s}$ denote the variables $a_i$ after $1 \leq s \leq m$ steps.

A sketch of the solution will involve $n \times (1 + m)$ literals ($n$ in the
initial state, $n \times m$ after $m$ steps). The formula will consist of a
conjunction of the initial states, transition relations and an ingredient
describing the desired configuration.

(Note that the given change ($a_{i,s} = a_{i-1,s-1} + a_{i+1,s-1}$ for $1 < i <
n$ and $1 \leq s \leq m$) will always keep the first and last values unchanged
throughout the execution. So only one $a_1$ and $a_n$ would be sufficient. For
symmetry with all other variables, and to allow for arbitrary other changes in a
step, we have decided to keep this though.)

The ingredient to model the initial state:
\begin{align}
\label{eq:sum1}
\bigwedge_{i=1}^n a_{i,0} = i
\end{align}

Next, we try to reach the goal of finding $a_3=a_7$ in any state:
\begin{align}
\label{eq:sum2}
\bigvee_{s=0}^m a_{3,s} = a_{7,s}
\end{align}
Technically we can start with $s=1$ instead of $s=0$ since the values in the
initial state are all unique. We chose to keep it though such that the solution
can be generalized for arbitrary values in the initial state.

Finally we add the transition relations for each step $1 \leq s \leq m$ (reached
from the previous step $s-1$). In each transition, one variable $1 < i < n$ will
be changed to match the (previous) values of the neighbors while all others are
unchanged from the previous state:
\begin{align}
\label{eq:sum3}
\bigwedge_{s=1}^m
\bigvee_{i=2}^{n-1} (
a_{i,s} = a_{i-1,s-1} + a_{i+1,s-1} \land
\bigwedge_{1 \leq j \leq n, i \neq j} a_{j,s} = a_{j,s-1}
)
\end{align}

The conjunction of ingredients \ref{eq:sum1}, \ref{eq:sum2} and \ref{eq:sum3}
form the formula that is parameterized by $n$ and $m$. For our problem, $n=8$ so
we have to find $m$. At first we picked $m=20$ (arbitrary) and then narrowed
down $m$ using a binary search. In the end we found that $m=7$ is the minimum
solution. The resulting assignment was obtained using the command
\texttt{python generate-neighborsum.py 7 | z3 -smt -in} which completed within a
fraction of a second (even for $m=20$).
The annotated, generated input for \texttt{z3} is shown in
Listing~\ref{lst:sumA} while the z3 output is formatted into
Table~\ref{tbl:sumA}.

\begin{minipage}{.45\textwidth}
\begin{table}[H]
\centering
\begin{tabular}{r|rrrrrrrr}
   & $a_1$ & $a_2$ & $a_3$ & $a_4$ & $a_5$ & $a_6$ & $a_7$ & $a_8$ \\
\hline
 0 &     1 &     2 &     3 &     4 &     5 &     6 &     7 &     8 \\
 1 &     1 &     2 & \bf 6 &     4 &     5 &     6 &     7 &     8 \\
 2 &     1 &     2 &     6 & \bf11 &     5 &     6 &     7 &     8 \\
 3 &     1 &     2 & \bf13 &    11 &     5 &     6 &     7 &     8 \\
 4 &     1 &     2 &    13 & \bf18 &     5 &     6 &     7 &     8 \\
 5 &     1 &     2 &    13 &    18 &     5 & \bf12 &     7 &     8 \\
 6 &     1 &     2 &    13 &    18 &     5 &    12 & \bf20 &     8 \\
 7 &     1 &     2 & \bf20 &    18 &     5 &    12 &    20 &     8 \\
\end{tabular}
\caption{\label{tbl:sumA}The values of each variable where the modified values
in each step are highlighted. Indeed, $a_3=a_7=20$ after some steps.}
\end{table}
\end{minipage}
\hfill
\begin{minipage}{.45\textwidth}
\begin{lstlisting}[
    caption={NuSMV output for $n=8$ and maximum value 100 that satisfies
    $a_3=a_7=20$ after 8 rounds.},
    label={lst:sumAsmvOutput},basicstyle=\scriptsize
]
Trace Type: Counterexample
  -> State: 1.1 <-
    a1 = 1
    a2 = 2
    a3 = 3
    a4 = 4
    a5 = 5
    a6 = 6
    a7 = 7
    a8 = 8
  -> State: 1.2 <-
    a3 = 6
  -> State: 1.3 <-
    a4 = 11
  -> State: 1.4 <-
    a3 = 13
  -> State: 1.5 <-
    a6 = 12
  -> State: 1.6 <-
    a7 = 20
  -> State: 1.7 <-
    a4 = 18
  -> State: 1.8 <-
    a3 = 20
\end{lstlisting}
\end{minipage}

\begin{lstlisting}[
    caption={Generated SMT program for $n=8, m=7$ that satisfies $a_3=a_7$},
    label={lst:sumA},language=lisp,basicstyle=\scriptsize
]
(benchmark test.smt
:logic QF_UFLIA
:extrafuns (
(a1_0 Int) ...  (a8_0 Int)
...
(a1_7 Int) ...  (a8_7 Int)
)
:formula (and
(= a1_0 1) ...  (= a8_0 8)
; trying to reach the goal in each state
(or (= a3_0 a7_0) ... (= a3_7 a7_7))
; in each state, one of the n-2=6 values must change,
; while leaving the others unchanged from the previous state.
(or
  (and (= a2_1 (+ a1_0 a3_0))
       (= a1_1 a1_0) ...  (= a8_1 a8_0))
  ...
  (and (= a7_1 (+ a6_0 a8_0))
       (= a1_1 a1_0) ...  (= a8_1 a8_0))
)
...
(or
  (and (= a2_7 (+ a1_6 a3_6))
       (= a1_7 a1_6) ...  (= a8_7 a8_6))
  ...
  (and (= a7_7 (+ a6_6 a8_6))
       (= a1_7 a1_6) ...  (= a8_7 a8_6))
  )
))
\end{lstlisting}

\textbf{Remark}: we observed that for some larger choices of $m$ (say $m=20$),
duplicate states (rows) occur having the same values for the variables. This can
be explained by the conjunction used in ingredient~\ref{eq:sum2}. When the
previous value is already the sum of the neighbors, then the new sum will be
equal to the previous one. As the other variables remain unchanged, the whole
state will have the same values as the previous state.

The same problem was also solved with NuSMV. Here we do not model every possible
transition between state $s-1$ and $s$ (for all $1 \leq s < m$). Instead, we
describe the form of a transition in terms of the begin state and the next
state for $n$ variables (and no $m$ parameter is necessary). Again, only one of
the variables are updated while all others stay unchanged, this can be expressed
in NuSMV as follows:
\begin{align*}
\bigvee_{1 < i < n}
next(a_i) = a_{i-1} + a_{i+1}
\land
(\bigwedge_{1 \leq j \leq n, i \neq j} next(a_j) = a_j)
\end{align*}

In the given problem, the first and last elements are unchanged (as before), so
$next(a_1)=a_1 \land next(a_n) = a_n$ can be moved outside the large
disjunction.

As for the initialization, the range $0..100$ was chosen arbitrarily, but given
the answer from the SMT solver, we know that it should be sufficient.

To find out when the desired condition ($a_3=a_7$) is satisfied for the first
time, we add a $\lnot (a_3=a_7)$ as global formula. When a counter example is
found, then we know that this particular run exhibits the desired condition.

Listing~\ref{lst:sumAsmv} shows the full implementation for $n=8$. NuSMV found a
counterexample (shown in Listing~\ref{lst:sumAsmvOutput}) and took 51 seconds.
This is much longer than the SMT solver (which solved this setting in 5
seconds). Interestingly, by reducing the maximum values of $a_i$ from 100 to 20,
the running time dropped to less than a second. Reducing the maximum to 19
yields no counterexample and also completed in a fraction of a second.
For a maximum of 50, the running time is 6 seconds. Indeed, increasing the
maximum value also results in larger trees with more nodes to check. Choosing
the maximum too small might fail to find a satisfying assignment while a too
large value incurs a performance hit.

\begin{lstlisting}[
    caption={Generated NuSMV program for $n=8$ that searches for $a_3=a_7$.},
    label={lst:sumAsmv},basicstyle=\tiny
]
MODULE main
VAR
a1 : 0..100; a2 : 0..100; a3 : 0..100; a4 : 0..100; a5 : 0..100; a6 : 0..100; a7 : 0..100; a8 : 0..100;
INIT
a1 = 1 & a2 = 2 & a3 = 3 & a4 = 4 & a5 = 5 & a6 = 6 & a7 = 7 & a8 = 8
TRANS
next(a1) = a1 & next(a8) = a8 & (
(next(a2) = a1 + a3 & next(a3) = a3 & next(a4) = a4 & next(a5) = a5 & next(a6) = a6 & next(a7) = a7)|
(next(a3) = a2 + a4 & next(a2) = a2 & next(a4) = a4 & next(a5) = a5 & next(a6) = a6 & next(a7) = a7)|
(next(a4) = a3 + a5 & next(a2) = a2 & next(a3) = a3 & next(a5) = a5 & next(a6) = a6 & next(a7) = a7)|
(next(a5) = a4 + a6 & next(a2) = a2 & next(a3) = a3 & next(a4) = a4 & next(a6) = a6 & next(a7) = a7)|
(next(a6) = a5 + a7 & next(a2) = a2 & next(a3) = a3 & next(a4) = a4 & next(a5) = a5 & next(a7) = a7)|
(next(a7) = a6 + a8 & next(a2) = a2 & next(a3) = a3 & next(a4) = a4 & next(a5) = a5 & next(a6) = a6))
LTLSPEC G ! (a3 = a7)
\end{lstlisting}



\subsubsection*{(b)}
The generic approach from (a) can be adopted for this solution with a minor
modification. Simply replace the second ingredient by:
\begin{align}
\label{eq:sum2new}
\bigvee_{s=0}^m a_{3,s} = a_{5,s} \land a_{5,s} = a_{7,s}
\end{align}

Interestingly, the runtime of the SMT solver varies. For $m=25$, a solution was
found in 9 seconds. For $m=22$, it took 5 seconds to find one. For $m=10, 15,
16$, no satisfying assignment was found in respectively 1, 82 and 286 seconds.
$m=17$ is apparently the minimal satisfying solution which was found in 3.5
seconds and shown in Table~\ref{tbl:sumB}.
(Also interesting was that $m=18, 19, 20$ also found satisfying solutions in
3.2, 5.9 and 3.0 seconds (in that order).)

The NuSMV program needs a similar modification to the \texttt{LTLSPEC} line, its
output is shown in in Listing~\ref{lst:sumAsmvOutput2}. This also took 51
seconds, just like (a). Lowering the maximum from 100 to 46 reduced the running
time to about 2.2 seconds while a maximum value of 50 took 3.5 seconds. The
explanation from (a) about the relation between the maximum value and the
running time is still valid.

\begin{minipage}{.45\textwidth}
\begin{table}[H]
\centering
\begin{tabular}{r|rrrrrrrr}
   & $a_1$ & $a_2$ & $a_3$ & $a_4$ & $a_5$ & $a_6$ & $a_7$ & $a_8$ \\
\hline
 0 &     1 &     2 &     3 &     4 &     5 &     6 &     7 &     8 \\
 1 &     1 &     2 &     3 & \bf 8 &     5 &     6 &     7 &     8 \\
 2 &     1 &     2 &     3 &     8 &     5 & \bf12 &     7 &     8 \\
 3 &     1 & \bf 4 &     3 &     8 &     5 &    12 &     7 &     8 \\
 4 &     1 &     4 &     3 &     8 &     5 &    12 & \bf20 &     8 \\
 5 &     1 &     4 & \bf12 &     8 &     5 &    12 &    20 &     8 \\
 6 &     1 & \bf13 &    12 &     8 &     5 &    12 &    20 &     8 \\
 7 &     1 &    13 &    12 &     8 & \bf20 &    12 &    20 &     8 \\
 8 &     1 &    13 & \bf21 &     8 &    20 &    12 &    20 &     8 \\
 9 &     1 &    13 &    21 &     8 &    20 & \bf40 &    20 &     8 \\
10 &     1 & \bf22 &    21 &     8 &    20 &    40 &    20 &     8 \\
11 &     1 &    22 &    21 &     8 &    20 &    40 & \bf48 &     8 \\
12 &     1 &    22 & \bf30 &     8 &    20 &    40 &    48 &     8 \\
13 &     1 & \bf31 &    30 &     8 &    20 &    40 &    48 &     8 \\
14 &     1 &    31 &    30 &     8 & \bf48 &    40 &    48 &     8 \\
15 &     1 &    31 & \bf39 &     8 &    48 &    40 &    48 &     8 \\
16 &     1 & \bf40 &    39 &     8 &    48 &    40 &    48 &     8 \\
17 &     1 &    40 & \bf48 &     8 &    48 &    40 &    48 &     8 \\
\end{tabular}
\caption{\label{tbl:sumB}The values of each variable where modified values in
each step are highlighted. Indeed, $a_3=a_5=a_7=48$ after some steps.}
\end{table}
\end{minipage}
\hfill
\begin{minipage}{.45\textwidth}
\begin{lstlisting}[
    caption={NuSMV program for $n=8$ and maximum value 100 that satisfies
    $a_3=a_5=a_7=46$ after 17 rounds.},
    label={lst:sumAsmvOutput2},basicstyle=\tiny
]
Trace Type: Counterexample
  -> State: 1.1 <-
    a1 = 1
    a2 = 2
    a3 = 3
    a4 = 4
    a5 = 5
    a6 = 6
    a7 = 7
    a8 = 8
  -> State: 1.2 <-
    a4 = 8
  -> State: 1.3 <-
    a3 = 10
  -> State: 1.4 <-
    a2 = 11
  -> State: 1.5 <-
    a3 = 19
  -> State: 1.6 <-
    a2 = 20
  -> State: 1.7 <-
    a3 = 28
  -> State: 1.8 <-
    a2 = 29
  -> State: 1.9 <-
    a3 = 37
  -> State: 1.10 <-
    a6 = 12
  -> State: 1.11 <-
    a7 = 20
  -> State: 1.12 <-
    a6 = 25
  -> State: 1.13 <-
    a7 = 33
  -> State: 1.14 <-
    a6 = 38
  -> State: 1.15 <-
    a7 = 46
  -> State: 1.16 <-
    a5 = 46
  -> State: 1.17 <-
    a2 = 38
  -> State: 1.18 <-
    a3 = 46
\end{lstlisting}
\end{minipage}

\end{document}