1.tex

   1 \section{Problem 1}
   2 {\em
   3 Six trucks have to deliver pallets of obscure building blocks to a magic
   4 factory. Every truck has a capacity of 7800 kg and can carry at most
   5 eight pallets. In total, the following has to be delivered:
   6 \begin{itemize}
   7         \item Four pallets of nuzzles, each of weight 700 kg.
   8         \item A number of pallets of prittles, each of weight 800 kg.
   9         \item Eight pallets of skipples, each of weight 1000 kg.
  10         \item Ten pallets of crottles, each of weight 1500 kg.
  11         \item Five pallets of dupples, each of weight 100 kg.
  12 \end{itemize}
  13 Prittles and crottles are an explosive combination: they are not allowed to be
  14 put in the same truck.
  15
  16 Skipples need to be cooled; only two of the six trucks have facility for
  17 cooling skipples. Dupples are very valuable; to distribute the risk of loss no
  18 two pallets of dupples may be in the same truck.
  19
  20 Investigate what is the maximum number of pallets of prittles that can be
  21 delivered, and show how for that number all pallets may be divided over the six
  22 trucks.
  23 }
  24
  25 \newpage
  26 \subsection{Formal definition}
  27 For every truck $t_i$ for $i\in T$ where $T=\{1,\ldots,6\}$ in combination with
  28 every nuzzle $n$, prittle $p$, skipple $s$, crottle $c$ and dupple $d$ we
  29 declare a variable that holds the amount of that type of building block in that
  30 truck. We group all pallets $r\in P$ where $P=\{n,p,s,c,d\}$. We also
  31 define function $w(r)$ that defines the weight of the pallet and $n(r)$ that
  32 defines the number of pallets needed.
  33
  34 This leads to the following formalization where we maximize $n(p)$.
  35
  36 \begin{align}
  37         \bigwedge^{T}_{i=1}\Biggl(
  38         & \bigwedge_{r\in P}t_{i}r\geq0\\
  39         & \wedge \sum_{r\in P}t_{i}r\leq8\\
  40         & \wedge \left(\sum_{r\in P}t_{i}r\cdot w(r)\right)\leq7800)\\
  41         & \wedge (t_{i}p=0\vee t_{i}c=0)\\
  42         & \wedge t_{i}d\leq1\\
  43         & \wedge (t_{i}=t_{1} \vee t_{i}=t_{2} \vee t_{i}s=0)\Biggr)\wedge\\
  44         \bigwedge_{r\in P}\Biggl(
  45         & \left(\sum^{T}_{i=1}t_{i}r\right)=n(r)\Biggr)
  46 \end{align}
  47
  48 Every numbered subformula describes a constraint from the problem description.
  49 We can separated the subformulas in formulas going over all trucks and formulas
  50 going over all pallets.
  51
  52 \begin{itemize}
  53         \item \textbf{Trucks}
  54         \begin{enumerate}
  55                 \item Makes sure you can not have a negative number of pallets
  56                         in a truck by stating that the number of pallets in a
  57                         truck is not smaller then $0$.
  58                 \item Makes sure you can not have more then $8$ pallets in a
  59                         truck by stating that the sum of all pallets in a truck
  60                         is not bigger then $8$.
  61                 \item Makes sure the weight will never go over the maximum
  62                         weight per truck by stating that all the pallets times
  63                         their weight in a truck will not go over $7800$kg.
  64                 \item Makes sure prittles and crottles are never together in a
  65                         truck by stating that either the number of prittles is
  66                         zero or the number of crottles is zero in a truck.
  67                 \item Makes sure that skipples are only in the first two cooled
  68                         trucks by stating that if the truck number not one or
  69                         two the number of skipples is zero.
  70         \end{enumerate}
  71         \item \textbf{Pallets}
  72         \begin{enumerate}
  73                 \setcounter{enumi}{6}
  74                 \item Makes sure that all mandatory pallets are transported by
  75                         summing over all trucks and assuring the number of the
  76                         pallets of that type is exactly $n(r)$.
  77         \end{enumerate}
  78 \end{itemize}
  79
  80 \subsection{SMT format solution}
  81 The formula is easily convertable to SMT format by literal conversion and is
  82 listed in Listing~\ref{listing:a1.smt}. The maximization is done by
  83 incrementing a special variable called \texttt{<REP>} which is an instantiation
  84 of $n(p)$.  When the iteration yields unsat we know that the current number
  85 minus one is the maximum amount of prittles the trucks can carry. The
  86 maximization is done with a bash script shown in Listing~\ref{listing:1.bash}.
  87
  88 \lstinputlisting[language=bash,
  89         caption={Iteratively find the largest solution for problem 1},
  90         label={listing:1.bash}]{src/a1.bash}
  91
  92 \subsection{Solution}
  93 The bash script finds and shows the maximal solution of $18$ prittles. Finding
  94 this solution takes less then $0.12$ seconds and is shown in Table~\ref{tab:s1}.
  95
  96 \begin{table}[H]
  97         \centering
  98         \begin{tabular}{l|lllll|ll}
  99                 \toprule
 100                 Truck & Nuzzles & Prittles & Skipples & Crottles & Dupples &
 101                         Weight & Pallets\\
 102                 \midrule
 103                 1 & 0 & 0 & 4 & 2 & 1 & 7100 & 7\\
 104                 2 & 0 & 3 & 4 & 0 & 1 & 6500 & 8\\
 105                 3 & 0 & 8 & 0 & 0 & 0 & 6400 & 7\\
 106                 4 & 0 & 7 & 0 & 0 & 1 & 5700 & 8\\
 107                 5 & 0 & 0 & 0 & 5 & 1 & 7600 & 6\\
 108                 6 & 4 & 0 & 0 & 3 & 1 & 7400 & 8\\
 109                 \midrule
 110                 total & 4 & 18 & 8 & 10 & 5 & &\\
 111                 \bottomrule
 112         \end{tabular}
 113         \caption{Solution visualization for problem 1}
 114 \label{tab:s1}
 115 \end{table}