From 040dbd43cc98074d6a20e9fe66bc99485f87ea86 Mon Sep 17 00:00:00 2001 From: Peter Wu Date: Fri, 13 Jan 2017 23:13:00 +0100 Subject: FoodDelivery: adjust SMT and table output, add text for 1b --- food_delivery/food-to-table.py | 6 +-- food_delivery/generate-food.py | 11 +++--- part2.tex | 86 +++++++++++++++++++++++++++++++++++++++--- 3 files changed, 89 insertions(+), 14 deletions(-) diff --git a/food_delivery/food-to-table.py b/food_delivery/food-to-table.py index c66a774..4cb77c3 100755 --- a/food_delivery/food-to-table.py +++ b/food_delivery/food-to-table.py @@ -45,9 +45,9 @@ if False: for step, cells in enumerate(matrix): line = "%3d" % step for col, value in enumerate(cells): - if nextNodes.get(step + 1) == col: - #line += r" & \bf%2d" % value - line += r" & %4d." % value + if nextNodes.get(step) == col and col > 0: + line += r" &\bf%3d" % value + #line += r" & %4d." % value else: line += " & %5d" % value line += r" & %s \\" % "SABCD"[nextNodes[step]] diff --git a/food_delivery/generate-food.py b/food_delivery/generate-food.py index 192131b..ef9a00d 100755 --- a/food_delivery/generate-food.py +++ b/food_delivery/generate-food.py @@ -124,18 +124,17 @@ if is_b: literals += ["k0", "k1"] for k in range(1, m + 1): for j in range(1, m + 1): - if k >= j: + if j >= k: continue - jprev = j - 1 highers = " ".join([ - "(>= s{i}_{j} s{i}_{k})".format(i=i, j=j, k=k) - for i in range(1, len(states)) + "(<= s{i}_{j} s{i}_{k})".format(i=i, j=j, k=k) + for i in range(len(states)) ]) stuff += fillin([ - "(and {highers} (= l{j} l{k}) (= k0 {j}) (= k1 {k}))" + "(and (= k0 {j}) (= k1 {k}) (= l{j} l{k}) {highers})" ], vars()) - preds += ["(or %s)" % " ".join(stuff)] + preds += ["(or %s)" % "\n".join(stuff)] # Begin generator s = """(benchmark test.smt diff --git a/part2.tex b/part2.tex index 60e7ea4..d140546 100644 --- a/part2.tex +++ b/part2.tex @@ -5,6 +5,7 @@ \usepackage{epic} \usepackage{graphicx} \usepackage{gensymb} +\usepackage[table]{xcolor} \usepackage{listings} \usepackage{tikz} \usepackage{amsmath} @@ -167,13 +168,15 @@ 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. Since no satisfying assignment was found -for a route where every village can have sufficient food, we can conclude that -it is indeed impossible to deliver food packages in such a way that each of the -villages can consume one food package forever. +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 +in such a way that each of the villages can consume one food packge forever. \begin{lstlisting}[ - caption={Generated SMT program for food delivery problem (a).}, + caption={Generated SMT program for food delivery problem (a) with $m=30$.}, label={lst:food},basicstyle=\scriptsize,language=lisp ] (benchmark test.smt @@ -212,8 +215,81 @@ villages can consume one food package forever. ... )) \end{lstlisting} + \subsubsection*{(b)} +In the solution to (a) we showed that an infinite series with the previous +requirements is already impossible. When the maximum truck capacity is increased +from $capacity(T)=240$ to $capacity(T)=260$, we shall add another ingredient +to check that villages can indeed consume food forever. + +We do so by trying to find a state $k_1 \leq m$ where the stock of the truck and +the stock of each village is at least as high as a previous state $0 \leq k_0$ +at the same location: +\begin{align} +\label{eq:food8} +\bigvee_{0 \leq k_0 < k_1 \leq m} +k_0 < k_1 \land l_{k_0} = l_{k_1} \land +s_{T,k_0} \leq s_{T,k_1} +\land +\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 +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 +seconds. The resulting assignment is shown in Table~\ref{tbl:foodB}. Indeed, now +it is possible to deliver food in a way such that every village can consume food +forever. + +\begin{lstlisting}[ + caption={Generated SMT program for food delivery problem (b) with $m=13$.}, + label={lst:foodB},basicstyle=\scriptsize,language=lisp +] +(benchmark test.smt +:logic QF_UFLIA +:extrafuns ( +... +(s0_13 Int) (s1_13 Int) ... (s4_13 Int) (l13 Int) +(k0 Int) (k1 Int) +) +:formula (and +... +(or (and (= k0 1) (= k1 2) (= l1 l2) (<= s0_1 s0_2) ... (<= s4_1 s4_2)) + (and (= k0 1) (= k1 3) (= l1 l3) (<= s0_1 s0_3) ... (<= s4_1 s4_3)) + ... + (and (= k0 12) (= k1 13) (= l12 l13) (<= s0_12 s0_13) ... (<= s4_12 s4_13))) +)) +\end{lstlisting} + +\begin{table}[H] +\centering +\begin{tabular}{r|r|rrrr|c} + & \multicolumn{4}{c}{Stock at location} & \\ + $j$& T & A & B & C & D & $l_j$ \\ +\hline + 0 & 260 & 80 & 80 & 80 & 80 & S \\ + 1 & 222 &\bf103 & 65 & 65 & 65 & A \\ + 2 & 181 & 86 &\bf 89 & 48 & 48 & B \\ +\rowcolor{lightgray} + 3 & 52 & 66 & 69 & 28 &\bf157 & D \\ % PAIR + 4 & 3 & 46 & 49 &\bf 57 & 137 & C \\ + 5 & 260 & 31 & 34 & 42 & 122 & S \\ + 6 & 219 &\bf 57 & 19 & 27 & 107 & A \\ + 7 & 62 & 40 &\bf159 & 10 & 90 & B \\ + 8 & 1 & 30 & 149 &\bf 61 & 80 & C \\ + 9 & 260 & 15 & 134 & 46 & 65 & S \\ + 10 & 144 &\bf116 & 119 & 31 & 50 & A \\ + 11 & 260 & 101 & 104 & 16 & 35 & S \\ + 12 & 213 & 86 & 89 &\bf 48 & 20 & C \\ +\rowcolor{lightgray} + 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.} +\end{table} \section*{Problem: Nondeterministic finite automaton (NFA)} Let an NFA be defined as in Wikipedia \\ -- cgit v1.2.1