$a_i, b_i, c_i, t_i, l_i, d_i$ respectively for the capacity of city $A$,
city $B$, city $C$, the truck, the trucks location and a help variable to
record how much food is dumped in the city. The distance between two cities is
-described with the function $dist(x, y)$. For all cities except $S$ a variable
-is defined that states the maximum capacity.
-$$a_{\max}=120\wedge b_{\max}=120\wedge c_{\max}=200$$
+described with the function $dist(x, y)$. For all cities except $S$ and the
+truck a variable is defined that states the maximum capacity. We express all
+the constant values in the formula called $const$.
+$$a_{\max}=120\wedge b_{\max}=120\wedge c_{\max}=200\wedge t_{\max}=300$$
+
Iteration $0$ depicts the initial state and can be described with a simple
-conjuction:
+conjunction called $initial$.
$$a_0=40\wedge b_0=30\wedge c_0=145\wedge t_0=300\wedge l_0=S\wedge d_0=0$$
-After that all iterations can be formalized as
-$$\begin{array}{lrl}
- \bigwedge_{i\in I} \Bigg(
- % Bent in S
- & \Bigg[ & l_i=S\wedge d_i=0\wedge t_i=300\wedge\\
- & & \bigvee_{k\in\{A,B\}}
- \bigg(l_{i-1}=k\wedge
- \bigwedge_{s\in\{A,B,C\}}
- s_i=s_{i-1}-dist(S, k)\bigg)\Bigg]\vee\\
- % Bent in A,B,C
- & \bigvee_{k\in\{a,b,c\}}\Bigg[ & l_i=k\wedge\\
- & & d_i>0\wedge d_i<t_{i-1}\wedge d_i<k_{\max}-k_{i-1}\wedge\\
- & & t_i=t_{i-1}-d_i\wedge k_i=k_{i-1}+d_i\wedge\\
- & & \bigwedge_{k'\in\{k\}\setminus\{S,A,B,C\}}
- \bigg(l_{i-1}=k'\wedge
- \bigwedge_{s\in\{k\}\setminus\{A,B,C\}}
- s_i=s_{i-1}-dist(k, k')\bigg)\Bigg]\\
- & \Bigg)
-\end{array}$$
+In every iteration there are certain constraints that always have to hold. We
+call them $constraints$ and they are expressed as:
+$$d_i>0\wedge
+d_i\leq t_{\max}\wedge
+t_i\geq\wedge
+t_i\leq t_{\max}\wedge
+\bigwedge_{k\in\{A,B,C\}}k_i>0$$
-\begin{enumerate}
- \item This part of the formula describes what happens if the truck is in
- $S$. This is a special case of the generalized case dsecribed in $2$
- and $3$. The truck always gets a refill in $S$ and no food is dumped.
- The truck could either have come from $A$ or $B$ and thus the food
- stocks of $A,B$ and $C$ will drop accordingly.
- \item
-\end{enumerate}
+We reason about the new iteration $i$ from the things we know about iteration
+$i-1$. The crucial part is the location we were in iteration $i-1$ and we make
+a disjunction over all possible cities and describe the result in the following
+formula called $trans$. We introduce a function $conn(s)$ that returns the set
+of all cities connected to city $s$. $(2)$ deals with the fact that the truck
+can not dump any food in city $S$ and constraints the amount of food dumped in
+the city. $(3)$ deals with the fact that the dumped food is added to the
+current stock of the city. Subformula $(4)$ deals with the fact that if the
+truck is in $S$ it is replenished and otherwise the dumped load is subtracted
+from the trucks load. Finally $(5)$ deals with the other cities which will have
+their stock decremented with the distance traveled.
+
+\begin{align}
+ \bigvee_{k\in\{S\}\cup V}
+ l_{i-1}=k\wedge
+ \bigvee_{k'\in conn(k)} & l_i=k'\wedge\\
+ & (k'=S\wedge d_i=0)\vee(d_i\leq dist(k,k')+k'_{\max}-k'_{i-1}\wedge\\
+ & (k'\neq S\rightarrow k_i=k_i-dist(k,k')+d_i))\wedge\\
+ & (k'=S\wedge t_i=t_{\max})\vee t_i=t_{i-1}-d_i\wedge\\
+ & \bigwedge_{k''\in V\setminus\{k\}}
+ k''_i=k''_{i-1}-dist(k,k')
+\end{align}
+
+We tie all this together in one big formula that is as follows:
+$$const\wedge initial\wedge
+\bigwedge_{i\in I}\left(constraints\wedge trans\right)$$
\begin{enumerate}[a.]
\item \emph{Show that it is impossible to deliver food packages in such a
way that each of the villages consumes one food package per time unit
forever.}
+
\item \emph{Show that this is possible if the capacity of the truck is
increased to 320 food packages. (Note that a finite graph contains an
infinite path starting in a node $v$ if and only if there is a path
from $v$ to a node $w$ for which there is a non-empty path from $w$ to
itself.)}
+ To show this we need to prove that there is a state in the statespace
+ that is exactly the same as some previous state. To do this we add the
+ following formula to the conjunction.
+ $$\bigvee_{i\in I}\bigvee_{j\in \{0\ldots i-1\}}\left(
+ t_i=t_j\wedge l_i=l_j\wedge\bigwedge_{k\in V}k_i=k_j\right)
+ $$
+
+ When we incrementally increase the number of iterations we see that
+ when we have more then $8$ iterations we encounter a cycle. This is
+ shown in the following table where iteration $2$ and iteration $9$ are
+ equal.
+ \begin{table}[H]
+ \centering
+ \begin{tabular}{ccccccc}
+ \toprule
+ $I$ & $A$ & $B$ & $C$ & Truck & Location & Dump\\
+ \midrule
+ $0$ & $40$ & $30$ & $145$ & $320$ & $0$ & $0$\\
+ $1$ & $19$ & $22$ & $124$ & $307$ & $2$ & $9$\\
+ $2$ & $96$ & $5$ & $107$ & $213$ & $1$ & $98$\\
+ $3$ & $79$ & $119$ & $90$ & $82$ & $2$ & $133$\\
+ $4$ & $58$ & $98$ & $69$ & $320$ & $0$ & $0$\\
+ $5$ & $108$ & $69$ & $40$ & $241$ & $1$ & $79$\\
+ $6$ & $76$ & $37$ & $194$ & $55$ & $3$ & $186$\\
+ $7$ & $39$ & $55$ & $157$ & $0$ & $2$ & $53$\\
+ $8$ & $18$ & $34$ & $136$ & $320$ & $0$ & $0$\\
+ $9$ & $96$ & $5$ & $107$ & $213$ & $1$ & $107$\\
+ \bottomrule
+ \end{tabular}
+ \end{table}
\item \emph{Figure out whether it is possible if the capacity of the truck
is set to $318$.}
\end{enumerate}
repositories / ar1516.git / blobdiff