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$.
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$.
19 This leads to the following formalization where we minimize $K$.
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(
30 \bigvee_{j
\in I
}i
\neq j
\wedge a_i^N=a_j^N
\Biggr)
33 Every number subformula describes either the precondition, program or
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
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 Python script optimizes a little bit from the original formula by leaving out
51 the $i=j$ comparison in subformula
17 and
18 by removing them from the set
52 looped over. The script also optimizes by not checking variables $a_0^n$ and
53 $a_I^n$ 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
}.
58 \lstinputlisting[language=bash,firstline=
58,
59 caption=
{Iteratively find the shortest solution for problem
4},
60 label=
{listing:
4.bash
}]{src/a4.bash
}
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
}.
67 Every line in the table represents the iteration and the bold items represent
68 the step chosen in transition between iterations.
72 \caption{Solution table for problem
4}