summaryrefslogtreecommitdiff
path: root/part2.tex
diff options
context:
space:
mode:
authorPeter Wu <peter@lekensteyn.nl>2017-01-13 23:51:08 +0100
committerPeter Wu <peter@lekensteyn.nl>2017-01-13 23:51:08 +0100
commit7b61d1db9459b60f403538716c30bc8fa7fd284c (patch)
tree4a93d75ac83bef8d53f9a07e03f9dd3e4b078c34 /part2.tex
parent614dda5057dde417247110064361c5e91cd59954 (diff)
download2IMF25-AR-7b61d1db9459b60f403538716c30bc8fa7fd284c.tar.gz
Grammar and readability improvements
Diffstat (limited to 'part2.tex')
-rw-r--r--part2.tex22
1 files changed, 11 insertions, 11 deletions
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)}