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 \subsection{Formal definition}
  26 For every truck $t_i$ for $i\in T$ where $T=\{1,\ldots,6\}$ in combination with
  27 every nuzzle $n$, prittle $p$, skipple $s$, crottle $c$ and dupple $d$ we
  28 declare a variable that holds the amount of that type of building block in that
  29 truck. We group all pallets $r\in P$ where $P=\{n,p,s,c,d\}$. We also
  30 define function $w(r)$ that defines the weight of the pallet and $n(r)$ that
  31 defines the number of pallets needed.
  32
  33 This leads to the following formalization where we maximize $n(p)$.
  34
  35 \begin{align}
  36         \bigwedge^{T}_{i=1}\Biggl(
  37         & \bigwedge_{r\in P}t_{i}r\geq0\\
  38         & \wedge \sum_{r\in P}t_{i}r\leq8\\
  39         & \wedge \left(\sum_{r\in P}t_{i}r\cdot w(r)\right)\leq7800)\\
  40         & \wedge (t_{i}p=0\vee t_{i}c=0)\\
  41         & \wedge t_{i}d\leq1\\
  42         & \wedge (t_{i}=t_{1} \vee t_{i}=t_{2} \vee t_{i}s=0)\Biggr)\wedge\\
  43         \bigwedge_{r\in P}\Biggl(
  44         & \left(\sum^{T}_{i=1}t_{i}r\right)=n(r)\Biggr)
  45 \end{align}
  46
  47 Every numbered subformula describes a constraint from the problem description.
  48 We can separated the subformulas in formulas going over all trucks and formulas
  49 going over all pallets.
  50
  51 \begin{itemize}
  52         \item \textbf{Trucks}
  53         \begin{enumerate}
  54                 \item Makes sure you can not have a negative number of pallets
  55                         in a truck by stating that the number of pallets in a
  56                         truck is not smaller then $0$.
  57                 \item Makes sure you can not have more then $8$ pallets in a
  58                         truck by stating that the sum of all pallets in a truck
  59                         is not bigger then $8$.
  60                 \item Makes sure the weight will never go over the maximum
  61                         weight per truck by stating that all the pallets times
  62                         their weight in a truck will not go over $7800$kg.
  63                 \item Makes sure prittles and crottles are never together in a
  64                         truck by stating that either the number of prittles is
  65                         zero or the number of crottles is zero in a truck.
  66                 \item Makes sure that skipples are only in the first two cooled
  67                         trucks by stating that if the truck number not one or
  68                         two the number of skipples is zero.
  69         \end{enumerate}
  70         \item \textbf{Pallets}
  71         \begin{enumerate}
  72                 \setcounter{enumi}{6}
  73                 \item Makes sure that all mandatory pallets are transported by
  74                         summing over all trucks and assuring the number of the
  75                         pallets of that type is exactly $n(r)$.
  76         \end{enumerate}
  77 \end{itemize}
  78
  79 \subsection{SMT format solution}
  80 The formula is easily convertable to SMT format by literal conversion. The
  81 maximization is done by incrementing a special variable called \texttt{<REP>}
  82 which is an instantiation of $n(p)$.  When the iteration yields unsat we know
  83 that the current number minus one is the maximum amount of prittles the trucks
  84 can carry. The maximization is done with a bash script shown in
  85 Listing~\ref{listing:1.bash} and visualized with the python script.
  86
  87 \lstinputlisting[language=bash,firstline=66,
  88         caption={Iteratively find the largest solution for problem 1},
  89         label={listing:1.bash}]{src/a1.bash}
  90
  91 \subsection{Solution}
  92 The bash script finds and shows the maximal solution of $18$ prittles. Finding
  93 this solution takes less then $0.12$ seconds and is shown in Table~\ref{tab:s1}.
  94
  95 \begin{table}[H]
  96         \centering
  97 \input{a1.tex}
  98         \caption{Solution visualization for problem 1}
  99 \label{tab:s1}
 100 \end{table}