$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. Sub formula $(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.
+of all cities connected to city $s$. To begin with $(1)$ sets the location of
+the previous iteration correct and checks whether the city will not run out of
+food while travelled too. $(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. Sub formula $(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\\
+ \bigvee_{k'\in conn(k)} & l_i=k'\wedge k'_{i-1}\geq dist(k,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\\
\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.}
- Incrementally increasing the number of iterations does not result in a
- state where a city is without food. Therefore we try to find proof that
- the truck is actually capable of keeping all cities saturated.
-
+ Incrementally increasing the number of iterations does result in
+ finding an unsatisfiable formula with $I=21$. Thus there is no infinite
+ path that keeps the cities saturated 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 state space
that is exactly the same as some previous state. To do this we add the
following formula to the conjunction.
$$
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. The amount dumped is only shown for more readability. For state
- isomorphism it is not a factor.
+ when we have more then $10$ iterations we encounter a cycle. This is
+ shown in Table~\ref{tbl:s3b} where iteration $4$ and iteration $11$ are
+ equal.
\begin{table}[H]
\centering
\begin{tabular}{lrrrrcr}
\toprule
$I$ & $A$ & $B$ & $C$ & Truck & Location & Dump\\
\midrule
- $0$ & $40$ & $30$ & $145$ & $300$ & $S$ & $0$\\
- $1$ & $19$ & $36$ & $124$ & $273$ & $B$ & $27$\\
- \textbf{2} & \textbf{120} & \textbf{19} & \textbf{107} &
- \textbf{155} & \textbf{A} & \textbf{118}\\
- $3$ & $103$ & $117$ & $90$ & $40$ & $B$ & $115$\\
- $4$ & $82$ & $96$ & $69$ & $300$ & $S$ & $0$\\
- $5$ & $94$ & $67$ & $40$ & $259$ & $A$ & $41$\\
- $6$ & $62$ & $35$ & $194$ & $73$ & $C$ & $186$\\
- $7$ & $25$ & $69$ & $157$ & $2$ & $B$ & $71$\\
- $8$ & $4$ & $48$ & $136$ & $300$ & $S$ & $0$\\
- \textbf{9} & \textbf{120} & \textbf{19} & \textbf{107} &
- \textbf{155} & \textbf{A} & \textbf{145}\\
+ $0$ & $40$ & $30$ & $145$ & $320$ & $S$ & $0$\\
+ $1$ & $19$ & $35$ & $124$ & $294$ & $B$ & $26$\\
+ $2$ & $120$ & $18$ & $107$ & $176$ & $A$ & $118$\\
+ $3$ & $103$ & $120$ & $90$ & $57$ & $B$ & $119$\\
+ \textbf{4} & \textbf{82} & \textbf{99} & \textbf{69} &
+ \textbf{320} & \textbf{S} & \textbf{0}\\
+ $5$ & $119$ & $70$ & $40$ & $254$ & $A$ & $66$\\
+ $6$ & $87$ & $38$ & $194$ & $68$ & $C$ & $186$\\
+ $7$ & $50$ & $67$ & $157$ & $2$ & $B$ & $66$\\
+ $8$ & $29$ & $46$ & $136$ & $320$ & $S$ & $0$\\
+ $9$ & $120$ & $17$ & $107$ & $200$ & $A$ & $120$\\
+ $10$ & $103$ & $120$ & $90$ & $80$ & $B$ & $120$\\
+ \textbf{11} & \textbf{82} & \textbf{99} & \textbf{69} &
+ \textbf{320} & \textbf{S} & \textbf{0}\\
\bottomrule
\end{tabular}
+ \caption{Solution for problem $3b$}\label{tbl:s3b}
\end{table}
- \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.)}
- Solution idem to $(a)$. Just imagine the truck operator glueing $20$
- food packages to the truck which he can not deliver.
\item \emph{Figure out whether it is possible if the capacity of the truck
is set to $318$.}
- Solution idem to $(a)$. Just imagine the truck operator glueing $18$
- food packages to the truck which he can not deliver.
+
\end{enumerate}