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;
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
}
18 \begin{equation
}\label{eq:
4pre
}
21 \bigwedge_{k=
2}^
{I-
1} (i_0a_i=i)\\
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
}
30 {\medmuskip=
0mu
\thinmuskip=
0mu
\thickmuskip=
0mu
33 \bigwedge_{n=
1}^
{N
}\left(
34 \bigvee_{k=
2}^
{I-
1}\left(
37 (i_na_j = i_
{n-
1}a_
{j-
1} + i_
{n-
1}a_
{j+
1})
39 \bigwedge_{j=
2}^
{I-
1}\left(
40 (j
\neq k)
\wedge (i_na_j = i_
{n-
1}a_j)
44 \bigwedge_{k=
2}^
{I-
1}(i_na_k = i_
{n-
1}a_k)
\wedge (c_i=
0)
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
}
54 \begin{equation
}\label{eq:
4pst
}
55 \bigvee_{k=
2}^
{I-
1}\left(
57 \left(
\bigvee_{j=
2}^
{I-
1}(i_Na_k=i_Na_j)
\wedge(k
\neq j)
\right)
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
}$$
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.
77 \begin{lstlisting
}[language=bash,
78 caption=
{Iteratively find the shortest solution
},label=
{listing:
4bash
}]
80 while
[ "$(python a4.py $i | yices-smt)" = "unsat"
]
88 The bold cells represent the $a_i$ after applying the function. After ten
89 iterations cell $a_2$ and $a_6$ both hold $
54$ thus satisfying the problem
92 $
\begin{array
}{c|c|ccccc
}
93 \# & i & a_2 & a_3 & a_4 & a_5 & a_6\\
95 0 & - &
2 &
3 &
4 &
5 &
6\\
96 1 &
4 &
2 &
3 &
\bm{8} &
5 &
6\\
97 2 &
5 &
2 &
3 &
8 &
\bm{14} &
6\\
98 3 &
2 &
\bm{4} &
3 &
8 &
14 &
6\\
99 4 &
4 &
4 &
3 &
\bm{17} &
14 &
6\\
100 5 &
5 &
4 &
3 &
17 &
\bm{23} &
6\\
101 6 &
6 &
4 &
3 &
17 &
23 &
\bm{30}\\
102 7 &
5 &
4 &
3 &
17 &
\bm{47} &
30\\
103 8 &
4 &
4 &
3 &
\bm{50} &
47 &
30\\
104 9 &
3 &
4 &
\bm{54} &
50 &
47 &
30\\
105 10 &
6 &
4 &
54 &
50 &
47 &
\bm{54}