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.}
+$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$ and the
-truck a variable is defined that states the maximum capacity. We express all
-the constant values in the formula called $const$.
+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 createde respectively for the stock of city $A$, city $B$, city $C$,
+the truck, the trucks location and the amount of food dumped. We introduce a
+function $dist(x,y)$ that returns the distance between two cities. 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 $initial$.
+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. We
-call them $constraints$ and they are expressed as:
+call them $\mathcal{CST}(i)$ and they are 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$$
-We reason about the new iteration $i$ from the things we know about iteration
-$i-1$. The crucial part is the location we were in iteration $i-1$ and we make
-a disjunction over all possible cities and describe the result in the following
-formula called $trans$. We introduce a function $conn(s)$ that returns the set
-of all cities connected to city $s$. To begin with $(1)$ sets the location of
-the previous iteration correct and checks whether the city will not run out of
-food while travelled too. $(2)$ deals with the fact that the truck can not dump
-any food in city $S$ and constraints the amount of food dumped in the city.
-$(3)$ deals with the fact that the dumped food is added to the current stock of
-the city. Sub formula $(4)$ deals with the fact that if the truck is in $S$ it
-is replenished and otherwise the dumped load is subtracted from the trucks
-load. Finally $(5)$ deals with the other cities which will have their stock
-decremented with the distance traveled.
-
+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}$. We introduce a function
+$conn(s)$ 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
k''_i=k''_{i-1}-dist(k,k')
\end{align}
-We tie all this together in one big formula that is as follows:
-$$const\wedge initial\wedge
-\bigwedge_{i\in I}\left(constraints\wedge trans\right)$$
+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 forever.
+ 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
$$\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)
$$
-
- When we incrementally increase the number of iterations we see that
- when we have more then $10$ iterations we encounter a cycle. This is
- shown in Table~\ref{tbl:s3b} where iteration $4$ and iteration $11$ are
- equal.
- \begin{table}[H]
- \centering
- \begin{tabular}{lrrrrcr}
- \toprule
- $I$ & $A$ & $B$ & $C$ & Truck & Location & Dump\\
- \midrule
- $0$ & $40$ & $30$ & $145$ & $320$ & $S$ & $0$\\
- $1$ & $19$ & $35$ & $124$ & $294$ & $B$ & $26$\\
- $2$ & $120$ & $18$ & $107$ & $176$ & $A$ & $118$\\
- $3$ & $103$ & $120$ & $90$ & $57$ & $B$ & $119$\\
- \textbf{4} & \textbf{82} & \textbf{99} & \textbf{69} &
- \textbf{320} & \textbf{S} & \textbf{0}\\
- $5$ & $119$ & $70$ & $40$ & $254$ & $A$ & $66$\\
- $6$ & $87$ & $38$ & $194$ & $68$ & $C$ & $186$\\
- $7$ & $50$ & $67$ & $157$ & $2$ & $B$ & $66$\\
- $8$ & $29$ & $46$ & $136$ & $320$ & $S$ & $0$\\
- $9$ & $120$ & $17$ & $107$ & $200$ & $A$ & $120$\\
- $10$ & $103$ & $120$ & $90$ & $80$ & $B$ & $120$\\
- \textbf{11} & \textbf{82} & \textbf{99} & \textbf{69} &
- \textbf{320} & \textbf{S} & \textbf{0}\\
- \bottomrule
- \end{tabular}
- \caption{Solution for problem $3b$}\label{tbl:s3b}
- \end{table}
+ 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}
repositories / ar1516.git / blobdiff