\section{Problem 4}
{\em
Seven integer variables $a_1; a_2; a_3; a_4; a_5; a_6; a_7$ are given, for
which the initial value of $a_i$ is $i$ for $i=1,\ldots,I$ where $I=7$. The
following steps are defined: choose $i$ with $1<i<7$ 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. Show how it is possible that
after a number of steps a number of steps a number $\geq 50$ occurs at least
twice in $a_1; a_2; a_3; a_4; a_5; a_6; a_7$.
}

\newpage
\subsection{Formal definition}
For every variable $a_i$ for $i\in I$ where $I=\{1,\ldots,7\}$ we define
variables for all iterations $n$ for $n\in N$ where $N=\{1,\ldots,K\}$ for a
fixed $K$ and call the $a_i^n$.

This leads to the following formalization where we minimize $K$.

\begin{align}
	\bigwedge_{i\in I}a_i^0=i\wedge\\
	\bigwedge_{n\in N}\Biggl(\bigvee_{i\in I}\Bigl( 
		& j\neq 0\wedge j\neq I\wedge
			a_i^n=a_{i-1}^{n-1}+a_{i+1}^{n-1}\wedge\\
	\nonumber & \bigwedge_{j\in I}i\neq j\wedge
			a_j^n=a_j^{n-1}\Bigr)\Biggr)\\
	\bigvee_{i\in I}\Biggl(
		& a_i^N\geq50\wedge 
		\bigvee_{j\in I}i\neq j\wedge a_i^N=a_j^N\Biggr)
\end{align}

Every number subformula describes either the precondition, program or
postcondition.
\begin{enumerate}
	\setcounter{enumi}{15}
	\item Makes sure all $a_i^0$ have the specified initial value.
	\item Makes sure that in one iteration zero or one of the $a_i$ becomes
		the sum of its neighbors by stating in the first part that
		$a_i^n=a_{i-1}^{n-1}+a_{i+1}^{n-1}$ for $i$ not being $0$ or
		$I$. The second part states that all other $a_i$ stay the same.
	\item Makes sure that the postcondition is satisfied by stating there
		are $a_i$ and $a_j$ where $i\neq j$ and $a_i^N=a_j^N$ and both
		are bigger then $50$
\end{enumerate}

\subsection{SMT format solution}
The formula is easily convertable via a Python script to SMT format by literal
conversion and said script is listed in Listing~\ref{listing:a4.bash}. The
Python script optimizes a little bit from the original formula by leaving out
the $i=j$ comparison in subformula 17 and 18 by removing them from the set
looped over. The script also optimizes by not checking variables $a_0^n$ and
$a_I^n$ since they always stay the same anyways. The minimization is done by
incrementing variable $N$ every time the current $N$ yields unsat with a bash
script shown in Listing~\ref{listing:4.bash}.

\lstinputlisting[language=bash,firstline=58,
	caption={Iteratively find the shortest solution for problem 4},
	label={listing:4.bash}]{src/a4.bash}

\subsection{Solution}
The bash script finds and shows the minimal solution in which the postcondition
is satisfied for $N=10$. Finding this solution takes less then $75$ seconds and
is shown in Table~\ref{tab:s4}.

Every line in the table represents the iteration and the bold items represent
the step chosen in transition between iterations.
\begin{table}[H]
	\centering
\input{a4.tex}
\caption{Solution table for problem 4}
\label{tab:s4}
\end{table}
