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
  69         \item \emph{Show that this is possible if the capacity of the truck is
  70                 increased to 320 food packages. (Note that a finite graph contains an
  71                 infinite path starting in a node $v$ if and only if there is a path
  72                 from $v$ to a node $w$ for which there is a non-empty path from $w$ to
  73                 itself.)}
  74                 To show this we need to prove that there is a state in the statespace
  75                 that is exactly the same as some previous state. To do this we add the
  76                 following formula to the conjunction.
  77                 $$\bigvee_{i\in I}\bigvee_{j\in \{0\ldots i-1\}}\left(
  78                 t_i=t_j\wedge l_i=l_j\wedge\bigwedge_{k\in V}k_i=k_j\right)
  79                 $$
  80
  81                 When we incrementally increase the number of iterations we see that
  82                 when we have more then $8$ iterations we encounter a cycle. This is
  83                 shown in the following table where iteration $2$ and iteration $9$ are
  84                 equal.
  85                 \begin{table}[H]
  86                         \centering
  87                         \begin{tabular}{ccccccc}
  88                                 \toprule
  89                                 $I$ & $A$ & $B$ & $C$ & Truck & Location & Dump\\
  90                                 \midrule
  91                                 $0$ & $40$ & $30$ & $145$ & $320$ & $0$ & $0$\\
  92                                 $1$ & $19$ & $22$ & $124$ & $307$ & $2$ & $9$\\
  93                                 $2$ & $96$ & $5$ & $107$ & $213$ & $1$ & $98$\\
  94                                 $3$ & $79$ & $119$ & $90$ & $82$ & $2$ & $133$\\
  95                                 $4$ & $58$ & $98$ & $69$ & $320$ & $0$ & $0$\\
  96                                 $5$ & $108$ & $69$ & $40$ & $241$ & $1$ & $79$\\
  97                                 $6$ & $76$ & $37$ & $194$ & $55$ & $3$ & $186$\\
  98                                 $7$ & $39$ & $55$ & $157$ & $0$ & $2$ & $53$\\
  99                                 $8$ & $18$ & $34$ & $136$ & $320$ & $0$ & $0$\\
 100                                 $9$ & $96$ & $5$ & $107$ & $213$ & $1$ & $107$\\
 101                                 \bottomrule
 102                         \end{tabular}
 103                 \end{table}
 104         \item \emph{Figure out whether it is possible if the capacity of the truck
 105                 is set to $318$.}
 106 \end{enumerate}