+++ /dev/null
-\section{Problem 1}
-{\em
-Six trucks have to deliver pallets of obscure building blocks to a magic
-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.
- \item A number of pallets of prittles, each of weight 800 kg.
- \item Eight pallets of skipples, each of weight 1000 kg.
- \item Ten pallets of crottles, each of weight 1500 kg.
- \item Five pallets of dupples, each of weight 100 kg.
-\end{itemize}
-Prittles and crottles are an explosive combination: they are not allowed to be
-put in the same truck.
-
-Skipples need to be cooled; only two of the six trucks have facility for
-cooling skipples. Dupples are very valuable; to distribute the risk of loss no
-two pallets of dupples may be in the same truck.
-
-Investigate what is the maximum number of pallets of prittles that can be
-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 T$ where $T=\{1,\ldots,6\}$ 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 in that
-truck. We group all pallets $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.
-
-This leads to the following formalization where we maximize $n(p)$.
-
-\begin{align}
- \bigwedge^{T}_{i=1}\Biggl(
- & \bigwedge_{r\in P}t_{i}r\geq0\\
- & \wedge \sum_{r\in P}t_{i}r\leq8\\
- & \wedge \left(\sum_{r\in P}t_{i}r\cdot w(r)\right)\leq7800)\\
- & \wedge (t_{i}p=0\vee t_{i}c=0)\\
- & \wedge t_{i}d\leq1\\
- & \wedge (t_{i}=t_{1} \vee t_{i}=t_{2} \vee t_{i}s=0)\Biggr)\wedge\\
- \bigwedge_{r\in P}\Biggl(
- & \left(\sum^{T}_{i=1}t_{i}r\right)=n(r)\Biggr)
-\end{align}
-
-Every numbered subformula describes a constraint from the problem description.
-We can separated the subformulas in formulas going over all trucks and formulas
-going over all pallets.
-
-\begin{itemize}
- \item \textbf{Trucks}
- \begin{enumerate}
- \item Makes sure you can not have a negative number of pallets
- in a truck by stating that the number of pallets in a
- truck is not smaller 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
- weight per truck by stating that all the pallets times
- their weight in a truck will 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 in a truck.
- \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)$.
- \end{enumerate}
-\end{itemize}
-
-\subsection{SMT format solution}
-The formula is easily convertable to SMT format and is listed in
-Listing~\ref{listing:a1.smt}. The maximization is done by incrementing a
-special variable called \texttt{<REP>} which is an instantiation of $n(p)$.
-When the iteration yields unsat we know that the current number minus one is
-the maximum amount of prittles the trucks can carry. The maximization is done
-with a bash script shown in Listing~\ref{listing:1.bash}.
-
-\lstinputlisting[language=bash,
- caption={Iteratively find the largest solution for problem 1},
- label={listing:1.bash}]{src/a1.bash}
-
-\subsection{Solution}
-The bash script finds and shows the maximal solution of $18$ prittles. Finding
-this solution takes less then $0.12$ seconds and is shown in Table~\ref{tab:s1}.
-
-\begin{table}[H]
- \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}
- \caption{Solution visualization for problem 1}
-\label{tab:s1}
-\end{table}
repositories / master.git / blobdiff