\section{Problem 1}
{\em
Six trucks have to deliver pallets of obscure building blocks to a magic
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.
	\item A number of pallets of prittles, each of weight 800 kg.
	\item Eight pallets of skipples, each of weight 1000 kg.
	\item Ten pallets of crottles, each of weight 1500 kg.
	\item Five pallets of dupples, each of weight 100 kg.
\end{itemize}
Prittles and crottles are an explosive combination: they are not allowed to be
put in the same truck.

Skipples need to be cooled; only two of the six trucks have facility for
cooling skipples. Dupples are very valuable; to distribute the risk of loss no
two pallets of dupples may be in the same truck.

Investigate what is the maximum number of pallets of prittles that can be
delivered, and show how for that number all pallets may be divided over the six
trucks.
}

\newpage
\subsection{Formal definition}
For every truck $t_i$ for $i\in T$ where $T=\{1,\ldots,6\}$ 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 in that
truck. We group all pallets $r\in P$ where $P=\{n,p,s,c,d\}$. We also
define function $w(r)$ that defines the weight of the pallet and $n(r)$ that
defines the number of pallets needed.

This leads to the following formalization where we maximize $n(p)$.

\begin{align}
	\bigwedge^{T}_{i=1}\Biggl(
	& \bigwedge_{r\in P}t_{i}r\geq0\\
	& \wedge \sum_{r\in P}t_{i}r\leq8\\
	& \wedge \left(\sum_{r\in P}t_{i}r\cdot w(r)\right)\leq7800)\\
	& \wedge (t_{i}p=0\vee t_{i}c=0)\\
	& \wedge t_{i}d\leq1\\
	& \wedge (t_{i}=t_{1} \vee t_{i}=t_{2} \vee t_{i}s=0)\Biggr)\wedge\\
	\bigwedge_{r\in P}\Biggl(
	& \left(\sum^{T}_{i=1}t_{i}r\right)=n(r)\Biggr)
\end{align}

Every numbered subformula describes a constraint from the problem description.
We can separated the subformulas in formulas going over all trucks and formulas
going over all pallets.

\begin{itemize}
	\item \textbf{Trucks}
	\begin{enumerate}
		\item Makes sure you can not have a negative number of pallets
			in a truck by stating that the number of pallets in a
			truck is not smaller then $0$.
		\item Makes sure you can not have more then $8$ pallets in a
			truck by stating that the sum of all pallets in a truck
			is not bigger then $8$.
		\item Makes sure the weight will never go over the maximum
			weight per truck by stating that all the pallets times
			their weight in a truck will not go over $7800$kg.
		\item Makes sure prittles and crottles are never together in a
			truck by stating that either the number of prittles is
			zero or the number of crottles is zero in a truck.
		\item Makes sure that skipples are only in the first two cooled
			trucks by stating that if the truck number not one or
			two the number of skipples is zero.
	\end{enumerate}
	\item \textbf{Pallets}
	\begin{enumerate}
		\setcounter{enumi}{6}
		\item Makes sure that all mandatory pallets are transported by
			summing over all trucks and assuring the number of the
			pallets of that type is exactly $n(r)$.
	\end{enumerate}
\end{itemize}

\subsection{SMT format solution}
The formula is easily convertable to SMT format by literal conversion and is
listed in Listing~\ref{listing:a1.bash}. The maximization is done by
incrementing a special variable called \texttt{<REP>} which is an instantiation
of $n(p)$.  When the iteration yields unsat we know that the current number
minus one is the maximum amount of prittles the trucks can carry. The
maximization is done with a bash script shown in Listing~\ref{listing:1.bash}
and visualized with the python script shown in Listing~\ref{listing:a1.py}

\lstinputlisting[language=bash,firstline=66,
	caption={Iteratively find the largest solution for problem 1},
	label={listing:1.bash}]{src/a1.bash}

\subsection{Solution}
The bash script finds and shows the maximal solution of $18$ prittles. Finding
this solution takes less then $0.12$ seconds and is shown in Table~\ref{tab:s1}.

\begin{table}[H]
	\centering
\input{a1.tex}
	\caption{Solution visualization for problem 1}
\label{tab:s1}
\end{table}
