From 7b61d1db9459b60f403538716c30bc8fa7fd284c Mon Sep 17 00:00:00 2001
From: Peter Wu <peter@lekensteyn.nl>
Date: Fri, 13 Jan 2017 23:51:08 +0100
Subject: Grammar and readability improvements

---
 part2.tex | 22 +++++++++++-----------
 1 file changed, 11 insertions(+), 11 deletions(-)

(limited to 'part2.tex')

diff --git a/part2.tex b/part2.tex
index c9e0082..50296f2 100644
--- a/part2.tex
+++ b/part2.tex
@@ -160,19 +160,19 @@ y = S \implies
 s_{T,j} = capacity(T)
 \end{align}
 
-With the given definitions path travelling costs $cost$, the truck and villages
-$V$ (and their capacities $capacity$) we are able to build the route that the
-truck travels, parameterized under the $m$ (the number of visited locations).
+With the given path travelling costs $cost$, truck and villages $V$ and their
+capacities $capacity$, we are able to build the route that the truck travels,
+parameterized by the number of visited locations $m$.
 We wrote a generator program in Python that outputs a SMT corresponding to
 conjunction of the above ingredients (mapping $V=\{S,A,B,C,D\}$ to the indices
 $0,1,2,3,4$), this is shown in Listing~\ref{lst:food}.
 
 We picked (arbitrary) $m=30$ and applied Z3 to the generated SMT which resulted
 in \texttt{unsat} after four seconds. Then we applied binary search and found
-that for $m=22$ the output would still be \texttt{unsat} (after four seconds)
-while for $m=21$ a solution was found within a second. This shows that a valid
-route can be obtained where 21 locations are visited, but that no route exists
-that passes through 22 locations. It is thus impossible to deliver food packages
+that for $m=22$ the output is still \texttt{unsat} (after four seconds)
+while for $m=21$ a solution is found within a second. This shows that a valid
+route with 21 visited locations can be obtained and that no route exists such
+that 22 locations are visited. It is thus impossible to deliver food packages
 in such a way that each of the villages can consume one food packge forever.
 
 \begin{lstlisting}[
@@ -228,7 +228,7 @@ s_{T,k_0} \leq s_{T,k_1}
 \bigwedge_{i \in V'} s_{i,k_0} \leq s_{i,k_1}
 \end{align}
 
-The SMT output by the augmented generator program includes two new variables and
+The SMT output generated by the augmented program includes two new variables and
 adds Part~\ref{eq:food8} to the conjunction as shown in Listing~\ref{lst:foodB}.
 For $m=12$ we obtained \texttt{unsat} after 9 seconds (showing that a loop was
 not yet obtained) while for $m=13$ a satisfying assignment was found in 10
@@ -276,9 +276,9 @@ forever.
  13 &    56 &    66 &    69 &    28 &\bf157 & D \\ % PAIR
 \end{tabular}
 \caption{\label{tbl:foodB}The solution calculated by z3 for $m=13$, showing the
-initial and following states (truck and village stock and current location
-$l_j$) after $j$ transitions. State $j=13$ has higher stocks than state $j=13$
-at location D.}
+initial and following states (consisting of truck and village stock and current
+location $l_j$) after $j$ transitions. State $j=13$ has greater or equal stocks
+than state $j=13$ at location D.}
 \end{table}
 
 \section*{Problem: Nondeterministic finite automaton (NFA)}
-- 
cgit v1.2.1

