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.bash}. The
  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} and visualized with the python
  56 script shown in Listing~\ref{listing:a4.py}.
  57
  58 \lstinputlisting[language=bash,firstline=58,
  59         caption={Iteratively find the shortest solution for problem 4},
  60         label={listing:4.bash}]{src/a4.bash}
  61
  62 \subsection{Solution}
  63 The bash script finds and shows the minimal solution in which the postcondition
  64 is satisfied for $N=10$. Finding this solution takes less then $20$ seconds and
  65 is shown in Table~\ref{tab:s4}.
  66
  67 Every line in the table represents the iteration and the bold items represent
  68 the step chosen in transition between iterations.
  69 \begin{table}[H]
  70         \centering
  71 \input{a4.tex}
  72 \caption{Solution table for problem 4}
  73 \label{tab:s4}
  74 \end{table}