From 7b61d1db9459b60f403538716c30bc8fa7fd284c Mon Sep 17 00:00:00 2001 From: Peter Wu 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