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$ a variable
  21 is defined that states the maximum capacity.
  22 $$a_{\max}=120\wedge b_{\max}=120\wedge c_{\max}=200$$
  23 Iteration $0$ depicts the initial state and can be described with a simple
  24 conjuction:
  25 $$a_0=40\wedge b_0=30\wedge c_0=145\wedge t_0=300\wedge l_0=S\wedge d_0=0$$
  26
  27 After that all iteration can be formalized as
  28 $$\begin{array}{lrl}
  29         \bigwedge_{i\in I} \Bigg(
  30         % Bent in S
  31         & \Bigg[ & l_i=S\wedge d_i=0\wedge t_i=300\wedge\\
  32         & & \bigvee_{k\in\{A,B\}}
  33                 \bigg(l_{i-1}=k\wedge
  34                 \bigwedge_{s\in\{A,B,C\}}
  35                         s_i=s_{i-1}-dist(S, k)\bigg)\Bigg]\vee\\
  36         % Bent in A,B,C
  37         & \bigvee_{k\in\{a,b,c\}}\Bigg[ & l_i=k\wedge\\
  38         & & d_i>0\wedge d_i<t_{i-1}\wedge d_i<k_{\max}-k_{i-1}\wedge\\
  39         & & t_i=t_{i-1}-d_i\wedge k_i=k_{i-1}+d_i\wedge\\
  40         & & \bigwedge_{k'\in\{k\}\setminus\{S,A,B,C\}}
  41                 \bigg(l_{i-1}=k'\wedge
  42                 \bigwedge_{s\in\{k\}\setminus\{A,B,C\}}
  43                         s_i=s_{i-1}-dist(k, k')\bigg)\Bigg]\\
  44         & \Bigg)
  45 \end{array}$$
  46
  47 \begin{enumerate}
  48         \item This part of the formula describes what happens if the truck is in
  49                 $S$. This is a special case of the generalized case dsecribed in $2$
  50                 and $3$. The truck always gets a refill in $S$ and no food is dumped.
  51                 The truck could either have come from $A$ or $B$ and thus the food
  52                 stocks of $A,B$ and $C$ will drop accordingly.
  53         \item
  54 \end{enumerate}
  55
  56 \begin{enumerate}[a.]
  57         \item \emph{Show that it is impossible to deliver food packages in such a
  58                 way that each of the villages consumes one food package per time unit
  59                 forever.}
  60         \item \emph{Show that this is possible if the capacity of the truck is
  61                 increased to 320 food packages. (Note that a finite graph contains an
  62                 infinite path starting in a node $v$ if and only if there is a path
  63                 from $v$ to a node $w$ for which there is a non-empty path from $w$ to
  64                 itself.)}
  65         \item \emph{Figure out whether it is possible if the capacity of the truck
  66                 is set to $318$.}
  67 \end{enumerate}