+\section{Problem 1}
+{\em Three non-self-supporting villages $A$, $B$ and $C$ in the middle of
+nowhere consume one food package each per time unit. The required food packages
+are delivered by a truck, having a capacity of $300$ food packages. The
+locations of the villages are given in the following picture, in which the
+numbers indicate the distance, more precisely, the number of time units the
+truck needs to travel from one village to another, including loading or
+delivering. The truck has to pick up its food packages at location $S$
+containing an unbounded supply. The villages only have a limited capacity to
+store food packages: for $A$ and $B$ this capacity is $120$, for $C$ it is
+$200$. Initially, the truck is in $S$ and is fully loaded, and in $A$, $B$ and
+$C$ there are $40$, $30$ and $145$ food packages, respectively.}
+
+The problem can be described as a SAT problem that we can solve in SAT-solver.
+Every movement from the truck from a city to a city is called an iteration $i$
+for $i\in I$ where $I=\{0\ldots\}$. For every iteration $i$ we make variables
+$a_i, b_i, c_i, t_i, l_i, d_i$ respectively for the capacity of city $A$,
+city $B$, city $C$, the truck, the trucks location and a help variable to
+record how much food is dumped in the city. The distance between two cities is
+described with the function $dist(x, y)$. For all cities except $S$ a variable
+is defined that states the maximum capacity.
+$$a_{max}=120\wedge b_{max}=120\wedge c_{max}=200$$
+Iteration $0$ depicts the initial state and can be described with a simple
+conjuction:
+$$a_0=40\wedge b_0=30\wedge c_0=145\wedge t_0=300\wedge l_0=S\wedge d_0=0$$.
+
+After that all iteration can be formalized as
+\begin{align}
+ \bigwedge_{i\in I} \Bigg(
+ % Bent in S
+ & \Bigg[l_i=S\wedge d_i=0\wedge t_i=300\wedge
+ \bigvee_{k\in\{A,B\}}\bigg(l_{i-1}=k\wedge
+ \bigwedge_{s\in\{A,B,C\}}s_i=s_{i-1}-dist(S, k)\bigg)\Bigg]\vee\\
+ % Bent in A,B,C
+ & \bigvee_{k\in\{a,b,c\}}
+ \Bigg[l_i=k\wedge d_i>0\wedge d_i<t_{i-1}\wedge d_i<k_{max}-k_{i-1}
+ t_i=t_i-d_i\wedge k_i=k_i+d_i\wedge\\
+ & \qquad\qquad\bigwedge_{k'\in\{k\}\setminus\{S,A,B,C\}}\bigg(
+ l_{i-1}=k'\wedge
+ \bigwedge_{s\in\{k\}\setminus\{A,B,C\}}
+ s_i=s_{i-1}-dist(k, s)\bigg)\Bigg]\\
+ \nonumber\Bigg)
+\end{align}
+
+\begin{enumerate}
+ \item This part of the formula describes what happens if the truck is in
+ $S$. This is a special case of the generalized case dsecribed in $2$
+ and $3$. The truck always gets a refill in $S$ and no food is dumped.
+ The truck could either have come from $A$ or $B$ and thus the food
+ stocks of $A,B$ and $C$ will drop accordingly.
+ \item
+\end{enumerate}
+
+\begin{enumerate}[a.]
+ \item {\em Show that it is impossible to deliver food packages in such a
+ way that each of the villages consumes one food package per time unit
+ forever.}
+ \item {\em Show that this is possible if the capacity of the truck is
+ increased to 320 food packages. (Note that a finite graph contains an
+ infinite path starting in a node $v$ if and only if there is a path
+ from $v$ to a node $w$ for which there is a non-empty path from $w$ to
+ itself.)}
+ \item {\em Figure out whether it is possible if the capacity of the truck
+ is set to $318$.}
+\end{enumerate}
repositories / ar1516.git / commitdiff