summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorPeter Wu <peter@lekensteyn.nl>2017-01-13 23:13:00 +0100
committerPeter Wu <peter@lekensteyn.nl>2017-01-13 23:13:00 +0100
commit040dbd43cc98074d6a20e9fe66bc99485f87ea86 (patch)
tree16b1b4cde5882e46125c602d96daaac698baf512
parent2b84767d5b493bde658b443637b8733cfaf57a34 (diff)
download2IMF25-AR-040dbd43cc98074d6a20e9fe66bc99485f87ea86.tar.gz
FoodDelivery: adjust SMT and table output, add text for 1b
-rwxr-xr-xfood_delivery/food-to-table.py6
-rwxr-xr-xfood_delivery/generate-food.py11
-rw-r--r--part2.tex86
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 \\