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}$.
+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. We
-call them $\mathcal{CST}(i)$ and they are expressed as:
+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
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
+$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
repositories / ar1516.git / blobdiff