From: Mart Lubbers Date: Tue, 5 Jan 2016 17:57:58 +0000 (+0100) Subject: spellcheck X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=00f818b82ceb225ef29e33a147408159b56f18e9;p=ar1516.git spellcheck --- diff --git a/a2/1.tex b/a2/1.tex index 61dc95d..c9a7625 100644 --- a/a2/1.tex +++ b/a2/1.tex @@ -14,19 +14,19 @@ $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 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 @@ -35,8 +35,8 @@ t_i\leq t_{\max}\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 diff --git a/a2/2.tex b/a2/2.tex index f490d0d..aa88a8a 100644 --- a/a2/2.tex +++ b/a2/2.tex @@ -38,7 +38,7 @@ next state is not defined for a bottle $b_i$ we assume $next(b_i)=b_i$. $next(b_j)=b_j+\min(b_{j\max}-b_j, b_i)$ \end{itemize} -All transitions together in a disjuction would specify all possible +All transitions together in a disjunction would specify all possible transitions. \newpage