\section{Problem 1}
\emph{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 solved by transforming it to a SAT problem. Every movement
from the truck from a city to a city is called an iteration $i\in I$ where 
$I=\{0\ldots\}$. For every iteration $i$ variables $a_i, b_i, c_i, t_i, l_i,
d_i$ are created respectively for the stock of city $A$, city $B$, city $C$,
the truck, the trucks location and the amount of food dumped. A function
$dist(x,y)$ that returns the distance between two cities is introduced. For
$A,B,C$ and the truck a variable is declared which states the maximum capacity.
All the constants together is called $\mathcal{CON}$.
$$a_{\max}=120\wedge b_{\max}=120\wedge c_{\max}=200\wedge t_{\max}=300$$

Iteration $0$ depicts the initial state and can be described with a simple
conjunction called $\mathcal{INI}$.
$$a_0=40\wedge b_0=30\wedge c_0=145\wedge t_0=300\wedge l_0=S\wedge d_0=0$$

In every iteration there are certain constraints that always have to hold and
are called them $\mathcal{CST}(i)$ and expressed as:
$$d_i>0\wedge 
d_i\leq t_{\max}\wedge
t_i\geq\wedge 
t_i\leq t_{\max}\wedge
\bigwedge_{k\in\{A,B,C\}}k_i>0$$

Besides the constraints the movement of the truck should be modeled. Depending
on $l_{i-1}$ we want to reason about the consequences of the truck moving to
$l_{i}$. The formula is called $\mathcal{TRA}$. A function $conn(s)$ is
introduced that returns the set of all cities connected to city $s$. $(1)$ sets
the location of the previous iteration correct and checks whether the city is
reachable without running out of food. $(2)$ limits the amount of food dumped
according to distance traveled, the old stock and the truck stock. When the
truck is in $S$ the truck will just be filled. $(3)$ adds the dumped food to
the stock of the city. $(4)$ subtracts the dumped food stock from the truck.
Finally $(5)$ subtracts the distance traveled from the food stock.
\begin{align}
	\bigvee_{k\in\{S\}\cup V}
		l_{i-1}=k\wedge
		\bigvee_{k'\in conn(k)} & l_i=k'\wedge k'_{i-1}\geq dist(k,k')\wedge\\
			& (k'=S\wedge d_i=0)\vee(d_i\leq dist(k,k')+k'_{\max}-k'_{i-1}\wedge\\
			& (k'\neq S\rightarrow k_i=k_i-dist(k,k')+d_i))\wedge\\
			& (k'=S\wedge t_i=t_{\max})\vee t_i=t_{i-1}-d_i\wedge\\
			& \bigwedge_{k''\in V\setminus\{k\}}
				k''_i=k''_{i-1}-dist(k,k')
\end{align}

All the formulas tied together leads to the final formula that is satisfiable
if and only if there is never a depleted city in any iteration.
$$\mathcal{CON}\wedge\mathcal{INI}\wedge
\bigwedge_{i\in I}\left(\mathcal{CST}(i)\wedge\mathcal{TRA}(i)\right)$$

\newpage
\begin{enumerate}[(a)]
	\item \emph{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.}
		Incrementally increasing the number of iterations does result in
		finding an unsatisfiable formula with $I=21$. Thus there is no infinite
		path that keeps the cities saturated.
	\item \emph{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.)}
		To show this we need to prove that there is a state in the state space
		that is exactly the same as some previous state. To do this we add the
		following formula to the conjunction.
		$$\bigvee_{i\in I}\bigvee_{j\in \{0\ldots i-1\}}\left(
		t_i=t_j\wedge l_i=l_j\wedge\bigwedge_{k\in V}k_i=k_j\right)
		$$
		Since $(c)$ is also true the solution in Table~\ref{tbl:s3c} is also
		correct for a truck with size $320$.
	\item \emph{Figure out whether it is possible if the capacity of the truck
		is set to $318$.}
		When we incrementally increase the number of iterations we see that
		when we have more then $10$ iterations we encounter a cycle. Changing
		$t_{\max}=318$ and keeping the rest the same as in $b$ we find also
		cycle after $11$ iterations as shown in Table~\ref{tbl:s3c}
\end{enumerate}
\begin{table}[h]
	\centering
	\begin{tabular}{lrrrrcr}
		\toprule
		$I$ & $A$ & $B$ & $C$ & Truck & Location & Dump\\
		\midrule
		$0$  & $40$  & $30$  & $145$ & $318$ & $0$ & $0$\\
		$1$  & $19$  & $35$  & $124$ & $292$ & $2$ & $26$\\
		$2$  & $120$ & $18$  & $107$ & $174$ & $1$ & $118$\\
		$3$  & $103$ & $120$ & $90$  & $55$  & $2$ & $119$\\
		\textbf{4} & \textbf{82} & \textbf{99} & 
			\textbf{69} & \textbf{318} & \textbf{0} & \textbf{0}\\
		$5$  & $119$ & $70$  & $40$  & $252$ & $1$ & $66$\\
		$6$  & $87$  & $38$  & $194$ & $66$  & $3$ & $186$\\
		$7$  & $50$  & $67$  & $157$ & $0$   & $2$ & $66$\\
		$8$  & $29$  & $46$  & $136$ & $318$ & $0$ & $0$\\
		$9$  & $120$ & $17$  & $107$ & $198$ & $1$ & $120$\\
		$10$ & $103$ & $120$ & $90$  & $78$  & $2$ & $120$\\
		\textbf{11} & \textbf{82} & \textbf{99} &
			\textbf{69} & \textbf{318} & \textbf{0} & \textbf{0}\\
		\bottomrule
	\end{tabular}
	\caption{Solution for problem $3b$ and $3c$}\label{tbl:s3c}
\end{table}
