+++ /dev/null
-\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,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 $\ge 50$ occurs at least twice in $a_1; a_2; a_3;
-a_4; a_5; a_6; a_7$.
-}
-
-\newpage
-\subsection{Formal definition}
-\paragraph{Precondition}
-Say we have $I$ $a$'s denoted as $a_i$ and we have $N$ iterations. $i_na_i$
-means variable $a_i$ in iteration $n$. Iteration $0$ is seen as the starting
-point and can be expressed as in Equation~\ref{eq:4pre}
-
-\begin{equation}\label{eq:4pre}
- (a_1=1)\wedge
- (a_I=I)\wedge
- \bigwedge_{k=2}^{I-1} (i_0a_i=i)\\
-\end{equation}
-
-\paragraph{Program}
-Every iteration we can choose to do $a_i=a_{i-1}+a_{i+1}$ or nothing. To keep
-track of what we do we keep a counter $c_n$ for every $n$ that holds either the
-$i$ if an $a_i$ is chosen or $0$ if no action has been taken. Therefore for all
-iterations we can express this as in Equation~\ref{eq:4pro}
-
-{\medmuskip=0mu \thinmuskip=0mu \thickmuskip=0mu
-\begin{equation}
-\label{eq:4pro}
- \bigwedge_{n=1}^{N}\left(
- \bigvee_{k=2}^{I-1}\left(
- (c_i = k)
- \wedge
- (i_na_j = i_{n-1}a_{j-1} + i_{n-1}a_{j+1})
- \wedge
- \bigwedge_{j=2}^{I-1}\left(
- (j\neq k)\wedge (i_na_j = i_{n-1}a_j)
- \right)
- \right)
- \vee
- \bigwedge_{k=2}^{I-1}(i_na_k = i_{n-1}a_k) \wedge (c_i=0)
- \right)
-\end{equation}
-}
-
-\paragraph{Postcondition}
-Finally the post condition can be described as $a_i>50$ and some other
-$a_i= a_j\wedge i\neq j$ for all $i$. This is expressed in
-Equation~\ref{eq:4pst}
-
-\begin{equation}\label{eq:4pst}
- \bigvee_{k=2}^{I-1}\left(
- (i_Na_k >= 50)\wedge
- \left(\bigvee_{j=2}^{I-1}(i_Na_k=i_Na_j)\wedge(k\neq j)\right)
- \right)
-\end{equation}
-
-\paragraph{Total}
-To tie this all together we just put $\wedge$ in between and that results in:
-$$\text{precondition }\wedge\text{ program }\wedge\text{ postcondition}$$
-
-\subsection{SMT format solution}
-Naming the precondition, program and postcondition respectively $p_1, p_2, p_3$
-we can easily convert it to a SMT format. The converting is tedious and takes a
-lot of time and therefore an automatization script has been created that is
-visible in the appendices in Listing~\ref{listing:4.py}. The script
-automatically assumes $11$ iterations and $7$ $a_i$ variables but via command
-line arguments this is easily extendable. To determine the minimal number of
-iterations a simple bash script can be made that iteratively increases the
-iterations as shown in Listing~\ref{listing:4bash}. The shortest solution with
-length $11$ is found in around $30$ seconds. Finding the smallest solution
-length incrementally takes around $75$ seconds.
-
-\begin{lstlisting}[language=bash,
- caption={Iteratively find the shortest solution},label={listing:4bash}]
-i=1
-while [ "$(python a4.py $i | yices-smt)" = "unsat" ]
-do
- echo $((++i));
-done
-\end{lstlisting}
-
-\subsection{Solution}
-The iterative solution terminates with $i=11$ so the minimum number of steps
-required is $11$. When we rerun the solution with $11$ steps and the
-\texttt{-m} flag we can see the solution as in Table~\ref{tab:s4}.
-The bold cells represent the $a_i$ after applying the function. After ten
-iterations cell $a_2$ and $a_6$ both hold $54$ thus satisfying the problem
-specification.
-\begin{table}[H]
- \begin{tabular}{c|c|ccccc}
- \# & $i$ & $a_2$ & $a_3$ & $a_4$ & $a_5$ & $a_6$\\
- \hline
- $0$ & - & $2$ & $3$ & $4$ & $5$ & $6$\\
- $1$ & $4$ & $2$ & $3$ & $\bm{8}$ & $5$ & $6$\\
- $2$ & $5$ & $2$ & $3$ & $8$ & $\bm{14}$ & $6$\\
- $3$ & $2$ & $\bm{4}$ & $3$ & $8$ & $14$ & $6$\\
- $4$ & $4$ & $4$ & $3$ & $\bm{17}$ & $14$ & $6$\\
- $5$ & $5$ & $4$ & $3$ & $17$ & $\bm{23}$ & $6$\\
- $6$ & $6$ & $4$ & $3$ & $17$ & $23$ & $\bm{30}$\\
- $7$ & $5$ & $4$ & $3$ & $17$ & $\bm{47}$ & $30$\\
- $8$ & $4$ & $4$ & $3$ & $\bm{50}$ & $47$ & $30$\\
- $9$ & $3$ & $4$ & $\bm{54}$ & $50$ & $47$ & $30$\\
- $10$ & $6$ & $4$ & $54$ & $50$ & $47$ & $\bm{54}$
- \end{tabular}
-\caption{Solution table for problem 4}
-\label{tab:s4}
-\end{table}
repositories / master.git / blobdiff