ar/assignment1/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,I$ where $I=7$. The
   5 following steps are defined: choose $i$ with $1<i<7$ and execute
   6 $$a_i:=a_{i-1}+a_{i+1}$$
   7 that is, $a_i$ gets the sum of the values of its
   8 neighbors and all other values remain unchanged. Show how it is possible that
   9 after a number of steps a number of steps a number $\geq 50$ occurs at least
  10 twice in $a_1; a_2; a_3; a_4; a_5; a_6; a_7$.
  11 }
  12
  13 \newpage
  14 \subsection{Formal definition}
  15 For every variable $a_i$ for $i\in I$ where $I=\{1,\ldots,7\}$ we define
  16 variables for all iterations $n$ for $n\in N$ where $N=\{1,\ldots,K\}$ for a
  17 fixed $K$ and call the $a_i^n$.
  18
  19 This leads to the following formalization where we minimize $K$.
  20
  21 \begin{align}
  22         \bigwedge_{i\in I}a_i^0=i\wedge\\
  23         \bigwedge_{n\in N}\Biggl(\bigvee_{i\in I}\Bigl(
  24                 & j\neq 0\wedge j\neq I\wedge
  25                         a_i^n=a_{i-1}^{n-1}+a_{i+1}^{n-1}\wedge\\
  26         \nonumber & \bigwedge_{j\in I}i\neq j\wedge
  27                         a_j^n=a_j^{n-1}\Bigr)\Biggr)\\
  28         \bigvee_{i\in I}\Biggl(
  29                 & a_i^N\geq50\wedge
  30                 \bigvee_{j\in I}i\neq j\wedge a_i^N=a_j^N\Biggr)
  31 \end{align}
  32
  33 Every number subformula describes either the precondition, program or
  34 postcondition.
  35 \begin{enumerate}
  36         \setcounter{enumi}{15}
  37         \item Makes sure all $a_i^0$ have the specified initial value.
  38         \item Makes sure that in one iteration zero or one of the $a_i$ becomes
  39                 the sum of its neighbors by stating in the first part that
  40                 $a_i^n=a_{i-1}^{n-1}+a_{i+1}^{n-1}$ for $i$ not being $0$ or
  41                 $I$. The second part states that all other $a_i$ stay the same.
  42         \item Makes sure that the postcondition is satisfied by stating there
  43                 are $a_i$ and $a_j$ where $i\neq j$ and $a_i^N=a_j^N$ and both
  44                 are bigger then $50$
  45 \end{enumerate}
  46
  47 \subsection{SMT format solution}
  48 The formula is easily convertable via a Python script to SMT format by literal
  49 conversion and said script is listed in Listing~\ref{listing:a4.py}. The Python
  50 script optimizes a little bit from the original formula by leaving out the
  51 $i=j$ comparison in subformula 17 and 18 by removing them from the set looped
  52 over. The script also optimizes by not checking variables $a_0^n$ and $a_I^n$
  53 since they always stay the same anyways. The minimization is done by
  54 incrementing variable $N$ every time the current $N$ yields unsat with a bash
  55 script shown in Listing~\ref{listing:4.bash}.
  56
  57 \lstinputlisting[language=bash,
  58         caption={Iteratively find the shortest solution for problem 4},
  59         label={listing:4.bash}]{src/a4.bash}
  60
  61 \subsection{Solution}
  62 The bash script finds and shows the minimal solution in which the postcondition
  63 is satisfied for $N=11$. Finding this solution takes less then $75$ seconds and
  64 is shown in Table~\ref{tab:s4}.
  65
  66 Every line in the table represents the iteration and the bold items represent
  67 the step chosen in transition between iterations.
  68 \begin{table}[H]
  69         \centering
  70         $\begin{array}{cc|ccccc}
  71                 \toprule
  72                 n & i & a_2 & a_3 & a_4 & a_5 & a_6\\
  73                 \midrule
  74                 0 & - & 2 & 3 & 4 & 5 & 6\\
  75                 1 & 4 & 2 & 3 & \mathbf{8} & 5 & 6\\
  76                 2 & 5 & 2 & 3 & 8 & \mathbf{14} & 6\\
  77                 3 & 2 & \mathbf{4} & 3 & 8 & 14 & 6\\
  78                 4 & 4 & 4 & 3 & \mathbf{17} & 14 & 6\\
  79                 5 & 5 & 4 & 3 & 17 & \mathbf{23} & 6\\
  80                 6 & 6 & 4 & 3 & 17 & 23 & \mathbf{30}\\
  81                 7 & 5 & 4 & 3 & 17 & \mathbf{47} & 30\\
  82                 8 & 4 & 4 & 3 & \mathbf{50} & 47 & 30\\
  83                 9 & 3 & 4 & \mathbf{54} & 50 & 47 & 30\\
  84                 10 & 6 & 4 & 54 & 50 & 47 & \mathbf{54}\\
  85                 \bottomrule
  86         \end{array}$
  87 \caption{Solution table for problem 4}
  88 \label{tab:s4}
  89 \end{table}