NeighborSum: add 4b (SMT soler part)

1 files changed, 42 insertions, 0 deletions

diff --git a/part1.tex b/part1.tex
index 1ae8d96..b1288e4 100644
--- a/part1.tex
+++ b/part1.tex
@@ -562,5 +562,47 @@ equal to the previous one. As the other variables remain unchanged, the whole
 state will have the same values as the previous state.
 
 \subsubsection*{(b)}
+The generic approach from (a) can be adopted for this solution with a minor
+modification. Simply replace the second ingredient by:
+\begin{align}
+\label{eq:sum2new}
+\bigvee_{s=0}^m a_{3,s} = a_{5,s} \land a_{5,s} = a_{7,s}
+\end{align}
+
+Interestingly, the runtime of the SMT solver varies. For $m=25$, a solution was
+found in 9 seconds. For $m=22$, it took 5 seconds to find one. For $m=10, 15,
+16$, no satisfying assignment was found in respectively 1, 82 and 286 seconds.
+$m=17$ is apparently the minimal satisfying solution which was found in 3.5
+seconds and shown in Table~\ref{tbl:sumB}.
+(Also interesting was that $m=18, 19, 20$ also found satisfying solutions in
+3.2, 5.9 and 3.0 seconds (in that order).)
+
+\begin{table}[H]
+\centering
+\begin{tabular}{r|rrrrrrrr}
+   & $a_1$ & $a_2$ & $a_3$ & $a_4$ & $a_5$ & $a_6$ & $a_7$ & $a_8$ \\
+\hline
+ 0 &     1 &     2 &     3 &     4 &     5 &     6 &     7 &     8 \\
+ 1 &     1 &     2 &     3 & \bf 8 &     5 &     6 &     7 &     8 \\
+ 2 &     1 &     2 &     3 &     8 &     5 & \bf12 &     7 &     8 \\
+ 3 &     1 & \bf 4 &     3 &     8 &     5 &    12 &     7 &     8 \\
+ 4 &     1 &     4 &     3 &     8 &     5 &    12 & \bf20 &     8 \\
+ 5 &     1 &     4 & \bf12 &     8 &     5 &    12 &    20 &     8 \\
+ 6 &     1 & \bf13 &    12 &     8 &     5 &    12 &    20 &     8 \\
+ 7 &     1 &    13 &    12 &     8 & \bf20 &    12 &    20 &     8 \\
+ 8 &     1 &    13 & \bf21 &     8 &    20 &    12 &    20 &     8 \\
+ 9 &     1 &    13 &    21 &     8 &    20 & \bf40 &    20 &     8 \\
+10 &     1 & \bf22 &    21 &     8 &    20 &    40 &    20 &     8 \\
+11 &     1 &    22 &    21 &     8 &    20 &    40 & \bf48 &     8 \\
+12 &     1 &    22 & \bf30 &     8 &    20 &    40 &    48 &     8 \\
+13 &     1 & \bf31 &    30 &     8 &    20 &    40 &    48 &     8 \\
+14 &     1 &    31 &    30 &     8 & \bf48 &    40 &    48 &     8 \\
+15 &     1 &    31 & \bf39 &     8 &    48 &    40 &    48 &     8 \\
+16 &     1 & \bf40 &    39 &     8 &    48 &    40 &    48 &     8 \\
+17 &     1 &    40 & \bf48 &     8 &    48 &    40 &    48 &     8 \\
+\end{tabular}
+\caption{\label{tbl:sumB}The values of each variable where the modified values
+in each step are highlighted. Indeed, $a_3=a_5=a_7=48$ after some steps.}
+\end{table}
 
 \end{document}