fixed 1
[ar1516.git] / a2 / 1.tex
index 324e7d8..6de7ceb 100644 (file)
--- a/a2/1.tex
+++ b/a2/1.tex
@@ -38,18 +38,20 @@ 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. 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\\
@@ -65,10 +67,14 @@ $$const\wedge initial\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.
@@ -77,40 +83,34 @@ $$const\wedge initial\wedge
                $$
 
                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}