diff options
Diffstat (limited to 'part1.tex')
| -rw-r--r-- | part1.tex | 151 |
1 files changed, 142 insertions, 9 deletions
@@ -58,15 +58,148 @@ are an explosive combination: they are not allowed to be put in the same truck. \subsection*{Solution:} \subsubsection*{(a)} -We generalized this problem to fitting pallets into $T$ trucks, with capacity $c_T$ and maximum amount of pallets $p_T$. Then we added variables $N$, $P$, $C$, $S$ and $D$ representing Nuzzles, Prittles, Crottles, Skipples and Dupples respectively. -The size of $P$ is to be determined. -To put a constraint on the capacity of a truck, we created the following formula:\\ -$\sum_{x \in X} (ite (x \in T) (weight(x)) (0))$, where $X \in {N, P, C, S, D}$.\\ We summed the result for all $X$, and compared it to $c_T$. -We did exactly the same for the amount of pallets, where we substituted $weight(x)$ with $1$, and $c_T$ with $p_T$. -After this, we added the static constraints that $s \in S$ must be in truck $1$, $2$ or $3$ as these are our cooling trucks. -Finally we added a constraint saying all $n \in N$ are distinct. - -Since we have $8$ trucks, with maximum amount of pallets $8$, we can carry at most $64$ pallets. This means that we can carry at most $22$ pallets of prittles. We searched for the solution of how many pallets we could actually carry in a binary sense: First we tried $11$ pallets, then $16$, then $19$, $21$ and finally $22$. These tries were all satisfiable, thus we can carry at most $22$ pallets of prittles. +We generalize this problem to fitting $m$ different types of pallets into $n$ +trucks. Let $B$ be the set of pallet types (with building blocks). +Each type of a building block $b \in B$ has a corresponding weight $W_b$ and a +total number $C_b$ that must be spread over all trucks. +We introduce $m \times n$ different variables that describe how many +pallets of each type are assigned to each truck. For every truck $1 \leq j \leq +n$ and every $b \in B$, we define variable $b_j$ as the number of pallets of +type $b$ assigned to truck $j$. + +In our scenario, $B = \{ N, P, S, C, D \}$ (denoting Nuzzles, Prittles, +Skipples, Crottles and Dupples respectively). +We have maximum weight capacity $W_{truck}=8000$ and maximum pallet capacity +$C_{truck}=8$. + +First a sanity check, the number of assigned pallets must be positive: +\begin{align} +\label{eq:truck1} +\bigwedge_{b \in B} +\bigwedge_{i=1}^n +b_i \geq 0 +\end{align} + +Next, we require that all pallets are indeed distributed over the trucks: +\begin{align} +\label{eq:truck2} +\bigwedge_{b \in B} +C_b = +\sum_{i=1}^n +b_i +\end{align} + +Each truck has a maximum pallet and weight capacity that must not be exceeded: +\begin{align} +\label{eq:truck3} +\bigwedge_{i=1}^n +( + (\sum_{b \in B} b_i) + \leq + C_{truck} +) \land ( + (\sum_{b \in B} b_i \cdot w_i) + \leq + W_{truck} +) +\end{align} + +The above ingredients describe the basic capacity requirements. Next, additional +requirements are incorporated. These may make some of the above requirements +partially unnecessary, but we choose to keep these for easier understanding. +Optimizations (like subsumption) can be easily handled by the SAT solvers. + +At most three trucks can store Skipples. This can be expressed as each triple of +trucks having the sum equal to $C_S$ (the total number of skipples). +Or alternatively, all trucks other than these triple must carry zero Skipples. +We tried to implement both, but for some reason the second comparison was faster +(probably because the first one was expressed as a conjunction with small +disjunctions while the latter one is expressed as one big disjunction). The +alternative is expressed as: +\begin{align} +\label{eq:truck4} +\bigvee_{1 \leq x,y,z \leq n, x \neq y, y \neq z, x \neq z} +\bigwedge_{1 \leq i \leq n, i \not\in\{x,y,z\}}^n +S_i = 0 +\end{align} + +Finally the limitation that trucks can carry only one pallet of Nuzzles: +\begin{align} +\label{eq:truck5} +\bigwedge_{i=1}^n +N_i \leq 1 +\end{align} + +We wrote a generator program that takes the conjunction of the above parts +(ingredients \ref{eq:truck1}, \ref{eq:truck2}, \ref{eq:truck3}, \ref{eq:truck4} +and \ref{eq:truck5}). At first, $C_P$ was unknown, so we removed clauses that +relied on this. The initial evaluation with z3 finished within a second and +allowed us to make a better educated guess at the actual (maximum) value of +$C_P$. It turns out that with 22 pallets were unassigned, so we used this in the +next evaluation. + +Evaluation of the generated output (shown in Listing~\ref{lst:palletsInTrucks}) +using the command \texttt{python generate-chipdesign.py 22 | z3 -smt -in} +finished in 100 milliseconds. The result is shown in +Table~\ref{tbl:palletsInTrucks}. It happens that all trucks can be filled, +including 22 Prittles. As mentioned before, the alternative check for +Ingredient~\ref{eq:truck4} takes more time (200ms). + +\begin{table}[H] +\centering +\begin{tabular}{r|rrrrr|rr} + & N & P & S & C & D & weight & \#pallets \\ +\hline + 1 & 1 & 5 & 0 & 2 & 0 & 7700 & 8 \\ + 2 & 1 & 1 & 0 & 2 & 4 & 6900 & 8 \\ + 3 & 0 & 3 & 0 & 2 & 3 & 6800 & 8 \\ + 4 & 0 & 0 & 8 & 0 & 0 & 8000 & 8 \\ + 5 & 1 & 7 & 0 & 0 & 0 & 3500 & 8 \\ + 6 & 1 & 0 & 0 & 2 & 5 & 6700 & 8 \\ + 7 & 0 & 6 & 0 & 2 & 0 & 7400 & 8 \\ + 8 & 0 & 0 & 0 & 0 & 8 & 1600 & 8 \\ +\hline + & 4 & 22 & 8 & 10 & 20 +\end{tabular} +\caption{\label{tbl:palletsInTrucks}The assignment of pallets to trucks. The + rows of the table body describe the contents of a truck. The last row shows + the total number of one pallet type as distributed over all trucks.} +\end{table} + +\begin{lstlisting}[ + caption={Generated SMT for pallet fitting problem.}, + label={lst:palletsInTrucks},language=lisp,basicstyle=\scriptsize +] +(benchmark test.smt +:logic QF_UFLIA +:extrafuns ( +(N1 Int) (P1 Int) (S1 Int) (C1 Int) (D1 Int) +... +(N8 Int) (P8 Int) (S8 Int) (C8 Int) (D8 Int) +) +:formula (and +(>= N1 0) (>= P1 0) (>= S1 0) (>= C1 0) (>= D1 0) +... +(>= N8 0) (>= P8 0) (>= S8 0) (>= C8 0) (>= D8 0) +(= 4 (+ N1 N2 N3 N4 N5 N6 N7 N8)) +(= 22 (+ P1 P2 P3 P4 P5 P6 P7 P8)) +(= 8 (+ S1 S2 S3 S4 S5 S6 S7 S8)) +(= 10 (+ C1 C2 C3 C4 C5 C6 C7 C8)) +(= 20 (+ D1 D2 D3 D4 D5 D6 D7 D8)) +(>= 8 (+ N1 P1 S1 C1 D1)) +(>= 8000 (+ (* N1 700) (* P1 400) (* S1 1000) (* C1 2500) (* D1 200))) +... +(>= 8 (+ N8 P8 S8 C8 D8)) +(>= 8000 (+ (* N8 700) (* P8 400) (* S8 1000) (* C8 2500) (* D8 200))) +(or (= 0 S4) (= 0 S5) (= 0 S6) (= 0 S7) (= 0 S8)) +(or (= 0 S3) (= 0 S5) (= 0 S6) (= 0 S7) (= 0 S8)) +... +(or (= 0 S1) (= 0 S2) (= 0 S3) (= 0 S4) (= 0 S6)) +(or (= 0 S1) (= 0 S2) (= 0 S3) (= 0 S4) (= 0 S5)) +(>= 1 N1) (>= 1 N2) (>= 1 N3) (>= 1 N4) (>= 1 N5) (>= 1 N6) (>= 1 N7) (>= 1 N8) +)) +\end{lstlisting} + \subsubsection*{(b)} For part b of the assignment, we added a set of constraints saying that whenever a truck contains a pallet of Crottles, it may not contain a pallet of Prittles. |