From 61af52b0328d1a875af998fd0ead513ee14eb503 Mon Sep 17 00:00:00 2001 From: Peter Wu Date: Wed, 14 Dec 2016 19:37:35 +0100 Subject: PackingPallets; redid 1a A bit more formal and generalized. --- .../generate-packingpallets.py | 155 +++++++++++++++++++++ packing_pallets_in_trucks/pallets-to-latex.py | 79 +++++++++++ part1.tex | 151 ++++++++++++++++++-- 3 files changed, 376 insertions(+), 9 deletions(-) create mode 100755 packing_pallets_in_trucks/generate-packingpallets.py create mode 100755 packing_pallets_in_trucks/pallets-to-latex.py diff --git a/packing_pallets_in_trucks/generate-packingpallets.py b/packing_pallets_in_trucks/generate-packingpallets.py new file mode 100755 index 0000000..e46694d --- /dev/null +++ b/packing_pallets_in_trucks/generate-packingpallets.py @@ -0,0 +1,155 @@ +#!/usr/bin/env python +# Usage for 1a (where -1 is the number of prittles, -1 means unrestricted) +# $0 -1 | z3 -smt -in +# Usage for 1b: +# $0 -1 b | z3 -smt -in + +import sys + +number_of_prittles = int(sys.argv[1]) +prtl = None if number_of_prittles == -1 else number_of_prittles +is_b = len(sys.argv) >= 3 and sys.argv[2] == 'b' + +# List of m types ("m types"): +# - exact number of items needed (or None for no restriction) +# - Name (first letter is used for variable) +# - Weight (in kg) +stuff = [ + (4, "Nuzzles", 700), + (prtl, "Prittles", 400), + (8, "Skipples", 1000), + (10, "Crottles", 2500), + (20, "Dupples", 200), +] + +# T trucks ("n trucks") +n_trucks = 8 +# Capacity C_T +truck_capacity = 8000 +# Maximum pallets p_T +max_pallets = 8 + +def fillin(cases, template_vars): + if type(cases) == str: + return cases.format(**template_vars) + return [template.format(**template_vars) for template in cases] + +literals = [] +preds = [] + +# For each truck, +# define the number of pallets of each type that will be contained in. +for i in range(1, n_trucks + 1): + for needed, name, weight in stuff: + name = "{name[0]}{i}".format(name=name, i=i) + literals.append(name) + # Cannot have negative number of items... + preds += fillin([ + "(>= {name} 0)" + ], vars()) + +# For each item, require exact as many items spread over all trucks +for needed, name, weight in stuff: + if needed is None: + continue + # total_items = item_in_truck0 + ... + item_in_truckN + items_in_truckX = " ".join( + "{name[0]}{i}".format(name=name, i=i) + for i in range(1, n_trucks + 1) + ) + preds += fillin([ + "(= {needed} (+ {items_in_truckX}))", + ], vars()) + +# Each truck may hold a maximum number of pallets. +# and a maximum weight. +for i in range(1, n_trucks + 1): + # max_pallets >= item0_in_truck + ... + itemM_in_truck + itemX_in_truck = " ".join( + "{name[0]}{i}".format(name=name, i=i) + for needed, name, weight in stuff + ) + total_weight_in_truck = " ".join( + "(* {name[0]}{i} {weight})".format(name=name, i=i, weight=weight) + for needed, name, weight in stuff + ) + preds += fillin([ + "(>= {max_pallets} (+ {itemX_in_truck}))", + "(>= {truck_capacity} (+ {total_weight_in_truck}))", + ], vars()) + + +# Skipples must be distributed over at most three trucks. +# So, Any combination of n-3 trucks must have zero skipples. +number_of_skipples = None +for needed, name, weight in stuff: + if name[0] == 'S': + number_of_skipples = needed +assert number_of_skipples is not None +skipple_preds = [] +for x in range(1, n_trucks + 1): + for y in range(1, n_trucks + 1): + if x == y: + # Require unique pairs (x, y, 0, ..., 0) as optimization. + # This is weaker than (x, 0, ... 0) + continue + for z in range(1, n_trucks + 1): + if x == z or y == z: + # Same as above, require unique x, y, z such that + # (x, y, z, 0, ..., 0) + continue + + # "These threee trucks hold all available skipples" + #items_all_in_these_trucks = [ + # "S{i}".format(i=i) + # for i in (x, y, z) + #] + #skipple_preds += fillin([ + # "(= {number_of_skipples} (+ %s))" % " ".join(items_all_in_these_trucks) + #], vars()) + + # "All other n-3" trucks have no skipples + items_in_other_trucks_zero = [ + "(= 0 S{i})".format(i=i) + for i in range(1, n_trucks + 1) + if i not in (x, y, z) + ] + preds += [ + "(or %s)" % " ".join(items_in_other_trucks_zero) + ] +#preds += [ +# "(or\n%s\n)" % "\n".join(skipple_preds) +#] + +# Nuzzles: max 1 per truck +for i in range(1, n_trucks + 1): + preds += fillin([ + "(>= 1 N{i})" + ], vars()) + + +# Begin generator +s = """(benchmark test.smt +:logic QF_UFLIA +:extrafuns +( +""" +s += "\n".join("(%s Int)" % x for x in literals) +s += """ +) +:formula +(and +""" +s += "\n".join(preds) +s += """ +)) +""" + +try: + import sys + print(s) + # Hack to avoid printing a ugly error in case stdin of next pipe is closed. + sys.stdout.flush() + sys.stdout.close() +except BrokenPipeError: + pass diff --git a/packing_pallets_in_trucks/pallets-to-latex.py b/packing_pallets_in_trucks/pallets-to-latex.py new file mode 100755 index 0000000..6c533d1 --- /dev/null +++ b/packing_pallets_in_trucks/pallets-to-latex.py @@ -0,0 +1,79 @@ +#!/usr/bin/env python3 +import re +import sys + +# Order of all "k" elements +order = "NPSCD" +k = len(order) + +# Weights of the elements (in the above order) +stuff = [ + (4, "Nuzzles", 700), + (-1, "Prittles", 400), + (8, "Skipples", 1000), + (10, "Crottles", 2500), + (20, "Dupples", 200), +] +weights = [item[2] for item in stuff] +counts = [item[0] for item in stuff] + +matrix = [] + +for line in sys.stdin: + line = line.strip() + if line == "unsat": + sys.exit('unsat!') + if line == "sat": + continue + m = re.match(r'([A-Z])(\d+) -> (\d+)', line) + item_type, trucknr, value = m.groups() + trucknr, value = int(trucknr), int(value) + + # Map letter to column + col = order.index(item_type) + + # auto-detect size, extending matrix size if necessary. + while len(matrix) < trucknr: + matrix.append([None] * k) + + matrix[trucknr - 1][col] = value + +# Number of trucks +n = len(matrix) + +line = " " +for col in range(k): + line += " & %5s" % order[col] +line += " & weight" +line += r" & \#pallets" +line += r" \\" +print(line) +print(r"\hline") + +for step, cells in enumerate(matrix): + # Add truck nr + line = "%2d" % (step + 1) + + # Add building blocks and calculate weight and number of pallets + weight = 0 + number_of_pallets = 0 + for col, value in enumerate(cells): + line += " & %5d" % value + number_of_pallets += value + weight += value * weights[col] + + # Add weight and number of pallets + line += " & %5d & %d" % (weight, number_of_pallets) + line += r" \\" + print(line) + +# Print the total numbers +line = " " +helperline = "% " # for displaying the expected counts +for col in range(len(matrix[0])): + total_pallets_for_item = sum(truck[col] for truck in matrix) + line += " & %5d" % total_pallets_for_item + helperline += " & %5d" % counts[col] +print(r"\hline") +print(line) +#print(helperline) diff --git a/part1.tex b/part1.tex index a54e186..0546452 100644 --- a/part1.tex +++ b/part1.tex @@ -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. -- cgit v1.2.1