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 Skipples need to be cooled; only two of the six trucks have facility for
  16 cooling skipples. Dupples are very valuable; to distribute the risk of loss no
  17 two pallets of dupples may be in the same truck.\\
  18 Investigate what is the maximum number of pallets of prittles that can be
  19 delivered, and show how for that number all pallets may be divided over the six
  20 trucks.
  21 }
  22
  23 \subsection{Formal definition}
  24 For every truck $t_i$ for $i\in[1\ldots6]$ in combination with every nuzzle
  25 $n$, prittle $p$, skipple $s$, crottle $c$ and dupple $d$ we declare a variable
  26 that holds the amount of that type of building block. For truck 1 we thus have
  27 the variables: $t_1n, t_1p, t_1s, t_1c, t_1d$.
  28
  29 To lay a contraint on the weight we declare for every truck the following rule.
  30 $$\bigwedge^{T}_{i=1}\left(t_in*700+t_ip*800+t_is*1000+t_ic*1500+t_id*100<7800\right)$$
  31
  32 To limit the maximum number of pallets in a truck we define.
  33 $$\bigwedge^{T}_{i=1}\left(\left(\sum_{p\in\{n,p,s,c,d\}}t_ip\right)\leq8\right)$$
  34
  35 To limit the minimum number of pallets in a truck we define.
  36 $$\bigwedge^{T}_{i=1}\bigwedge_{p\in\{n,p,s,c,d\}}t_ip>0$$
  37
  38 To describe the number of pallets available we define for every type of pallet
  39 a variable that describes the number available if there is a limited number
  40 available.
  41 $$num_n=4\wedge num_s=8\wedge num_c=10\wedge num_d=5$$
  42
  43 To be sure the materials are all delivered we define.
  44 $$\bigwedge_{p\in\{n,s,c,d\}}\left(\left(\sum^{T}_{i=1}t_ip\right)=num_p\right)$$
  45
  46 The first constraint is that prittles and crottles can not be in the same
  47 truck. This is easily described with.
  48 $$\bigwedge^{T}_{i=1}\left(t_ip=0\vee t_ic=0\right)$$
  49
  50 Skipples need to be cooled and only two trucks have cooling. Therefore we
  51 specify.
  52 $$\bigwedge^{T}_{i=3}t_is=0$$
  53
  54 Dupples can only be in a truck with a maximum of two.
  55 $$\bigwedge^{T}_{i=1}t_id\leq1$$
  56
  57 We can tie this together by putting $\wedge$ symbols between all of the
  58 formulas.
  59
  60 \subsection{SMT format solution}
  61 The formula is easily convertable to SMT format and is listed in
  62 Listing~\ref{listing:a1.smt}. A final condition is added with a special
  63 variable named \texttt{<REP>} that we increment to find the maximum amount of
  64 prittles transportable. When running the script in Listing~\ref{listing:1bash}
  65 the loop terminates after it echoed $20$ meaning that the maximum number of
  66 prittles is 20. This iterative solution takes less then $0.1$ seconds to
  67 calculate.
  68
  69 \begin{lstlisting}[language=bash,
  70         caption={Iteratively find the largest solution},label={listing:1bash}]
  71 i=1
  72 while [ $(sed "s/<REP>/$i/g" a1.smt | yices-smt) = "sat" ]
  73 do
  74         echo $((++i));
  75 done
  76 \end{lstlisting}
  77
  78 \subsection{Solution}
  79 \begin{tabular}{|l|lllll|l|l|}
  80         \hline
  81         Truck & Nuzzles & Prittles & Skipples & Crottles & Dupples & Weight & Pallets\\
  82         \hline
  83         1 & 0 & 0 & 4 & 2 & 1 & 7100 & 7\\
  84         2 & 0 & 3 & 4 & 0 & 1 & 6500 & 8\\
  85         3 & 0 & 8 & 0 & 0 & 0 & 6400 & 7\\
  86         4 & 0 & 7 & 0 & 0 & 1 & 5700 & 8\\
  87         5 & 0 & 0 & 0 & 5 & 1 & 7600 & 6\\
  88         6 & 4 & 0 & 0 & 3 & 1 & 7400 & 8\\
  89         \hline
  90         total & 4 & 18 & 8 & 10 & 5 & &\\
  91         \hline
  92 \end{tabular}