ar/assignments/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\ldots6]$ 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.
  29 We group all pallets $r$ for $r\in P$ where $P=[n,p,s,c,d]$. We also define
  30 function $w(r)$ that defines the weight of the pallet and $n(r)$ that defines
  31 the number of pallets needed. Then the following combination of subformulas
  32 describes the problem.
  33
  34 \begin{align}
  35         \bigwedge^{T}_{i=1}\Biggl(
  36         & \bigwedge_{r\in P}t_ir\geq0\\
  37         & \wedge \sum_{r\in P}t_ir\leq8\\
  38         & \wedge \left(\sum_{r\in P}t_ir*w(r)\right)\leq7800)\\
  39         & \wedge (t_ip=0\vee t_ic=0)\\
  40         & \wedge t_id\leq1\\
  41         & \wedge (t_i=t_1 \vee t_i=t_2 \vee t_is=0)\Biggr)\wedge\\
  42         \bigwedge_{r\in P}\Biggl(
  43         & r=p\vee\left(\sum^{T}_{i=1}t_ir\right)=n(r)\Biggr)
  44 \end{align}
  45
  46 All the subformulas describe a constraint from the problem description and we
  47 can separate two groups. Subformulas going over all trucks and subformulas over
  48 all pallets.
  49 \begin{itemize}
  50         \item \textbf{Trucks}
  51         \begin{enumerate}
  52                 \item Makes sure you can not have a negative number of pallets.
  53                         by stating that all pallets numbers per truck are
  54                         bigger then $0$.
  55                 \item Makes sure you can not have more then $8$ pallets in a
  56                         truck by stating that the sum of all pallets in a truck
  57                         is not bigger then $8$.
  58                 \item Makes sure the weight will never go over the maximum by
  59                         stating that all the pallets times their weight in a
  60                         truck may not go over $7800$kg.
  61                 \item Makes sure prittles and crottles are never together in a
  62                         truck by stating that either the number of prittles is
  63                         zero or the number of crottles is zero. Note that they
  64                         therefore also can both be zero.
  65                 \item Makes sure that skipples are only in the first two cooled
  66                         trucks by stating that if the truck number not one or
  67                         two the number of skipples is zero.
  68         \end{enumerate}
  69         \item \textbf{Pallets}
  70         \begin{enumerate}
  71                 \setcounter{enumi}{6}
  72                 \item Makes sure that all mandatory pallets are transported by
  73                         summing over all trucks and assuring the number of the
  74                         pallets of that type is exactly $n(r)$. Note that this
  75                         should hold or that the current pallet is a prittle
  76                         pallet since we do not have a limit on prittles.
  77         \end{enumerate}
  78 \end{itemize}
  79
  80 \subsection{SMT format solution}
  81 The formula is easily convertable to SMT format and is listed in
  82 Listing~\ref{listing:a1.smt}. A final condition is added with a special
  83 variable named \texttt{<REP>} that we increment to find the maximum amount of
  84 prittles transportable. When running the script in Listing~\ref{listing:1bash}
  85 the loop terminates after it echoed $20$ meaning that the maximum number of
  86 prittles is 20. This iterative solution takes less then $0.1$ seconds to
  87 calculate.
  88
  89 \begin{lstlisting}[language=bash,
  90         caption={Iteratively find the largest solution},label={listing:1bash}]
  91 i=1
  92 while [ $(sed "s/<REP>/$i/g" a1.smt | yices-smt) = "sat" ]
  93 do
  94         echo $((++i));
  95 done
  96 \end{lstlisting}
  97
  98 \subsection{Solution}
  99 The iterative solution terminates with $i=18$ so the maximum number of prittles
 100 to be deliverd is $18$. When we rerun the solution with $18$ prittles and the
 101 \texttt{-m} flag we can see the solution as in Table~\ref{tab:s1}.
 102
 103 \begin{table}[H]
 104         \begin{tabular}{|l|lllll|l|l|}
 105                 \hline
 106                 Truck & Nuzzles & Prittles & Skipples & Crottles & Dupples & Weight & Pallets\\
 107                 \hline
 108                 1 & 0 & 0 & 4 & 2 & 1 & 7100 & 7\\
 109                 2 & 0 & 3 & 4 & 0 & 1 & 6500 & 8\\
 110                 3 & 0 & 8 & 0 & 0 & 0 & 6400 & 7\\
 111                 4 & 0 & 7 & 0 & 0 & 1 & 5700 & 8\\
 112                 5 & 0 & 0 & 0 & 5 & 1 & 7600 & 6\\
 113                 6 & 4 & 0 & 0 & 3 & 1 & 7400 & 8\\
 114                 \hline
 115                 total & 4 & 18 & 8 & 10 & 5 & &\\
 116                 \hline
 117         \end{tabular}
 118         \caption{Solution table for problem 1}
 119         \label{tab:s1}
 120 \end{table}