-\paragraph{Problem 4}
-
+\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
+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_4; a_5; a_6; a_7$.
}
-\paragraph{Solution}
-Say we have $I$ $a$'s denoted as $a_i$ and we have $N$ iterations.
-For every $a_i$ in every iteration we make a variable $i_na_i$ where $n$ is the
-number of the iteration. For $a_0$ and $a_7$ we can make an exception since
-they do not change over iterations. For documenting purposes we also keep a counter
-variable $c_n$ for every $n$th iteration. This leads in the initial state
-expressed by:
-
-$$
-\left(c_0=0\right)\wedge
-\left(a_1=1\right)\wedge
-\left(a_I=I\right)\wedge
-\bigwedge_{k=2}^{I-1} \left(i_0a_i = i\right)
-$$
-
-Every next iteration we only increment one $i$ from $2,\ldots,6$.
-
-Say we want to check if the state is reachable in $N$ iterations. Then we can
-specifiy postconditions. For every $i$ we specify this:
-$$\bigvee_{k=2}^{I-1}\left(
- \left(i_Na_k >= 50\right)\wedge\left(
- \bigvee_{j=2}^{I-1}\left(i_Na_k=i_Na_j\right)\wedge
- \left(k\neq j\right)
+\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)
-\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
+ i=$((i+1))
+ echo $i;
+done
+\end{lstlisting}
+\subsection{Solution}
+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{center}
$\begin{array}{c|c|ccccc}
\# & i & a_2 & a_3 & a_4 & a_5 & a_6\\
\hline
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}\\
+ 10 & 6 & 4 & 54 & 50 & 47 & \bm{54}
\end{array}$
+\end{center}
repositories / master.git / commitdiff