done with 1

diff --git a/a2/1.tex b/a2/1.tex
index 11692f6..8aeb788 100644 (file)
--- a/a2/1.tex
+++ b/a2/1.tex
@@ -65,12 +65,10 @@ $$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.
 
-       \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.
@@ -81,26 +79,38 @@ $$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.
+               equal. The amount dumped is only shown for more readability. For state
+               isomorphism it is not a factor.
                \begin{table}[H]
                        \centering
-                       \begin{tabular}{ccccccc}
+                       \begin{tabular}{lrrrrcr}
                                \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$\\
+                               $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}\\
                                \bottomrule
                        \end{tabular}
                \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}

diff --git a/a2/src/1a.bash b/a2/src/1a.bash
index 1724514..f157243 100755 (executable)
--- a/a2/src/1a.bash
+++ b/a2/src/1a.bash
@@ -160,7 +160,7 @@ GEN
        echo ")))"
 }
 it=1
-while generate $it 318 | $YICES -m | pee sort "grep -q unsat"
+while generate $it 300 | $YICES -m | pee sort "grep -q unsat"
 do
        echo $((it++))
 done