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 solved by transforming it to a SAT problem. Every movement
  15 from the truck from a city to a city is called an iteration $i\in I$ where
  16 $I=\{0\ldots\}$. For every iteration $i$ variables $a_i, b_i, c_i, t_i, l_i,
  17 d_i$ are created respectively for the stock of city $A$, city $B$, city $C$,
  18 the truck, the trucks location and the amount of food dumped. A function
  19 $dist(x,y)$ that returns the distance between two cities is introduced. For
  20 $A,B,C$ and the truck a variable is declared which states the maximum capacity.
  21 All the constants together is called $\mathcal{CON}$.
  22 $$a_{\max}=120\wedge b_{\max}=120\wedge c_{\max}=200\wedge t_{\max}=300$$
  23
  24 Iteration $0$ depicts the initial state and can be described with a simple
  25 conjunction called $\mathcal{INI}$.
  26 $$a_0=40\wedge b_0=30\wedge c_0=145\wedge t_0=300\wedge l_0=S\wedge d_0=0$$
  27
  28 In every iteration there are certain constraints that always have to hold and
  29 are called them $\mathcal{CST}(i)$ and expressed as:
  30 $$d_i>0\wedge
  31 d_i\leq t_{\max}\wedge
  32 t_i\geq\wedge
  33 t_i\leq t_{\max}\wedge
  34 \bigwedge_{k\in\{A,B,C\}}k_i>0$$
  35
  36 Besides the constraints the movement of the truck should be modeled. Depending
  37 on $l_{i-1}$ we want to reason about the consequences of the truck moving to
  38 $l_{i}$. The formula is called $\mathcal{TRA}$. A function $conn(s)$ is
  39 introduced that returns the set of all cities connected to city $s$. $(1)$ sets
  40 the location of the previous iteration correct and checks whether the city is
  41 reachable without running out of food. $(2)$ limits the amount of food dumped
  42 according to distance traveled, the old stock and the truck stock. When the
  43 truck is in $S$ the truck will just be filled. $(3)$ adds the dumped food to
  44 the stock of the city. $(4)$ subtracts the dumped food stock from the truck.
  45 Finally $(5)$ subtracts the distance traveled from the food stock.
  46 \begin{align}
  47         \bigvee_{k\in\{S\}\cup V}
  48                 l_{i-1}=k\wedge
  49                 \bigvee_{k'\in conn(k)} & l_i=k'\wedge k'_{i-1}\geq dist(k,k')\wedge\\
  50                         & (k'=S\wedge d_i=0)\vee(d_i\leq dist(k,k')+k'_{\max}-k'_{i-1}\wedge\\
  51                         & (k'\neq S\rightarrow k_i=k_i-dist(k,k')+d_i))\wedge\\
  52                         & (k'=S\wedge t_i=t_{\max})\vee t_i=t_{i-1}-d_i\wedge\\
  53                         & \bigwedge_{k''\in V\setminus\{k\}}
  54                                 k''_i=k''_{i-1}-dist(k,k')
  55 \end{align}
  56
  57 All the formulas tied together leads to the final formula that is satisfiable
  58 if and only if there is never a depleted city in any iteration.
  59 $$\mathcal{CON}\wedge\mathcal{INI}\wedge
  60 \bigwedge_{i\in I}\left(\mathcal{CST}(i)\wedge\mathcal{TRA}(i)\right)$$
  61
  62 \newpage
  63 \begin{enumerate}[(a)]
  64         \item \emph{Show that it is impossible to deliver food packages in such a
  65                 way that each of the villages consumes one food package per time unit
  66                 forever.}
  67                 Incrementally increasing the number of iterations does result in
  68                 finding an unsatisfiable formula with $I=21$. Thus there is no infinite
  69                 path that keeps the cities saturated.
  70         \item \emph{Show that this is possible if the capacity of the truck is
  71                 increased to 320 food packages. (Note that a finite graph contains an
  72                 infinite path starting in a node $v$ if and only if there is a path
  73                 from $v$ to a node $w$ for which there is a non-empty path from $w$ to
  74                 itself.)}
  75                 To show this we need to prove that there is a state in the state space
  76                 that is exactly the same as some previous state. To do this we add the
  77                 following formula to the conjunction.
  78                 $$\bigvee_{i\in I}\bigvee_{j\in \{0\ldots i-1\}}\left(
  79                 t_i=t_j\wedge l_i=l_j\wedge\bigwedge_{k\in V}k_i=k_j\right)
  80                 $$
  81                 Since $(c)$ is also true the solution in Table~\ref{tbl:s3c} is also
  82                 correct for a truck with size $320$.
  83         \item \emph{Figure out whether it is possible if the capacity of the truck
  84                 is set to $318$.}
  85                 When we incrementally increase the number of iterations we see that
  86                 when we have more then $10$ iterations we encounter a cycle. Changing
  87                 $t_{\max}=318$ and keeping the rest the same as in $b$ we find also
  88                 cycle after $11$ iterations as shown in Table~\ref{tbl:s3c}
  89 \end{enumerate}
  90 \begin{table}[h]
  91         \centering
  92         \begin{tabular}{lrrrrcr}
  93                 \toprule
  94                 $I$ & $A$ & $B$ & $C$ & Truck & Location & Dump\\
  95                 \midrule
  96                 $0$  & $40$  & $30$  & $145$ & $318$ & $0$ & $0$\\
  97                 $1$  & $19$  & $35$  & $124$ & $292$ & $2$ & $26$\\
  98                 $2$  & $120$ & $18$  & $107$ & $174$ & $1$ & $118$\\
  99                 $3$  & $103$ & $120$ & $90$  & $55$  & $2$ & $119$\\
 100                 \textbf{4} & \textbf{82} & \textbf{99} &
 101                         \textbf{69} & \textbf{318} & \textbf{0} & \textbf{0}\\
 102                 $5$  & $119$ & $70$  & $40$  & $252$ & $1$ & $66$\\
 103                 $6$  & $87$  & $38$  & $194$ & $66$  & $3$ & $186$\\
 104                 $7$  & $50$  & $67$  & $157$ & $0$   & $2$ & $66$\\
 105                 $8$  & $29$  & $46$  & $136$ & $318$ & $0$ & $0$\\
 106                 $9$  & $120$ & $17$  & $107$ & $198$ & $1$ & $120$\\
 107                 $10$ & $103$ & $120$ & $90$  & $78$  & $2$ & $120$\\
 108                 \textbf{11} & \textbf{82} & \textbf{99} &
 109                         \textbf{69} & \textbf{318} & \textbf{0} & \textbf{0}\\
 110                 \bottomrule
 111         \end{tabular}
 112         \caption{Solution for problem $3b$ and $3c$}\label{tbl:s3c}
 113 \end{table}