summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorPeter Wu <peter@lekensteyn.nl>2016-12-14 19:37:35 +0100
committerPeter Wu <peter@lekensteyn.nl>2016-12-14 19:37:35 +0100
commit61af52b0328d1a875af998fd0ead513ee14eb503 (patch)
tree40525137637fd960635c61809b6d83c13cfc5283
parent7eef4433fdea705038cbc504005ea74d502b7d53 (diff)
download2IMF25-AR-61af52b0328d1a875af998fd0ead513ee14eb503.tar.gz
PackingPallets; redid 1a
A bit more formal and generalized.
-rwxr-xr-xpacking_pallets_in_trucks/generate-packingpallets.py155
-rwxr-xr-xpacking_pallets_in_trucks/pallets-to-latex.py79
-rw-r--r--part1.tex151
3 files changed, 376 insertions, 9 deletions
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.