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$. To begin with $(1)$ sets the location of
  42 the previous iteration correct and checks whether the city will not run out of
  43 food while travelled too. $(2)$ deals with the fact that the truck can not dump
  44 any food in city $S$ and constraints the amount of food dumped in the city.
  45 $(3)$ deals with the fact that the dumped food is added to the current stock of
  46 the city. Sub formula $(4)$ deals with the fact that if the truck is in $S$ it
  47 is replenished and otherwise the dumped load is subtracted from the trucks
  48 load. Finally $(5)$ deals with the other cities which will have their stock
  49 decremented with the distance traveled.
  50
  51 \begin{align}
  52         \bigvee_{k\in\{S\}\cup V}
  53                 l_{i-1}=k\wedge
  54                 \bigvee_{k'\in conn(k)} & l_i=k'\wedge k'_{i-1}\geq dist(k,k')\wedge\\
  55                         & (k'=S\wedge d_i=0)\vee(d_i\leq dist(k,k')+k'_{\max}-k'_{i-1}\wedge\\
  56                         & (k'\neq S\rightarrow k_i=k_i-dist(k,k')+d_i))\wedge\\
  57                         & (k'=S\wedge t_i=t_{\max})\vee t_i=t_{i-1}-d_i\wedge\\
  58                         & \bigwedge_{k''\in V\setminus\{k\}}
  59                                 k''_i=k''_{i-1}-dist(k,k')
  60 \end{align}
  61
  62 We tie all this together in one big formula that is as follows:
  63 $$const\wedge initial\wedge
  64 \bigwedge_{i\in I}\left(constraints\wedge trans\right)$$
  65
  66 \begin{enumerate}[(a)]
  67         \item \emph{Show that it is impossible to deliver food packages in such a
  68                 way that each of the villages consumes one food package per time unit
  69                 forever.}
  70                 Incrementally increasing the number of iterations does result in
  71                 finding an unsatisfiable formula with $I=21$. Thus there is no infinite
  72                 path that keeps the cities saturated forever.
  73         \item \emph{Show that this is possible if the capacity of the truck is
  74                 increased to 320 food packages. (Note that a finite graph contains an
  75                 infinite path starting in a node $v$ if and only if there is a path
  76                 from $v$ to a node $w$ for which there is a non-empty path from $w$ to
  77                 itself.)}
  78                 To show this we need to prove that there is a state in the state space
  79                 that is exactly the same as some previous state. To do this we add the
  80                 following formula to the conjunction.
  81                 $$\bigvee_{i\in I}\bigvee_{j\in \{0\ldots i-1\}}\left(
  82                 t_i=t_j\wedge l_i=l_j\wedge\bigwedge_{k\in V}k_i=k_j\right)
  83                 $$
  84
  85                 When we incrementally increase the number of iterations we see that
  86                 when we have more then $10$ iterations we encounter a cycle. This is
  87                 shown in Table~\ref{tbl:s3b} where iteration $4$ and iteration $11$ are
  88                 equal.
  89                 \begin{table}[H]
  90                         \centering
  91                         \begin{tabular}{lrrrrcr}
  92                                 \toprule
  93                                 $I$ & $A$ & $B$ & $C$ & Truck & Location & Dump\\
  94                                 \midrule
  95                                 $0$ &  $40$  & $30$  & $145$ & $320$ & $S$ & $0$\\
  96                                 $1$ &  $19$  & $35$  & $124$ & $294$ & $B$ & $26$\\
  97                                 $2$ &  $120$ & $18$  & $107$ & $176$ & $A$ & $118$\\
  98                                 $3$ &  $103$ & $120$ & $90$  & $57$  & $B$ & $119$\\
  99                                 \textbf{4} & \textbf{82} & \textbf{99} & \textbf{69} &
 100                                         \textbf{320} & \textbf{S} & \textbf{0}\\
 101                                 $5$ &  $119$ & $70$  & $40$  & $254$ & $A$ & $66$\\
 102                                 $6$ &  $87$  & $38$  & $194$ & $68$  & $C$ & $186$\\
 103                                 $7$ &  $50$  & $67$  & $157$ & $2$   & $B$ & $66$\\
 104                                 $8$ &  $29$  & $46$  & $136$ & $320$ & $S$ & $0$\\
 105                                 $9$ &  $120$ & $17$  & $107$ & $200$ & $A$ & $120$\\
 106                                 $10$ & $103$ & $120$ & $90$  & $80$  & $B$ & $120$\\
 107                                 \textbf{11} & \textbf{82} & \textbf{99} & \textbf{69} &
 108                                         \textbf{320} & \textbf{S} & \textbf{0}\\
 109                                 \bottomrule
 110                         \end{tabular}
 111                         \caption{Solution for problem $3b$}\label{tbl:s3b}
 112                 \end{table}
 113         \item \emph{Figure out whether it is possible if the capacity of the truck
 114                 is set to $318$.}
 115
 116 \end{enumerate}