\section{Problem 1}
{\em
Six trucks have to deliver pallets of obscure building blocks to a magic
-factory. Every ruck has a capacity of 7800 kg and can carry at most
+factory. Every truck has a capacity of 7800 kg and can carry at most
eight pallets. In total, the following has to be delivered:\\
\begin{itemize}
\item Four pallets of nuzzles, each of weight 700 kg.
trucks.
}
+\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$$
+
+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)$$
+
+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.
+
+\subsection{SMT format solution}
+The formula is easily convertable to SMT format and is listed in
+Listing~\ref{listing:a1.smt}. A final condition is added with a special
+variable named \texttt{<REP>} that we increment to find the maximum amount of
+prittles transportable. When running the script in Listing~\ref{listing:1bash}
+the loop terminates after it echoed $20$ meaning that the maximum number of
+prittles is 20. This iterative solution takes less then $0.1$ seconds to
+calculate.
+
+\begin{lstlisting}[language=bash,
+ caption={Iteratively find the largest solution},label={listing:1bash}]
+i=1
+while [ $(sed "s/<REP>/$i/g" a1.smt | yices-smt) = "sat" ]
+do
+ echo $((++i));
+done
+\end{lstlisting}
+
+\subsection{Solution}
+\begin{tabular}{|l|lllll|l|l|}
+ \hline
+ Truck & Nuzzles & Prittles & Skipples & Crottles & Dupples & Weight & Pallets\\
+ \hline
+ 1 & 0 & 0 & 4 & 2 & 1 & 7100 & 7\\
+ 2 & 0 & 3 & 4 & 0 & 1 & 6500 & 8\\
+ 3 & 0 & 8 & 0 & 0 & 0 & 6400 & 7\\
+ 4 & 0 & 7 & 0 & 0 & 1 & 5700 & 8\\
+ 5 & 0 & 0 & 0 & 5 & 1 & 7600 & 6\\
+ 6 & 4 & 0 & 0 & 3 & 1 & 7400 & 8\\
+ \hline
+ total & 4 & 18 & 8 & 10 & 5 & &\\
+ \hline
+\end{tabular}
repositories / master.git / blobdiff