From fdae525c81636d257c7caef6ce75ebfec16ebe40 Mon Sep 17 00:00:00 2001 From: Peter Wu Date: Wed, 14 Dec 2016 00:46:19 +0100 Subject: NeighborSum: finished 4a Also uncommented questions (a, b, etc.) --- .../generate-neighborsum.py | 89 ++++++++++++ .../neighborsum-to-latex.py | 53 ++++++++ part1.tex | 151 ++++++++++++++++++--- 3 files changed, 274 insertions(+), 19 deletions(-) create mode 100755 integer_sum_from_neighbours/generate-neighborsum.py create mode 100755 integer_sum_from_neighbours/neighborsum-to-latex.py 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} -- cgit v1.2.1