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 bold cells represent the $a_i$ after applying the function. After ten
  88 iterations cell $a_2$ and $a_6$ both hold $54$ thus satisfying the problem
  89 specification.
  90 \begin{center}
  91 $\begin{array}{c|c|ccccc}
  92         \# & i & a_2 & a_3 & a_4 & a_5 & a_6\\
  93         \hline
  94         0 & - & 2 & 3 & 4 & 5 & 6\\
  95         1 & 4 & 2 & 3 & \bm{8} & 5 & 6\\
  96         2 & 5 & 2 & 3 & 8 & \bm{14} & 6\\
  97         3 & 2 & \bm{4} & 3 & 8 & 14 & 6\\
  98         4 & 4 & 4 & 3 & \bm{17} & 14 & 6\\
  99         5 & 5 & 4 & 3 & 17 & \bm{23} & 6\\
 100         6 & 6 & 4 & 3 & 17 & 23 & \bm{30}\\
 101         7 & 5 & 4 & 3 & 17 & \bm{47} & 30\\
 102         8 & 4 & 4 & 3 & \bm{50} & 47 & 30\\
 103         9 & 3 & 4 & \bm{54} & 50 & 47 & 30\\
 104         10 & 6 & 4 & 54 & 50 & 47 & \bm{54}
 105 \end{array}$
 106 \end{center}