From bf2a8c20aa1e7c82c01c07f5f1b087986a59aba5 Mon Sep 17 00:00:00 2001
From: Peter Wu <peter@lekensteyn.nl>
Date: Fri, 13 Jan 2017 16:42:13 +0100
Subject: FoodDelivery: initial text

---
 part2.tex | 138 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 138 insertions(+)

(limited to 'part2.tex')

diff --git a/part2.tex b/part2.tex
index c7c6acf..60e7ea4 100644
--- a/part2.tex
+++ b/part2.tex
@@ -73,7 +73,145 @@ which there is a non-empty path from $w$ to itself.)
 
 \subsection*{Solution:}
 \subsubsection*{(a)}
+We generalize the problem as a graph $G=(V,E)$ where the vertices $V$ represent
+villages and the supply location (denoted $S$) and edges $E$ represent the paths
+between the vertices. We also define a weight function $cost : E \to
+\mathbb{N}$. For brevity, we denote the villages (without the supply location)
+by $V'=V \setminus \{S\}$.
+The process of transporting and delivering food packages is modelled as state
+transitions. The state after $0 \leq j \leq m$ steps consists of:
+\begin{itemize}
+\item Current location of truck: $l_j \in V$.
+\item Remaining food stock at village $i \in V'$, denoted by $s_{i,j}$.
+\item Remaining food stock in truck, denoted by $s_{T,j}$.
+\end{itemize}
 
+The truck (denoted as $T$) and villages have maximum capacities, let these be
+defined by the function $capacity : (V' \cup \{T\}) \to \mathbb{N}$.
+With these definitions in place, let us define the initial state for the
+specific scenario where the truck starts at the supply location:
+\begin{align}
+\label{eq:food1}
+l_0 = S
+\land \bigwedge_{i \in V'} s_{i,0} = 80
+\land s_{T,0} = capacity(T)
+\end{align}
+
+Now require that the truck capacity never drops below zero and that villages
+always have some food to consume and are never overstocked:
+\begin{align}
+\label{eq:food2}
+\bigwedge_{j=0}^m
+0 \leq s_{T,j}
+\land
+\bigwedge_{i \in V' } 0 \leq s_{i,j} \leq capacity(i)
+\end{align}
+
+Finally we add the constraints for state transitions. At every state, any of
+the enabled transitions can be taken (if this is not possible for any state,
+then indeed it is impossible to deliver food packages in such a way without
+starving some villages).
+We add ingredients to express:
+\begin{itemize}
+\item Part~\ref{eq:food3}:
+whether the target is reachable from the previous location.
+\item Part~\ref{eq:food4}:
+whether the village has sufficient food for consumption while the truck travels.
+\item Part~\ref{eq:food5}:
+villages (other than the target) eat some food (but are not restocked).
+Note that this covers all villages if the next target is the supply location, so
+the village stock $s_{i,j}$ is always defined.
+\item Part~\ref{eq:food6}:
+if target is village, eat some and optionally restock the village (as long as
+the truck has some stock). For brevity, we define $drop(j) = s_{T,j-1} -
+s_{T,j}$, expressing how much food is unloaded from the truck and dropped into
+the village.
+\item Part~\ref{eq:food7}:
+if target is supply location, the truck is always fully restocked. (This and the
+previous part ensures that $s_{T,j}$ is always defined.)
+\end{itemize}
+\begin{align}
+\label{eq:food3}
+\bigwedge_{j=1}^m
+\bigvee_{(x, y) \in E}
+&(l_{j-1}, l_j) = (x, y)
+%
+\\\label{eq:food4}
+&\land
+\bigwedge_{i \in V'} s_{i,j-1} \geq cost(x, y)
+%
+\\\label{eq:food5}
+&\land
+\bigwedge_{i \in V', i \neq y}
+s_{i,j} = s_{i,j-1} - cost(x, y)
+%
+\\\label{eq:food6}
+&\land
+y \neq S \implies
+    (s_{i,j} = s_{i,j-1} - cost(x, y) + drop(j)
+    \land
+    drop(j) \geq 0
+    )
+%
+\\\label{eq:food7}
+&\land
+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).
+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. 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.
+
+\begin{lstlisting}[
+    caption={Generated SMT program for food delivery problem (a).},
+    label={lst:food},basicstyle=\scriptsize,language=lisp
+]
+(benchmark test.smt
+:logic QF_UFLIA
+:extrafuns (
+(s0_0 Int) (s1_0 Int) ... (s4_0 Int) (l0 Int)
+...
+(s0_30 Int) (s1_30 Int) ... (s4_30 Int) (l30 Int)
+)
+:formula (and
+(= l0 0)
+(= s1_0 80) (= s2_0 80) (= s3_0 80) (= s4_0 80)
+(= s0_0 240)
+(>= s0_0 0)
+(>= s1_0 0) (<= s1_0 120) (>= s2_0 0) (<= s2_0 160)
+(>= s3_0 0) (<= s3_0 100) (>= s4_0 0) (<= s4_0 160)
+...
+(or
+  (and (= l0 0) (= l1 1)
+       (>= s1_0 15) (>= s2_0 15) (>= s3_0 15) (>= s4_0 15)
+       (>= (- s0_0 s0_1) 0)
+       (= s1_1 (+ (- s1_0 15) (- s0_0 s0_1)))
+       (= s2_1 (- s2_0 15))
+       (= s3_1 (- s3_0 15))
+       (= s4_1 (- s4_0 15)))
+  ...
+  (and (= l0 1) (= l1 0)
+       (>= s1_0 15) (>= s2_0 15) (>= s3_0 15) (>= s4_0 15)
+       (= s1_1 (- s1_0 15))
+       (= s2_1 (- s2_0 15))
+       (= s3_1 (- s3_0 15))
+       (= s4_1 (- s4_0 15))
+       (= s0_1 240))
+  ...
+)
+...
+))
+\end{lstlisting}
 \subsubsection*{(b)}
 
 
-- 
cgit v1.2.1