ar/assignments/4.tex

   1 \section{Problem 4}
   2 {\em
   3 Seven integer variables $a_1; a_2; a_3; a_4; a_5; a_6; a_7$ are given, for
   4 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
   5 $$a_i:=a_{i-1}+a_{i+1}$$
   6 that is, $a_i$ gets the sum of the values of its neighbors and all other
   7 values remain unchanged. Show how it is possible that after a number of steps
   8 a number of steps a number $\ge 50$ occurs at least twice in $a_1; a_2; a_3;
   9 a_4; a_5; a_6; a_7$.
  10 }
  11
  12 \subsection{Formal definition}
  13 \paragraph{Precondition}
  14 Say we have $I$ $a$'s denoted as $a_i$ and we have $N$ iterations. $i_na_i$
  15 means variable $a_i$ in iteration $n$. Iteration $0$ is seen as the starting
  16 point and can be expressed as in Equation~\ref{eq:4pre}
  17
  18 \begin{equation}\label{eq:4pre}
  19         (a_1=1)\wedge
  20         (a_I=I)\wedge
  21         \bigwedge_{k=2}^{I-1} (i_0a_i=i)\\
  22 \end{equation}
  23
  24 \paragraph{Program}
  25 Every iteration we can choose to do $a_i=a_{i-1}+a_{i+1}$ or nothing. To keep
  26 track of what we do we keep a counter $c_n$ for every $n$ that holds either the
  27 $i$ if an $a_i$ is chosen or $0$ if no action has been taken. Therefore for all
  28 iterations we can express this as in Equation~\ref{eq:4pro}
  29
  30 {\medmuskip=0mu \thinmuskip=0mu \thickmuskip=0mu
  31 \begin{equation}
  32 \label{eq:4pro}
  33         \bigwedge_{n=1}^{N}\left(
  34                 \bigvee_{k=2}^{I-1}\left(
  35                         (c_i = k)
  36                         \wedge
  37                         (i_na_j = i_{n-1}a_{j-1} + i_{n-1}a_{j+1})
  38                         \wedge
  39                         \bigwedge_{j=2}^{I-1}\left(
  40                                 (j\neq k)\wedge (i_na_j = i_{n-1}a_j)
  41                         \right)
  42                 \right)
  43                 \vee
  44                 \bigwedge_{k=2}^{I-1}(i_na_k = i_{n-1}a_k) \wedge (c_i=0)
  45         \right)
  46 \end{equation}
  47 }
  48
  49 \paragraph{Postcondition}
  50 Finally the post condition can be described as $a_i>50$ and some other
  51 $a_i= a_j\wedge i\neq j$ for all $i$. This is expressed in
  52 Equation~\ref{eq:4pst}
  53
  54 \begin{equation}\label{eq:4pst}
  55         \bigvee_{k=2}^{I-1}\left(
  56                 (i_Na_k >= 50)\wedge
  57                 \left(\bigvee_{j=2}^{I-1}(i_Na_k=i_Na_j)\wedge(k\neq j)\right)
  58         \right)
  59 \end{equation}
  60
  61 \paragraph{Total}
  62 To tie this all together we just put $\wedge$ in between and that results in:
  63 $$\text{precondition }\wedge\text{ program }\wedge\text{ postcondition}$$
  64
  65 \subsection{SMT format solution}
  66 Naming the precondition, program and postcondition respectively $p_1, p_2, p_3$
  67 we can easily convert it to a SMT format. The converting is tedious and takes a
  68 lot of time and therefore an automatization script has been created that is
  69 visible in the appendices in Listing~\ref{listing:4.py}. The script
  70 automatically assumes $11$ iterations and $7$ $a_i$ variables but via command
  71 line arguments this is easily extendable. To determine the minimal number of
  72 iterations a simple bash script can be made that iteratively increases the
  73 iterations as shown in Listing~\ref{listing:4bash}. The shortest solution with
  74 length $11$ is found in around $30$ seconds. Finding the smallest solution
  75 length incrementally takes around $75$ seconds.
  76
  77 \begin{lstlisting}[language=bash,
  78         caption={Iteratively find the shortest solution},label={listing:4bash}]
  79 i=1
  80 while [ "$(python a4.py $i | yices-smt)" = "unsat" ]
  81 do
  82         echo $((++i));
  83 done
  84 \end{lstlisting}
  85
  86 \subsection{Solution}
  87 The iterative solution terminates with $i=11$ so the minimum number of steps
  88 required is $11$. When we rerun the solution with $11$ steps and the
  89 \texttt{-m} flag we can see the solution as in Table~\ref{tab:s4}.
  90 The bold cells represent the $a_i$ after applying the function. After ten
  91 iterations cell $a_2$ and $a_6$ both hold $54$ thus satisfying the problem
  92 specification.
  93 \begin{table}[H]
  94         \begin{tabular}{c|c|ccccc}
  95                 \# & $i$ & $a_2$ & $a_3$ & $a_4$ & $a_5$ & $a_6$\\
  96                 \hline
  97                 $0$ & - & $2$ & $3$ & $4$ & $5$ & $6$\\
  98                 $1$ & $4$ & $2$ & $3$ & $\bm{8}$ & $5$ & $6$\\
  99                 $2$ & $5$ & $2$ & $3$ & $8$ & $\bm{14}$ & $6$\\
 100                 $3$ & $2$ & $\bm{4}$ & $3$ & $8$ & $14$ & $6$\\
 101                 $4$ & $4$ & $4$ & $3$ & $\bm{17}$ & $14$ & $6$\\
 102                 $5$ & $5$ & $4$ & $3$ & $17$ & $\bm{23}$ & $6$\\
 103                 $6$ & $6$ & $4$ & $3$ & $17$ & $23$ & $\bm{30}$\\
 104                 $7$ & $5$ & $4$ & $3$ & $17$ & $\bm{47}$ & $30$\\
 105                 $8$ & $4$ & $4$ & $3$ & $\bm{50}$ & $47$ & $30$\\
 106                 $9$ & $3$ & $4$ & $\bm{54}$ & $50$ & $47$ & $30$\\
 107                 $10$ & $6$ & $4$ & $54$ & $50$ & $47$ & $\bm{54}$
 108         \end{tabular}
 109 \caption{Solution table for problem 4}
 110 \label{tab:s4}
 111 \end{table}