From 1a16fa19517540f916d96e39c21df11559ed9be0 Mon Sep 17 00:00:00 2001
From: Peter Wu <peter@lekensteyn.nl>
Date: Wed, 14 Dec 2016 01:18:06 +0100
Subject: part1: add running time and remark for 4a, add email addresses

---
 part1.tex | 25 ++++++++++++++++++++-----
 1 file changed, 20 insertions(+), 5 deletions(-)

diff --git a/part1.tex b/part1.tex
index 232f025..1ae8d96 100644
--- a/part1.tex
+++ b/part1.tex
@@ -16,7 +16,13 @@
 \newcommand{\bimp}{\leftrightarrow}     % bi-implication
 
 \title{Assignment part 1 for Automated Reasoning 2IMF25}
-\author{Koen van der Heijden (0807929), Peter Wu (0783206)}
+\author{%
+    Peter Wu (0783206)\\
+    \texttt{s.p.wu@student.tue.nl}
+\and
+    Koen van der Heijden (0807929)\\
+    \texttt{k.p.l.v.d.heijden@student.tue.nl}
+}
 \date{\today}
 
 \begin{document}
@@ -488,9 +494,11 @@ 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}.
+\texttt{python generate-neighborsum.py 7 | z3 -smt -in} which completed within a
+fraction of a second (even for $m=20$).
+The annotated, generated input for \texttt{z3} is shown in
+Listing~\ref{lst:sumA} while the z3 output is formatted into
+Table~\ref{tbl:sumA}.
 
 \begin{table}[H]
 \centering
@@ -507,7 +515,7 @@ Listing~\ref{lst:sumA}.
  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.}
+in each step are highlighted. Indeed, $a_3=a_7=20$ after some steps.}
 \end{table}
 
 \begin{lstlisting}[
@@ -546,6 +554,13 @@ in each step are highlighted.}
 
 \end{lstlisting}
 
+\textbf{Remark}: we observed that for some larger choices of $m$ (say $m=20$),
+duplicate states (rows) occur having the same values for the variables. This can
+be explained by the conjunction used in ingredient~\ref{eq:sum2}. When the
+previous value is already the sum of the neighbors, then the new sum will be
+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)}
 
 \end{document}
-- 
cgit v1.2.1