NeighborSum: add 4b (SMT soler part)

3 files changed, 57 insertions, 1 deletions

diff --git a/integer_sum_from_neighbours/generate-neighborsum.py b/integer_sum_from_neighbours/generate-neighborsum.py
index 7e06e02..14a8d23 100755
--- a/integer_sum_from_neighbours/generate-neighborsum.py
+++ b/integer_sum_from_neighbours/generate-neighborsum.py
@@ -1,9 +1,14 @@
 #!/usr/bin/env python
+# Usage for 4a (where 7 is the number of steps to run):
+#   $0 7 | z3 -smt -in
+# Usage for 4b:
+#   $0 7 b | z3 -smt -in
 import sys
 
 # i = 1..8
 n = 8
 steps = int(sys.argv[1])
+is_b = len(sys.argv) >= 3 and sys.argv[2] == 'b'
 
 literals = []
 preds = []
@@ -26,8 +31,12 @@ for i in range(1, n + 1):
     preds += ["(= a{i}_0 {i})".format(i=i)]
 
 # Goal: have a_3 = a_7 in any step:
+if not is_b:
+    goal = "(= a3_{i} a7_{i})"
+else:
+    goal = "(and (= a3_{i} a5_{i}) (= a5_{i} a7_{i}))"
 preds += [
-    "(or %s)" % " ".join("(= a3_{i} a7_{i})".format(i=i)
+    "(or %s)" % " ".join(goal.format(i=i)
     for i in range(steps + 1))
 ]
 
diff --git a/integer_sum_from_neighbours/neighborsum-to-latex.py b/integer_sum_from_neighbours/neighborsum-to-latex.py
index a920d9d..3fb3daa 100755
--- a/integer_sum_from_neighbours/neighborsum-to-latex.py
+++ b/integer_sum_from_neighbours/neighborsum-to-latex.py
@@ -34,6 +34,9 @@ for i, cells in enumerate(matrix):
             # Found changed cell!
             changedCells.append(col)
             break
+    else:
+        # Should not happen! Something got stuck?
+        changedCells.append(None)
 
 line = "  "
 for col in range(len(matrix[0])):
@@ -50,4 +53,6 @@ for step, cells in enumerate(matrix):
         else:
             line += " & %5d" % value
     line += r" \\"
+    if step > 0 and changedCells[step] is None:
+        line += " % unchanged!"
     print(line)
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}