trucks.
}
+\newpage
\subsection{Formal definition}
-For every truck $t_i$ for $i\in T$ where $T=[1\ldots6]$ in combination with
+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.
-We group all pallets $r$ for $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. Then the following combination of subformulas
-describes the problem.
+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_ir\geq0\\
- & \wedge \sum_{r\in P}t_ir\leq8\\
- & \wedge \left(\sum_{r\in P}t_ir*w(r)\right)\leq7800)\\
- & \wedge (t_ip=0\vee t_ic=0)\\
- & \wedge t_id\leq1\\
- & \wedge (t_i=t_1 \vee t_i=t_2 \vee t_is=0)\Biggr)\wedge\\
+ & \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(
- & r=p\vee\left(\sum^{T}_{i=1}t_ir\right)=n(r)\Biggr)
+ & \left(\sum^{T}_{i=1}t_{i}r\right)=n(r)\Biggr)
\end{align}
-All the subformulas describe a constraint from the problem description and we
-can separate two groups. Subformulas going over all trucks and subformulas over
-all pallets.
+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.
- by stating that all pallets numbers per truck are
- bigger then $0$.
+ \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 by
- stating that all the pallets times their weight in a
- truck may not go over $7800$kg.
+ \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. Note that they
- therefore also can both be zero.
+ 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.
\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)$. Note that this
- should hold or that the current pallet is a prittle
- pallet since we do not have a limit on prittles.
+ pallets of that type is exactly $n(r)$.
\end{enumerate}
\end{itemize}
\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.
+Listing~\ref{listing:a1.smt}. 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}.
-\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}
+\lstinputlisting[language=bash,
+ caption={Iteratively find the largest solution for problem 1},
+ label={listing:1.bash}]{src/a1.bash}
\subsection{Solution}
-The iterative solution terminates with $i=18$ so the maximum number of prittles
-to be deliverd is $18$. When we rerun the solution with $18$ prittles and the
-\texttt{-m} flag we can see the solution as in Table~\ref{tab:s1}.
+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]
\begin{tabular}{|l|lllll|l|l|}
\hline
- Truck & Nuzzles & Prittles & Skipples & Crottles & Dupples & Weight & Pallets\\
+ 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\\
total & 4 & 18 & 8 & 10 & 5 & &\\
\hline
\end{tabular}
- \caption{Solution table for problem 1}
- \label{tab:s1}
+ \caption{Solution visualization for problem 1}
+\label{tab:s1}
\end{table}
repositories / master.git / blobdiff