diff options
author | Peter Wu <peter@lekensteyn.nl> | 2017-01-13 23:51:08 +0100 |
---|---|---|
committer | Peter Wu <peter@lekensteyn.nl> | 2017-01-13 23:51:08 +0100 |
commit | 7b61d1db9459b60f403538716c30bc8fa7fd284c (patch) | |
tree | 4a93d75ac83bef8d53f9a07e03f9dd3e4b078c34 /part2.tex | |
parent | 614dda5057dde417247110064361c5e91cd59954 (diff) | |
download | 2IMF25-AR-7b61d1db9459b60f403538716c30bc8fa7fd284c.tar.gz |
Grammar and readability improvements
Diffstat (limited to 'part2.tex')
-rw-r--r-- | part2.tex | 22 |
1 files changed, 11 insertions, 11 deletions
@@ -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)} |