\section{Problem 1}
{\em
Six trucks have to deliver pallets of obscure building blocks to a magic
-factory. Every ruck has a capacity of 7800 kg and can carry at most
+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.
trucks.
}
+\subsection{Formal definition}
+For every truck $t_i$ for $i\in[1\ldots6]$ 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. For truck 1 we thus have
+the variables: $t_1n, t_1p, t_1s, t_1c, t_1d$.
+To lay a contraint on the weight we declare for every truck the following rule.
+$$\bigwedge^{T}_{i=1}\left(t_in*700+t_ip*800+t_is*1000+t_ic*1500+t_id*100<7800\right)$$
+
+To limit the maximum number of pallets in a truck we define.
+$$\bigwedge^{T}_{i=1}\left(\left(\sum_{p\in\{n,p,s,c,d\}}t_ip\right)\leq8\right)$$
+
+To limit the minimum number of pallets in a truck we define.
+$$\bigwedge^{T}_{i=1}\bigwedge_{p\in\{n,p,s,c,d\}}t_ip>0$$
+
+To describe the number of pallets available we define for every type of pallet
+a variable that describes the number available if there is a limited number
+available.
+$$num_n=4\wedge num_s=8\wedge num_c=10\wedge num_d=5$$
+
+To be sure the materials are all delivered we define.
+$$\bigwedge_{p\in\{n,s,c,d\}}\left(\left(\sum^{T}_{i=1}t_ip\right)=num_p\right)$$
+
+The first constraint is that prittles and crottles can not be in the same
+truck. This is easily described with.
+$$\bigwedge^{T}_{i=1}\left(t_ip=0\vee t_ic=0\right)$$
+
+Skipples need to be cooled and only two trucks have cooling. Therefore we
+specify.
+$$\bigwedge^{T}_{i=3}t_is=0$$
+
+Dupples can only be in a truck with a maximum of two.
+$$\bigwedge^{T}_{i=1}t_id\leq1$$
+
+We can tie this together by putting $\wedge$ symbols between all of the
+formulas.
+
+\subsection{SMT format solution}
+The formula is easily convertable to SMT format and is listed in
+Listing~\ref{listing:a1.smt}. A final condition is added with a special
+variable named \texttt{<REP>} that we increment to find the maximum amount of
+prittles transportable. When running the script in Listing~\ref{listing:1bash}
+the loop terminates after it echoed $20$ meaning that the maximum number of
+prittles is 20. This iterative solution takes less then $0.1$ seconds to
+calculate.
+
+\begin{lstlisting}[language=bash,
+ caption={Iteratively find the largest solution},label={listing:1bash}]
+i=1
+while [ $(sed "s/<REP>/$i/g" a1.smt | yices-smt) = "sat" ]
+do
+ echo $((++i));
+done
+\end{lstlisting}
+
+\subsection{Solution}
+\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}
(benchmark a1.smt
:logic QF_UFLIA
:extrafuns (
- (MaxTruck Int)
- (NuzzleWeight Int)
- (PrittleWeight Int)
- (SkippleWeight Int)
- (CrottleWeight Int)
- (DuppleWeight Int)
+ (t1p Int) (t1n Int) (t1s Int) (t1c Int) (t1d Int)
+ (t2p Int) (t2n Int) (t2s Int) (t2c Int) (t2d Int)
+ (t3p Int) (t3n Int) (t3s Int) (t3c Int) (t3d Int)
+ (t4p Int) (t4n Int) (t4s Int) (t4c Int) (t4d Int)
+ (t5p Int) (t5n Int) (t5s Int) (t5c Int) (t5d Int)
+ (t6p Int) (t6n Int) (t6s Int) (t6c Int) (t6d Int)
)
:formula
(and
- (= NuzzleWeight 700)
- (= PrittleWeight 800)
- (= SkippleWeight 1000)
- (= CrottleWeight 1500)
- (= DuppleWeight 100)
+ (>= t1p 0) (>= t1n 0) (>= t1s 0) (>= t1c 0) (>= t1d 0)
+ (>= t2p 0) (>= t2n 0) (>= t2s 0) (>= t2c 0) (>= t2d 0)
+ (>= t3p 0) (>= t3n 0) (>= t3s 0) (>= t3c 0) (>= t3d 0)
+ (>= t4p 0) (>= t4n 0) (>= t4s 0) (>= t4c 0) (>= t4d 0)
+ (>= t5p 0) (>= t5n 0) (>= t5s 0) (>= t5c 0) (>= t5d 0)
+ (>= t6p 0) (>= t6n 0) (>= t6s 0) (>= t6c 0) (>= t6d 0)
+
+ (<= (+ t1p t1n t1s t1c t1d) 8)
+ (<= (+ t2p t2n t2s t2c t2d) 8)
+ (<= (+ t3p t3n t3s t3c t3d) 8)
+ (<= (+ t4p t4n t4s t4c t4d) 8)
+ (<= (+ t5p t5n t5s t5c t5d) 8)
+ (<= (+ t6p t6n t6s t6c t6d) 8)
+
+ (<= (+ (* t1n 700) (* t1p 800) (* t1s 1000) (* t1c 1500) (* t1d 100)) 7800)
+ (<= (+ (* t2n 700) (* t2p 800) (* t2s 1000) (* t2c 1500) (* t2d 100)) 7800)
+ (<= (+ (* t3n 700) (* t3p 800) (* t3s 1000) (* t3c 1500) (* t3d 100)) 7800)
+ (<= (+ (* t4n 700) (* t4p 800) (* t4s 1000) (* t4c 1500) (* t4d 100)) 7800)
+ (<= (+ (* t5n 700) (* t5p 800) (* t5s 1000) (* t5c 1500) (* t5d 100)) 7800)
+ (<= (+ (* t6n 700) (* t6p 800) (* t6s 1000) (* t6c 1600) (* t6d 100)) 7800)
+
+ (= (+ t1n t2n t3n t4n t5n t6n) 4)
+ (= (+ t1s t2s t3s t4s t5s t6s) 8)
+ (= (+ t1c t2c t3c t4c t5c t6c) 10)
+ (= (+ t1d t2d t3d t4d t5d t6d) 5)
+
+ (or (= 0 t1p) (= 0 t1c))
+ (or (= 0 t2p) (= 0 t2c))
+ (or (= 0 t3p) (= 0 t3c))
+ (or (= 0 t4p) (= 0 t4c))
+ (or (= 0 t5p) (= 0 t5c))
+ (or (= 0 t6p) (= 0 t6c))
+
+ (= t3s 0)
+ (= t4s 0)
+ (= t5s 0)
+ (= t6s 0)
+
+ (<= t1d 1)
+ (<= t2d 1)
+ (<= t3d 1)
+ (<= t4d 1)
+ (<= t5d 1)
+ (<= t6d 1)
+
+ (>= (+ t1p t2p t3p t4p t5p t6p) <REP>)
)
)
repositories / master.git / commitdiff