PackingPallets: solved 1b

2 files changed, 45 insertions, 4 deletions

diff --git a/packing_pallets_in_trucks/generate-packingpallets.py b/packing_pallets_in_trucks/generate-packingpallets.py
index e46694d..ba81851 100755
--- a/packing_pallets_in_trucks/generate-packingpallets.py
+++ b/packing_pallets_in_trucks/generate-packingpallets.py
@@ -127,6 +127,13 @@ for i in range(1, n_trucks + 1):
         "(>= 1 N{i})"
     ], vars())
 
+if is_b:
+    # Prittles and crottles cannot both be on the same truck. Either one of them
+    # should be zero for every truck.
+    for i in range(1, n_trucks + 1):
+        preds += fillin([
+            "(or (= 0 P{i}) (= 0 C{i}))"
+        ], vars())
 
 # Begin generator
 s = """(benchmark test.smt
diff --git a/part1.tex b/part1.tex
index 0546452..b1242ce 100644
--- a/part1.tex
+++ b/part1.tex
@@ -139,7 +139,7 @@ $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}
+using the command \texttt{python generate-packingpallets.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
@@ -202,9 +202,43 @@ Ingredient~\ref{eq:truck4} takes more time (200ms).
 
 
 \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.
-This was captured by a set of constraints looping over all pallets of Crottles, and then for the Truck containing them, looping over all pallets to check whether they are not Prittles (giving us at most $10 \cdot 8 = 80$ new constraints). 
-After that, we again searched for a solution in a binary way. This time, we did not get a satisfiable solution anymore above 19 pallets of Prittles. Thus, we can take at most 19 pallets of Prittles if they may not be carried together with Crottles.
+The constraint that Prittles and Crottles cannot be transported together can be
+expressed as either one of them being zero:
+\begin{align}
+\label{eq:truckB}
+\bigwedge_{i=1}^n
+P_i = 0 \lor C_i = 0
+\end{align}
+
+The command \texttt{python generate-packingpallets.py 22 b | z3 -smt -in} does
+the same as (a), but with the additional restriction above added to the
+conjunction. After 40 seconds, it output ``unsat'' for $C_P=22$.
+
+For $C_P=21$, a satisfying assignment was found within 100 milliseconds. Its
+assignment is shown in Table~\ref{tbl:palletsInTrucksB}.
+
+
+\begin{table}[H]
+\centering
+\begin{tabular}{r|rrrrr|rr}
+   &     N &     P &     S &     C &     D & weight & \#pallets \\
+\hline
+ 1 &     0 &     0 &     2 &     2 &     4 &  7800 & 8 \\
+ 2 &     1 &     7 &     0 &     0 &     0 &  3500 & 8 \\
+ 3 &     1 &     0 &     0 &     2 &     4 &  6500 & 7 \\
+ 4 &     1 &     7 &     0 &     0 &     0 &  3500 & 8 \\
+ 5 &     0 &     0 &     2 &     2 &     4 &  7800 & 8 \\
+ 6 &     1 &     7 &     0 &     0 &     0 &  3500 & 8 \\
+ 7 &     0 &     0 &     2 &     2 &     4 &  7800 & 8 \\
+ 8 &     0 &     0 &     2 &     2 &     4 &  7800 & 8 \\
+\hline
+   &     4 &    21 &     8 &    10 &    20
+\end{tabular}
+\caption{\label{tbl:palletsInTrucksB}The assignment of pallets to trucks with
+    an additional restriction on Prittles and Crottles. 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}
 
 \section*{Problem: Chip design}
 Give a chip design containing two power components and ten regular components satisfying the following constraints: