NeighborSum: finished 4a

Also uncommented questions (a, b, etc.)

3 files changed, 274 insertions, 19 deletions

diff --git a/integer_sum_from_neighbours/generate-neighborsum.py b/integer_sum_from_neighbours/generate-neighborsum.py
new file mode 100755
index 0000000..7e06e02
--- /dev/null
+++ b/integer_sum_from_neighbours/generate-neighborsum.py
@@ -0,0 +1,89 @@
+#!/usr/bin/env python
+import sys
+
+# i = 1..8
+n = 8
+steps = int(sys.argv[1])
+
+literals = []
+preds = []
+
+def fillin(cases, template_vars):
+    if type(cases) == str:
+        return cases.format(**template_vars)
+    return [template.format(**template_vars) for template in cases]
+
+# a. Repeat a number of steps, check in each step
+# if a_3 = a_7 is possible in that step.
+# Number a_i in step s is encoded as a_i_s.
+# The initial state is a_i_0.
+for step in range(steps + 1):
+    for i in range(1, n + 1):
+        literals += ["a{i}_{step}".format(**vars())]
+
+# Initial state, a_i_0 = i
+for i in range(1, n + 1):
+    preds += ["(= a{i}_0 {i})".format(i=i)]
+
+# Goal: have a_3 = a_7 in any step:
+preds += [
+    "(or %s)" % " ".join("(= a3_{i} a7_{i})".format(i=i)
+    for i in range(steps + 1))
+]
+
+# In each step, can sum neighbors (leaving others unchanged).
+for step in range(1, steps + 1):
+    # The first and last one cannot be changed. In a step, one can choose to
+    # change a_i for any i, leaving all other j (i != j) intact.
+    altpreds = []
+    for i in range(2, n):
+        laststep = step - 1
+        prev = i - 1
+        next = i + 1
+
+        # Require a'_i = a_{i-1} + a_{i+1}
+        statepreds = fillin([
+            "(= a{i}_{step} (+ a{prev}_{laststep} a{next}_{laststep}))"
+        ], vars())
+
+        # Require a'_j = a_j for i != j
+        for j in range(1, n + 1):
+            if i == j:
+                continue
+            statepreds += fillin([
+                "(= a{j}_{step} a{j}_{laststep})"
+            ], vars())
+        # All assignments must apply for this step.
+        altpreds += [
+            "(and %s)" % "\n".join(statepreds)
+        ]
+    preds += [
+        "(or",
+        "%s" % "\n".join(altpreds),
+        ")"
+    ]
+
+
+# Begin generator
+s = """(benchmark test.smt
+:logic QF_UFLIA
+:extrafuns (
+"""
+s += "\n".join("(%s Int)" % x for x in literals)
+s += """
+)
+:formula (and
+"""
+s += "\n".join(preds)
+s += """
+))
+"""
+
+try:
+    import sys
+    print(s)
+    # Hack to avoid printing a ugly error in case stdin of next pipe is closed.
+    sys.stdout.flush()
+    sys.stdout.close()
+except BrokenPipeError:
+    pass
diff --git a/integer_sum_from_neighbours/neighborsum-to-latex.py b/integer_sum_from_neighbours/neighborsum-to-latex.py
new file mode 100755
index 0000000..a920d9d
--- /dev/null
+++ b/integer_sum_from_neighbours/neighborsum-to-latex.py
@@ -0,0 +1,53 @@
+#!/usr/bin/env python3
+import re
+import sys
+
+# Maximum number of elements
+n = 8
+
+matrix = []
+
+for line in sys.stdin:
+    line = line.strip()
+    if line == "unsat":
+        sys.exit('unsat!')
+    if line == "sat":
+        continue
+    m = re.match(r'a(\d+)_(\d+) -> (\d+)', line)
+    var_number, step, value = map(int, m.groups())
+
+    # auto-detect size, extending matrix size if necessary.
+    while len(matrix) <= step:
+        matrix.append([None] * n)
+
+    matrix[step][var_number - 1] = value
+
+# List of cells that have changed since the previous iteration. Note that the
+# first row has no changed cell and therefore stores "None"
+changedCells = [None]
+for i, cells in enumerate(matrix):
+    if i == 0:
+        continue # skip first row
+    previousRow = matrix[i - 1]
+    for col, prevValue in enumerate(previousRow):
+        if cells[col] != prevValue:
+            # Found changed cell!
+            changedCells.append(col)
+            break
+
+line = "  "
+for col in range(len(matrix[0])):
+    line += " & $a_%d$" % (col + 1)
+line += r" \\"
+print(line)
+print(r"\hline")
+
+for step, cells in enumerate(matrix):
+    line = "%2d" % step
+    for col, value in enumerate(cells):
+        if changedCells[step] == col:
+            line += r" & \bf%2d" % value
+        else:
+            line += " & %5d" % value
+    line += r" \\"
+    print(line)
diff --git a/part1.tex b/part1.tex
index 6944205..232f025 100644
--- a/part1.tex
+++ b/part1.tex
@@ -42,12 +42,13 @@ skipples.
 Nuzzles are very valuable: to distribute the risk of loss no two pallets of nuzzles may
 be in the same truck.
 
-% (a) Investigate what is the maximum number of pallets of prittles that can be delivered,
-% and show how for that number all pallets may be divided over the eight trucks.
-% and show how for that number all pallets may be divided over the eight trucks.
-
-% (b) Do the same, with the extra information that prittles and crottles are an explosive
-% combination: they are not allowed to be put in the same truck.
+\begin{itemize}
+\item[(a)] Investigate what is the maximum number of pallets of prittles that
+can be delivered, and show how for that number all pallets may be divided over
+the eight trucks.
+\item[(b)] Do the same, with the extra information that prittles and crottles
+are an explosive combination: they are not allowed to be put in the same truck.
+\end{itemize}
 
 \subsection*{Solution:}
 \subsubsection*{(a)}
@@ -239,13 +240,13 @@ then we have to check pairs that we have not seen yet:
 \bigwedge_{0 \leq i < m}
 \bigwedge_{i < j < m}
 cx_i \geq& cx_j + powerDistance \lor
-cx_j \geq cx_i + powerDistance \lor \\
+cx_j \geq cx_i + powerDistance \lor \nonumber \\
 cy_i \geq& cy_j + powerDistance \lor
 cy_j \geq cy_i + powerDistance
 \end{align}
 
 We wrote a generator program that takes the conjunction of the above parts
-(formulae \ref{eq:chip1}, \ref{eq:chip2}, \ref{eq:chip3}, \ref{eq:chip4},
+(ingredients \ref{eq:chip1}, \ref{eq:chip2}, \ref{eq:chip3}, \ref{eq:chip4} and
 \ref{eq:chip5}). Its annotated (partial) output is shown in
 Listing~\ref{lst:chipDesign}. Evaluation of this output using
 \texttt{python generate-chipdesign.py | z3 -smt -in} finished in 12 seconds.
@@ -339,12 +340,13 @@ Twelve jobs numbered from 1 to 12 have to be executed satisfying the following r
 no two of these jobs may run at the same time.
 \end{itemize}
 
-% (a) Find a solution of this scheduling problem for which the total running time is
-% minimal.
-
-% (b) Do the same with the extra requirement that job 6 and job 12 need a resource of
-% limited availability, by which job 6 may only run during the 17 time units in which
-% job 12 is running.
+\begin{itemize}
+\item[(a)] Find a solution of this scheduling problem for which the total
+    running time is minimal.
+\item[(b)] Do the same with the extra requirement that job 6 and job 12 need a
+    resource of limited availability, by which job 6 may only run during the 17
+    time units in which job 12 is running.
+\end{itemize}
 
 \subsection*{Solution:}
 \subsubsection*{(a)}
@@ -423,16 +425,127 @@ are given, for which the initial value of
 $a_i$ is $i$ for $i = 1$, \ldots, 8. The following steps are defined: choose $i$
 with $1 < i < 8$ and execute
 \[
-    a_i := a_{i-1} + a_i+1,
+    a_i := a_{i-1} + a_{i+1},
 \]
 that is, $a_i$ gets the sum of the values of its neighbors and all other values remain
 unchanged.
 
-% (a) Show how it is possible that $a_3 = a_7$ after a number of steps.
-
-% (b) Show how it is possible that $a_3 = a_5 = a_7$ after a number of steps.
-% For this problem both try to use an SMT solver and NuSMV, and discuss how they perform.
+\begin{itemize}
+\item[(a)] Show how it is possible that $a_3 = a_7$ after a number of steps.
+\item[(b)] Show how it is possible that $a_3 = a_5 = a_7$ after a number of steps.
+For this problem both try to use an SMT solver and NuSMV, and discuss how they perform.
+\end{itemize}
 
 \subsection*{Solution:}
+\subsubsection*{(a)}
+We generalize this problem to $n$ variables $a_1, a_2, \ldots, a_n$. Let
+$a_{i,0}$ denote the variables $a_i$ in the initial state.
+Let $m$ denote the number of steps we need to reach the desired configuration
+(this is the value we have to find out).
+Let $a_{i,s}$ denote the variables $a_i$ after $1 \leq s \leq m$ steps.
+
+A sketch of the solution will involve $n \times (1 + m)$ literals ($n$ in the
+initial state, $n \times m$ after $m$ steps). The formula will consist of a
+conjunction of the initial states, transition relations and an ingredient
+describing the desired configuration.
+
+(Note that the given change ($a_{i,s} = a_{i-1,s-1} + a_{i+1,s-1}$ for $1 < i <
+n$ and $1 \leq s \leq m$) will always keep the first and last values unchanged
+throughout the execution. So only one $a_1$ and $a_n$ would be sufficient. For
+symmetry with all other variables, and to allow for arbitrary other changes in a
+step, we have decided to keep this though.)
+
+The ingredient to model the initial state:
+\begin{align}
+\label{eq:sum1}
+\bigwedge_{i=1}^n a_{i,0} = i
+\end{align}
+
+Next, we try to reach the goal of finding $a_3=a_7$ in any state:
+\begin{align}
+\label{eq:sum2}
+\bigvee_{s=0}^m a_{3,s} = a_{7,s}
+\end{align}
+Technically we can start with $s=1$ instead of $s=0$ since the values in the
+initial state are all unique. We chose to keep it though such that the solution
+can be generalized for arbitrary values in the initial state.
+
+Finally we add the transition relations for each step $1 \leq s \leq m$ (reached
+from the previous step $s-1$). In each transition, one variable $1 < i < n$ will
+be changed to match the (previous) values of the neighbors while all others are
+unchanged from the previous state:
+\begin{align}
+\label{eq:sum3}
+\bigwedge_{s=1}^m
+\bigvee_{i=2}^{n-1} (
+a_{i,s} = a_{i-1,s-1} + a_{i+1,s-1} \land
+\bigwedge_{1 \leq j \leq n, i \neq j} a_{j,s} = a_{j,s-1}
+)
+\end{align}
+
+The conjunction of ingredients \ref{eq:sum1}, \ref{eq:sum2} and \ref{eq:sum3}
+form the formula that is parameterized by $n$ and $m$. For our problem, $n=8$ so
+we have to find $m$. At first we picked $m=20$ (arbitrary) and then narrowed
+down $m$ using a binary search. In the end we found that $m=7$ is the minimum
+solution. The resulting assignment was obtained using the command
+\texttt{python generate-neighborsum.py 7 | z3 -smt -in} and is summarized in
+Table~\ref{tbl:sumA}. The annotated, generated input for \texttt{z3} is shown in
+Listing~\ref{lst:sumA}.
+
+\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 & \bf 6 &     4 &     5 &     6 &     7 &     8 \\
+ 2 &     1 &     2 &     6 & \bf11 &     5 &     6 &     7 &     8 \\
+ 3 &     1 &     2 & \bf13 &    11 &     5 &     6 &     7 &     8 \\
+ 4 &     1 &     2 &    13 & \bf18 &     5 &     6 &     7 &     8 \\
+ 5 &     1 &     2 &    13 &    18 &     5 & \bf12 &     7 &     8 \\
+ 6 &     1 &     2 &    13 &    18 &     5 &    12 & \bf20 &     8 \\
+ 7 &     1 &     2 & \bf20 &    18 &     5 &    12 &    20 &     8 \\
+\end{tabular}
+\caption{\label{tbl:sumA}The values of each variable where the modified values
+in each step are highlighted.}
+\end{table}
+
+\begin{lstlisting}[
+    caption={Generated SMT output for $n=8, m=7$ that satisfies $a_3=a_7$},
+    label={lst:sumA},language=lisp,basicstyle=\scriptsize
+]
+(benchmark test.smt
+:logic QF_UFLIA
+:extrafuns (
+(a1_0 Int) ...  (a8_0 Int)
+...
+(a1_7 Int) ...  (a8_7 Int)
+)
+:formula (and
+(= a1_0 1) ...  (= a8_0 8)
+; trying to reach the goal in each state
+(or (= a3_0 a7_0) ... (= a3_7 a7_7))
+; in each state, one of the n-2=6 values must change,
+; while leaving the others unchanged from the previous state.
+(or
+  (and (= a2_1 (+ a1_0 a3_0))
+       (= a1_1 a1_0) ...  (= a8_1 a8_0))
+  ...
+  (and (= a7_1 (+ a6_0 a8_0))
+       (= a1_1 a1_0) ...  (= a8_1 a8_0))
+)
+...
+(or
+  (and (= a2_7 (+ a1_6 a3_6))
+       (= a1_7 a1_6) ...  (= a8_7 a8_6))
+  ...
+  (and (= a7_7 (+ a6_6 a8_6))
+       (= a1_7 a1_6) ...  (= a8_7 a8_6))
+  )
+))
+
+\end{lstlisting}
+
+\subsubsection*{(b)}
 
 \end{document}