a2/1.tex

   1 \section{Problem 1}
   2 \emph{Three non-self-supporting villages $A$, $B$ and $C$ in the middle of
   3 nowhere consume one food package each per time unit. The required food packages
   4 are delivered by a truck, having a capacity of $300$ food packages. The
   5 locations of the villages are given in the following picture, in which the
   6 numbers indicate the distance, more precisely, the number of time units the
   7 truck needs to travel from one village to another, including loading or
   8 delivering. The truck has to pick up its food packages at location $S$
   9 containing an unbounded supply. The villages only have a limited capacity to
  10 store food packages: for $A$ and $B$ this capacity is $120$, for $C$ it is
  11 $200$. Initially, the truck is in $S$ and is fully loaded, and in $A$, $B$ and
  12 $C$ there are $40$, $30$ and $145$ food packages, respectively.}
  13
  14 The problem can be described as a SAT problem that we can solve in SAT-solver.
  15 Every movement from the truck from a city to a city is called an iteration $i$
  16 for $i\in I$ where $I=\{0\ldots\}$. For every iteration $i$ we make variables
  17 $a_i, b_i, c_i, t_i, l_i, d_i$ respectively for the capacity of city $A$,
  18 city $B$, city $C$, the truck, the trucks location and a help variable to
  19 record how much food is dumped in the city. The distance between two cities is
  20 described with the function $dist(x, y)$. For all cities except $S$ and the
  21 truck a variable is defined that states the maximum capacity. We express all
  22 the constant values in the formula called $const$.
  23 $$a_{\max}=120\wedge b_{\max}=120\wedge c_{\max}=200\wedge t_{\max}=300$$
  24
  25 Iteration $0$ depicts the initial state and can be described with a simple
  26 conjunction called $initial$.
  27 $$a_0=40\wedge b_0=30\wedge c_0=145\wedge t_0=300\wedge l_0=S\wedge d_0=0$$
  28
  29 In every iteration there are certain constraints that always have to hold. We
  30 call them $constraints$ and they are expressed as:
  31 $$d_i>0\wedge
  32 d_i\leq t_{\max}\wedge
  33 t_i\geq\wedge
  34 t_i\leq t_{\max}\wedge
  35 \bigwedge_{k\in\{A,B,C\}}k_i>0$$
  36
  37 We reason about the new iteration $i$ from the things we know about iteration
  38 $i-1$. The crucial part is the location we were in iteration $i-1$ and we make
  39 a disjunction over all possible cities and describe the result in the following
  40 formula called $trans$. We introduce a function $conn(s)$ that returns the set
  41 of all cities connected to city $s$. $(2)$ deals with the fact that the truck
  42 can not dump any food in city $S$ and constraints the amount of food dumped in
  43 the city. $(3)$ deals with the fact that the dumped food is added to the
  44 current stock of the city. Subformula $(4)$ deals with the fact that if the
  45 truck is in $S$ it is replenished and otherwise the dumped load is subtracted
  46 from the trucks load. Finally $(5)$ deals with the other cities which will have
  47 their stock decremented with the distance traveled.
  48
  49 \begin{align}
  50         \bigvee_{k\in\{S\}\cup V}
  51                 l_{i-1}=k\wedge
  52                 \bigvee_{k'\in conn(k)} & l_i=k'\wedge\\
  53                         & (k'=S\wedge d_i=0)\vee(d_i\leq dist(k,k')+k'_{\max}-k'_{i-1}\wedge\\
  54                         & (k'\neq S\rightarrow k_i=k_i-dist(k,k')+d_i))\wedge\\
  55                         & (k'=S\wedge t_i=t_{\max})\vee t_i=t_{i-1}-d_i\wedge\\
  56                         & \bigwedge_{k''\in V\setminus\{k\}}
  57                                 k''_i=k''_{i-1}-dist(k,k')
  58 \end{align}
  59
  60 We tie all this together in one big formula that is as follows:
  61 $$const\wedge initial\wedge
  62 \bigwedge_{i\in I}\left(constraints\wedge trans\right)$$
  63
  64 \begin{enumerate}[a.]
  65         \item \emph{Show that it is impossible to deliver food packages in such a
  66                 way that each of the villages consumes one food package per time unit
  67                 forever.}
  68                 Incrementally increasing the number of iterations does not result in a
  69                 state where a city is without food. Therefore we try to find proof that
  70                 the truck is actually capable of keeping all cities saturated.
  71
  72                 To show this we need to prove that there is a state in the statespace
  73                 that is exactly the same as some previous state. To do this we add the
  74                 following formula to the conjunction.
  75                 $$\bigvee_{i\in I}\bigvee_{j\in \{0\ldots i-1\}}\left(
  76                 t_i=t_j\wedge l_i=l_j\wedge\bigwedge_{k\in V}k_i=k_j\right)
  77                 $$
  78
  79                 When we incrementally increase the number of iterations we see that
  80                 when we have more then $8$ iterations we encounter a cycle. This is
  81                 shown in the following table where iteration $2$ and iteration $9$ are
  82                 equal. The amount dumped is only shown for more readability. For state
  83                 isomorphism it is not a factor.
  84                 \begin{table}[H]
  85                         \centering
  86                         \begin{tabular}{lrrrrcr}
  87                                 \toprule
  88                                 $I$ & $A$ & $B$ & $C$ & Truck & Location & Dump\\
  89                                 \midrule
  90                                 $0$ & $40$  & $30$  & $145$ & $300$ & $S$ & $0$\\
  91                                 $1$ & $19$  & $36$  & $124$ & $273$ & $B$ & $27$\\
  92                                 \textbf{2} & \textbf{120} & \textbf{19}  & \textbf{107} &
  93                                         \textbf{155} & \textbf{A} & \textbf{118}\\
  94                                 $3$ & $103$ & $117$ & $90$  & $40$  & $B$ & $115$\\
  95                                 $4$ & $82$  & $96$  & $69$  & $300$ & $S$ & $0$\\
  96                                 $5$ & $94$  & $67$  & $40$  & $259$ & $A$ & $41$\\
  97                                 $6$ & $62$  & $35$  & $194$ & $73$  & $C$ & $186$\\
  98                                 $7$ & $25$  & $69$  & $157$ & $2$   & $B$ & $71$\\
  99                                 $8$ & $4$   & $48$  & $136$ & $300$ & $S$ & $0$\\
 100                                 \textbf{9} & \textbf{120} & \textbf{19}  & \textbf{107} &
 101                                         \textbf{155} & \textbf{A} & \textbf{145}\\
 102                                 \bottomrule
 103                         \end{tabular}
 104                 \end{table}
 105         \item \emph{Show that this is possible if the capacity of the truck is
 106                 increased to 320 food packages. (Note that a finite graph contains an
 107                 infinite path starting in a node $v$ if and only if there is a path
 108                 from $v$ to a node $w$ for which there is a non-empty path from $w$ to
 109                 itself.)}
 110                 Solution idem to $a.$. Just imagine the truck operator glueing $20$
 111                 food packages to the truck which he can not deliver.
 112         \item \emph{Figure out whether it is possible if the capacity of the truck
 113                 is set to $318$.}
 114                 Solution idem to $a.$. Just imagine the truck operator glueing $18$
 115                 food packages to the truck which he can not deliver.
 116 \end{enumerate}