delivered, and show how for that number all pallets may be divided over the six
trucks.
}
-
+\newpage
\subsection{Formal definition}
-For every truck $t_i$ for $i\in[1\ldots6]$ in combination with every nuzzle
-$n$, prittle $p$, skipple $s$, crottle $c$ and dupple $d$ we declare a variable
-that holds the amount of that type of building block. For truck 1 we thus have
-the variables: $t_1n, t_1p, t_1s, t_1c, t_1d$.
-
-To lay a contraint on the weight we declare for every truck the following rule.
-$$\bigwedge^{T}_{i=1}\left(t_in*700+t_ip*800+t_is*1000+t_ic*1500+t_id*100<7800\right)$$
-
-To limit the maximum number of pallets in a truck we define.
-$$\bigwedge^{T}_{i=1}\left(\left(\sum_{p\in\{n,p,s,c,d\}}t_ip\right)\leq8\right)$$
-
-To limit the minimum number of pallets in a truck we define.
-$$\bigwedge^{T}_{i=1}\bigwedge_{p\in\{n,p,s,c,d\}}t_ip>0$$
-
-To describe the number of pallets available we define for every type of pallet
-a variable that describes the number available if there is a limited number
-available.
-$$num_n=4\wedge num_s=8\wedge num_c=10\wedge num_d=5$$
+For every truck $t_i$ for $i\in T$ where $T=[1\ldots6]$ in combination with
+every nuzzle $n$, prittle $p$, skipple $s$, crottle $c$ and dupple $d$ we
+declare a variable that holds the amount of that type of building block.
+We group all pallets $r$ for $r\in P$ where $P=[n,p,s,c,d]$. We also define
+function $w(r)$ that defines the weight of the pallet and $n(r)$ that defines
+the number of pallets needed. Then the following combination of subformulas
+describes the problem.
-To be sure the materials are all delivered we define.
-$$\bigwedge_{p\in\{n,s,c,d\}}\left(\left(\sum^{T}_{i=1}t_ip\right)=num_p\right)$$
+\begin{align}
+ \bigwedge^{T}_{i=1}\Biggl(
+ & \bigwedge_{r\in P}t_ir\geq0\\
+ & \wedge \sum_{r\in P}t_ir\leq8\\
+ & \wedge \left(\sum_{r\in P}t_ir*w(r)\right)\leq7800)\\
+ & \wedge (t_ip=0\vee t_ic=0)\\
+ & \wedge t_id\leq1\\
+ & \wedge (t_i=t_1 \vee t_i=t_2 \vee t_is=0)\Biggr)\wedge\\
+ \bigwedge_{r\in P}\Biggl(
+ & r=p\vee\left(\sum^{T}_{i=1}t_ir\right)=n(r)\Biggr)
+\end{align}
-The first constraint is that prittles and crottles can not be in the same
-truck. This is easily described with.
-$$\bigwedge^{T}_{i=1}\left(t_ip=0\vee t_ic=0\right)$$
-
-Skipples need to be cooled and only two trucks have cooling. Therefore we
-specify.
-$$\bigwedge^{T}_{i=3}t_is=0$$
-
-Dupples can only be in a truck with a maximum of two.
-$$\bigwedge^{T}_{i=1}t_id\leq1$$
-
-We can tie this together by putting $\wedge$ symbols between all of the
-formulas.
+All the subformulas describe a constraint from the problem description and we
+can separate two groups. Subformulas going over all trucks and subformulas over
+all pallets.
+\begin{itemize}
+ \item \textbf{Trucks}
+ \begin{enumerate}
+ \item Makes sure you can not have a negative number of pallets.
+ by stating that all pallets numbers per truck are
+ bigger then $0$.
+ \item Makes sure you can not have more then $8$ pallets in a
+ truck by stating that the sum of all pallets in a truck
+ is not bigger then $8$.
+ \item Makes sure the weight will never go over the maximum by
+ stating that all the pallets times their weight in a
+ truck may not go over $7800$kg.
+ \item Makes sure prittles and crottles are never together in a
+ truck by stating that either the number of prittles is
+ zero or the number of crottles is zero. Note that they
+ therefore also can both be zero.
+ \item Makes sure that skipples are only in the first two cooled
+ trucks by stating that if the truck number not one or
+ two the number of skipples is zero.
+ \end{enumerate}
+ \item \textbf{Pallets}
+ \begin{enumerate}
+ \setcounter{enumi}{6}
+ \item Makes sure that all mandatory pallets are transported by
+ summing over all trucks and assuring the number of the
+ pallets of that type is exactly $n(r)$. Note that this
+ should hold or that the current pallet is a prittle
+ pallet since we do not have a limit on prittles.
+ \end{enumerate}
+\end{itemize}
\subsection{SMT format solution}
The formula is easily convertable to SMT format and is listed in
repositories / master.git / blobdiff