a1/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 \subsection{Formal definition}
  14 For every variable $a_i$ for $i\in I$ where $I=\{1,\ldots,7\}$ we define
  15 variables for all iterations $n$ for $n\in N$ where $N=\{1,\ldots,K\}$ for a
  16 fixed $K$ and call the $a_i^n$.
  17
  18 This leads to the following formalization where we minimize $K$.
  19
  20 \begin{align}
  21         \bigwedge_{i\in I}a_i^0=i\wedge\\
  22         \bigwedge_{n\in N}\Biggl(\bigvee_{i\in I}\Bigl(
  23                 & j\neq 0\wedge j\neq I\wedge
  24                         a_i^n=a_{i-1}^{n-1}+a_{i+1}^{n-1}\wedge\\
  25         \nonumber & \bigwedge_{j\in I}i\neq j\wedge
  26                         a_j^n=a_j^{n-1}\Bigr)\Biggr)\\
  27         \bigvee_{i\in I}\Biggl(
  28                 & a_i^N\geq50\wedge
  29                 \bigvee_{j\in I}i\neq j\wedge a_i^N=a_j^N\Biggr)
  30 \end{align}
  31
  32 Every number subformula describes either the precondition, program or
  33 postcondition.
  34 \begin{enumerate}
  35         \setcounter{enumi}{15}
  36         \item Makes sure all $a_i^0$ have the specified initial value.
  37         \item Makes sure that in one iteration zero or one of the $a_i$ becomes
  38                 the sum of its neighbors by stating in the first part that
  39                 $a_i^n=a_{i-1}^{n-1}+a_{i+1}^{n-1}$ for $i$ not being $0$ or
  40                 $I$. The second part states that all other $a_i$ stay the same.
  41         \item Makes sure that the postcondition is satisfied by stating there
  42                 are $a_i$ and $a_j$ where $i\neq j$ and $a_i^N=a_j^N$ and both
  43                 are bigger then $50$
  44 \end{enumerate}
  45
  46 \subsection{SMT format solution}
  47 The formula is easily convertable via a Python script to SMT format by literal
  48 conversion. The script optimizes a little bit from the original formula by
  49 leaving out the $i=j$ comparison in subformula 17 and 18 by removing them from
  50 the set looped over. The script also optimizes by not checking variables
  51 $a_0^n$ and $a_I^n$ since they always stay the same anyways. The minimization
  52 is done by incrementing variable $N$ every time the current $N$ yields unsat
  53 with a bash script shown in Listing~\ref{listing:4.bash}.
  54
  55 \lstinputlisting[language=bash,firstline=58,
  56         caption={Iteratively find the shortest solution for problem 4},
  57         label={listing:4.bash}]{src/a4.bash}
  58
  59 \subsection{Solution}
  60 The bash script finds and shows the minimal solution in which the postcondition
  61 is satisfied for $N=10$. Finding this solution takes less then $20$ seconds and
  62 is shown in Table~\ref{tab:s4}.
  63
  64 Every line in the table represents the iteration and the bold items represent
  65 the step chosen in transition between iterations.
  66 \begin{table}[H]
  67         \centering
  68 \input{a4.tex}
  69 \caption{Solution table for problem 4}
  70 \label{tab:s4}
  71 \end{table}