\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 generalized this problem to fitting pallets into $T$ trucks, with capacity $c_T$ and maximum amount of pallets $p_T$. Then we added variables $N$, $P$, $C$, $S$ and $D$ representing Nuzzles, Prittles, Crottles, Skipples and Dupples respectively.
The size of $P$ is to be determined.
To put a constraint on the capacity of a truck, we created the following formula:\\
$\sum_{x \in X} (ite (x \in T) (weight(x)) (0))$, where $X \in {N, P, C, S, D}$.\\ We summed the result for all $X$, and compared it to $c_T$.
We did exactly the same for the amount of pallets, where we substituted $weight(x)$ with $1$, and $c_T$ with $p_T$.
After this, we added the static constraints that $s \in S$ must be in truck $1$, $2$ or $3$ as these are our cooling trucks.
Finally we added a constraint saying all $n \in N$ are distinct.

Since we have $8$ trucks, with maximum amount of pallets $8$, we can carry at most $64$ pallets. This means that we can carry at most $22$ pallets of prittles. We searched for the solution of how many pallets we could actually carry in a binary sense: First we tried $11$ pallets, then $16$, then $19$, $21$ and finally $22$. These tries were all satisfiable, thus we can carry at most $22$ pallets of prittles.

\subsubsection*{(b)}
For part b of the assignment, we added a set of constraints saying that whenever a truck contains a pallet of Crottles, it may not contain a pallet of Prittles.
This was captured by a set of constraints looping over all pallets of Crottles, and then for the Truck containing them, looping over all pallets to check whether they are not Prittles (giving us at most $10 \cdot 8 = 80$ new constraints). 
After that, we again searched for a solution in a binary way. This time, we did not get a satisfiable solution anymore above 19 pallets of Prittles. Thus, we can take at most 19 pallets of Prittles if they may not be carried together with Crottles.

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

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