Problem Statement
Five trucks, including two fridge trucks, have to deliver the following 131 items to a grocery in Brisbane using no more than twenty pallets.
- 21 bunches of bananas, 2kg per bunch
- 20 bunches of tomatoes, 1.8kg per bunch
- 25 bags of nuts, 1.2kg per bag
- 30 bags of candies, 1kg per bag
- 35 packs of milk, 0.2kg per pack
Any solution to the problem should satisfy all of the following constraints.
- Each pallet can carry no more than 8 items, with a weight limit of 10kg.
- Candies and nuts can often mix, so they should not be carried on the same pallet.
- Each truck can carry no more than 30 items, with a weight limit of 40kg.
- Milk must be cooled, so it should be carried by a fridge truck.
- Bananas are valuable, so each truck can carry no more than 5 bunches of bananas.
I am finding it difficult to find a satisfiable solver for the problem.
Confused about if I should map each item to the objects or if i should just focus on the pallets and trucks. Total beginner to z3 and satisfiability problems.
from z3 import *
total_quantity = 131
max_trucks = 5
max_pallets = 20
items = {
"bananas": (21, 2),
"tomatoes": (20, 1.8),
"nuts": (25, 1.2),
"candies": (30, 1),
"milk": (35, 0.2)
}
p = Function('p', IntSort(), IntSort(), BoolSort()) #confirms if item is in pallet
fridge = Function('fridge', IntSort(), BoolSort()) #confirms if its a fridge truck
s = Solver()
# Set Fridge Trucks
constraint_data = [fridge(i) for i in range(max_trucks)]
s.add(Sum(constraint_data) == 2)
# Set Maximum number of pallets as 20
constraint_data = Or([p(item,pallet) for item in range(total_quantity) for pallet in range(max_pallets)])
s.add(Sum(constraint_data) <= max_pallets)
# Constraint1 - Set Pallet Capacity
for pallet in range(max_pallets):
quantity_constraint_data = [p(item, pallet) for item in range(total_quantity)]
weight_constraint_data = []
Problem Statement
Five trucks, including two fridge trucks, have to deliver the following 131 items to a grocery in Brisbane using no more than twenty pallets.
- 21 bunches of bananas, 2kg per bunch
- 20 bunches of tomatoes, 1.8kg per bunch
- 25 bags of nuts, 1.2kg per bag
- 30 bags of candies, 1kg per bag
- 35 packs of milk, 0.2kg per pack
Any solution to the problem should satisfy all of the following constraints.
- Each pallet can carry no more than 8 items, with a weight limit of 10kg.
- Candies and nuts can often mix, so they should not be carried on the same pallet.
- Each truck can carry no more than 30 items, with a weight limit of 40kg.
- Milk must be cooled, so it should be carried by a fridge truck.
- Bananas are valuable, so each truck can carry no more than 5 bunches of bananas.
I am finding it difficult to find a satisfiable solver for the problem.
Confused about if I should map each item to the objects or if i should just focus on the pallets and trucks. Total beginner to z3 and satisfiability problems.
from z3 import *
total_quantity = 131
max_trucks = 5
max_pallets = 20
items = {
"bananas": (21, 2),
"tomatoes": (20, 1.8),
"nuts": (25, 1.2),
"candies": (30, 1),
"milk": (35, 0.2)
}
p = Function('p', IntSort(), IntSort(), BoolSort()) #confirms if item is in pallet
fridge = Function('fridge', IntSort(), BoolSort()) #confirms if its a fridge truck
s = Solver()
# Set Fridge Trucks
constraint_data = [fridge(i) for i in range(max_trucks)]
s.add(Sum(constraint_data) == 2)
# Set Maximum number of pallets as 20
constraint_data = Or([p(item,pallet) for item in range(total_quantity) for pallet in range(max_pallets)])
s.add(Sum(constraint_data) <= max_pallets)
# Constraint1 - Set Pallet Capacity
for pallet in range(max_pallets):
quantity_constraint_data = [p(item, pallet) for item in range(total_quantity)]
weight_constraint_data = []
3 Answers
Reset to default 2I recently learnt about Clingo ASP, and enjoy its concise and ‘elegant’ way to model such combinatorial problems.
So, here is my attempt:
It’s not as fast as Axels minizinc model w/ CP-SAT ...
(see below update for a faster model)
% --- Global Constraints ---
%%% #const total_quantity = 131.
#const max_trucks = 5.
#const max_pallets = 20.
#const fridge_trucks = 2.
#const max_items_per_pallet = 8.
#const max_weight_per_pallet = 10000. % 10kg
#const max_items_per_truck = 30.
#const max_weight_per_truck = 40000. % 40kg
#const max_bananas_per_truck = 5.
%%%%% Facts --------------------------------
item("bananas", 1..21, 2000). % 2kg each
item("tomatoes", 1..20, 1800). % 1.8kg each
item("nuts", 1..25, 1200). % 1.2kg each
item("candies", 1..30, 1000). % 1kg each
item("milk", 1..35, 200). % 0.2kg each
pallet(1..max_pallets).
truck(1..max_trucks).
%%%%% Rules --------------------------------
{ item_pallet(I, Q, P) : pallet(P) } = 1 :- item(I, Q, _).
{ pallet_truck(P, T) : truck(T) } = 1 :- item_pallet(_, _, P).
truck_pallet_item(T, P, I, Q) :- item_pallet(I, Q, P), pallet_truck(P, T).
%%%%% Constraints ---------------------------
% --- Ensure pallets' max items and max weight ---
:- pallet(P), #sum { 1, I, Q: item_pallet(I, Q, P) } > max_items_per_pallet.
:- pallet(P), #sum { Wt, I, Q: item_pallet(I, Q, P), item(I, Q, Wt) } > max_weight_per_pallet.
% --- Candies and nuts must not be on the same pallet ---
:- item_pallet("candies", _, P), item_pallet("nuts", _, P).
% --- Milk must go on a fridge truck ---
:- pallet_truck(P, T), item_pallet("milk", _, P), T > fridge_trucks.
% --- Symmetry breaking ---
:- truck_pallet_item(T, P1, I, Q1), truck_pallet_item(T, P2, I, Q2), P1 > P2, Q1 < Q2.
% --- Ensure trucks' max items and max weight ---
:- truck(T), #sum { 1, I, Q, P : item_pallet(I, Q, P), pallet_truck(P, T) } > max_items_per_truck.
:- truck(T), #sum { Wt, I, Q, P : item_pallet(I, Q, P), item(I, Q, Wt), pallet_truck(P, T) } > max_weight_per_truck.
% --- No truck can carry more than max bunches of bananas ---
:- truck(T), #sum { 1, Q : item_pallet("bananas", Q, P), pallet_truck(P, T) } > max_bananas_per_truck.
% Output ----------------------------
#show truck_pallet_item/4.
Output: (copy and paste the code to run it online)
clingo version 5.7.2 (6bd7584d)
Reading from stdin
Solving...
Answer: 1
truck_pallet_item(2,1,"bananas",5) truck_pallet_item(2,1,"tomatoes",7) truck_pallet_item(2,1,"candies",2) truck_pallet_item(2,1,"milk",1) truck_pallet_item(2,1,"milk",2) truck_pallet_item(2,1,"milk",3) truck_pallet_item(3,2,"bananas",13) truck_pallet_item(3,2,"bananas",15) truck_pallet_item(3,2,"bananas",19) truck_pallet_item(3,2,"nuts",6) truck_pallet_item(3,2,"nuts",9) truck_pallet_item(3,2,"nuts",19) truck_pallet_item(4,3,"tomatoes",9) truck_pallet_item(4,3,"candies",5) truck_pallet_item(4,3,"candies",12) truck_pallet_item(4,3,"candies",16) truck_pallet_item(4,3,"candies",18) truck_pallet_item(4,3,"candies",19) truck_pallet_item(4,3,"candies",20) truck_pallet_item(4,3,"candies",21) truck_pallet_item(5,4,"bananas",2) truck_pallet_item(5,4,"bananas",12) truck_pallet_item(5,4,"bananas",14) truck_pallet_item(5,4,"bananas",16) truck_pallet_item(5,4,"candies",7) truck_pallet_item(5,4,"candies",10) truck_pallet_item(4,5,"bananas",6) truck_pallet_item(4,5,"bananas",7) truck_pallet_item(4,5,"bananas",8) truck_pallet_item(4,5,"bananas",10) truck_pallet_item(4,5,"nuts",12) truck_pallet_item(2,6,"candies",9) truck_pallet_item(2,6,"candies",24) truck_pallet_item(2,6,"candies",26) truck_pallet_item(2,6,"milk",8) truck_pallet_item(2,6,"milk",9) truck_pallet_item(2,6,"milk",10) truck_pallet_item(2,6,"milk",12) truck_pallet_item(2,6,"milk",16) truck_pallet_item(5,7,"bananas",18) truck_pallet_item(5,7,"nuts",1) truck_pallet_item(5,7,"nuts",2) truck_pallet_item(5,7,"nuts",3) truck_pallet_item(5,7,"nuts",7) truck_pallet_item(5,7,"nuts",10) truck_pallet_item(5,7,"nuts",11) truck_pallet_item(5,8,"tomatoes",3) truck_pallet_item(5,8,"nuts",13) truck_pallet_item(5,8,"nuts",14) truck_pallet_item(5,8,"nuts",15) truck_pallet_item(5,8,"nuts",16) truck_pallet_item(5,8,"nuts",17) truck_pallet_item(5,8,"nuts",18) truck_pallet_item(4,9,"bananas",17) truck_pallet_item(4,9,"tomatoes",16) truck_pallet_item(4,9,"candies",22) truck_pallet_item(4,9,"candies",25) truck_pallet_item(4,9,"candies",28) truck_pallet_item(4,9,"candies",29) truck_pallet_item(4,9,"candies",30) truck_pallet_item(5,10,"tomatoes",6) truck_pallet_item(5,10,"tomatoes",8) truck_pallet_item(5,10,"tomatoes",15) truck_pallet_item(5,10,"nuts",23) truck_pallet_item(5,10,"nuts",24) truck_pallet_item(5,10,"nuts",25) truck_pallet_item(2,11,"bananas",11) truck_pallet_item(2,11,"nuts",4) truck_pallet_item(2,11,"nuts",5) truck_pallet_item(2,11,"nuts",8) truck_pallet_item(2,11,"milk",17) truck_pallet_item(2,11,"milk",18) truck_pallet_item(2,11,"milk",19) truck_pallet_item(2,11,"milk",20) truck_pallet_item(1,12,"bananas",1) truck_pallet_item(1,12,"bananas",3) truck_pallet_item(1,12,"bananas",4) truck_pallet_item(1,12,"bananas",9) truck_pallet_item(1,12,"nuts",21) truck_pallet_item(1,13,"tomatoes",4) truck_pallet_item(1,13,"candies",11) truck_pallet_item(1,13,"candies",13) truck_pallet_item(1,13,"milk",4) truck_pallet_item(1,14,"milk",5) truck_pallet_item(1,14,"milk",6) truck_pallet_item(1,14,"milk",7) truck_pallet_item(1,14,"milk",11) truck_pallet_item(1,14,"milk",13) truck_pallet_item(1,14,"milk",14) truck_pallet_item(1,14,"milk",15) truck_pallet_item(1,14,"milk",21) truck_pallet_item(1,15,"bananas",21) truck_pallet_item(1,15,"milk",22) truck_pallet_item(1,15,"milk",24) truck_pallet_item(1,15,"milk",25) truck_pallet_item(1,15,"milk",26) truck_pallet_item(3,16,"bananas",20) truck_pallet_item(3,16,"tomatoes",1) truck_pallet_item(3,16,"tomatoes",2) truck_pallet_item(3,16,"candies",1) truck_pallet_item(3,16,"candies",3) truck_pallet_item(3,17,"tomatoes",5) truck_pallet_item(3,17,"tomatoes",10) truck_pallet_item(3,17,"tomatoes",11) truck_pallet_item(3,17,"tomatoes",12) truck_pallet_item(3,17,"candies",4) truck_pallet_item(3,17,"candies",6) truck_pallet_item(1,18,"milk",27) truck_pallet_item(1,18,"milk",28) truck_pallet_item(1,18,"milk",29) truck_pallet_item(1,18,"milk",30) truck_pallet_item(1,18,"milk",31) truck_pallet_item(1,18,"milk",32) truck_pallet_item(1,18,"milk",33) truck_pallet_item(1,18,"milk",34) truck_pallet_item(3,19,"tomatoes",18) truck_pallet_item(3,19,"tomatoes",20) truck_pallet_item(3,19,"candies",8) truck_pallet_item(3,19,"candies",14) truck_pallet_item(3,19,"candies",15) truck_pallet_item(3,19,"candies",17) truck_pallet_item(3,19,"candies",23) truck_pallet_item(3,19,"candies",27) truck_pallet_item(2,20,"tomatoes",13) truck_pallet_item(2,20,"tomatoes",14) truck_pallet_item(2,20,"tomatoes",17) truck_pallet_item(2,20,"tomatoes",19) truck_pallet_item(2,20,"nuts",20) truck_pallet_item(2,20,"nuts",22) truck_pallet_item(2,20,"milk",23) truck_pallet_item(2,20,"milk",35)
SATISFIABLE
Models : 1+
Calls : 1
Time : 11.958s (Solving: 5.38s 1st Model: 5.38s Unsat: 0.00s)
CPU Time : 0.000s
And this second part takes the result from above to verify the assigned items and the total load on all trucks:
% --- Global Constraints ---
#const total_quantity = 131.
#const total_weight = 145000.
#const max_trucks = 5.
#const max_pallets = 20.
#const fridge_trucks = 2.
#const max_items_per_pallet = 8.
#const max_weight_per_pallet = 10000. % 10kg
#const max_items_per_truck = 30.
#const max_weight_per_truck = 40000. % 40kg
#const max_bananas_per_truck = 5.
%%%%% Facts ---------------------------------
item("bananas", 1..21, 2000). % 2kg each
item("tomatoes", 1..20, 1800). % 1.8kg each
item("nuts", 1..25, 1200). % 1.2kg each
item("candies", 1..30, 1000). % 1kg each
item("milk", 1..35, 200). % 0.2kg each
truck(1..max_trucks).
% --- Input truck_pallet_item from previous step ---
% Example input (paste actual output from Step 1):
% truck_pallet_item(1, 3, "bananas", 2). = truck 1, pallet 3, bananas, batch #3
% truck_pallet_item(1, 3, "tomatoes", 5).
% ...
truck_pallet_item(1,12,"bananas",1). truck_pallet_item(1,12,"bananas",3). truck_pallet_item(1,12,"bananas",4). truck_pallet_item(1,12,"bananas",9). truck_pallet_item(1,12,"nuts",21).
truck_pallet_item(1,13,"tomatoes",4). truck_pallet_item(1,13,"candies",11). truck_pallet_item(1,13,"candies",13). truck_pallet_item(1,13,"milk",4).
truck_pallet_item(1,14,"milk",5). truck_pallet_item(1,14,"milk",6). truck_pallet_item(1,14,"milk",7). truck_pallet_item(1,14,"milk",11). truck_pallet_item(1,14,"milk",13). truck_pallet_item(1,14,"milk",14). truck_pallet_item(1,14,"milk",15). truck_pallet_item(1,14,"milk",21).
truck_pallet_item(1,15,"bananas",21). truck_pallet_item(1,15,"milk",22). truck_pallet_item(1,15,"milk",24). truck_pallet_item(1,15,"milk",25). truck_pallet_item(1,15,"milk",26).
truck_pallet_item(1,18,"milk",27). truck_pallet_item(1,18,"milk",28). truck_pallet_item(1,18,"milk",29). truck_pallet_item(1,18,"milk",30). truck_pallet_item(1,18,"milk",31). truck_pallet_item(1,18,"milk",32). truck_pallet_item(1,18,"milk",33). truck_pallet_item(1,18,"milk",34).
truck_pallet_item(2,1,"bananas",5). truck_pallet_item(2,1,"tomatoes",7). truck_pallet_item(2,1,"candies",2). truck_pallet_item(2,1,"milk",1). truck_pallet_item(2,1,"milk",2). truck_pallet_item(2,1,"milk",3).
truck_pallet_item(2,6,"candies",9). truck_pallet_item(2,6,"candies",24). truck_pallet_item(2,6,"candies",26). truck_pallet_item(2,6,"milk",8). truck_pallet_item(2,6,"milk",9). truck_pallet_item(2,6,"milk",10). truck_pallet_item(2,6,"milk",12). truck_pallet_item(2,6,"milk",16).
truck_pallet_item(2,11,"bananas",11). truck_pallet_item(2,11,"nuts",4). truck_pallet_item(2,11,"nuts",5). truck_pallet_item(2,11,"nuts",8). truck_pallet_item(2,11,"milk",17). truck_pallet_item(2,11,"milk",18). truck_pallet_item(2,11,"milk",19). truck_pallet_item(2,11,"milk",20).
truck_pallet_item(2,20,"tomatoes",13). truck_pallet_item(2,20,"tomatoes",14). truck_pallet_item(2,20,"tomatoes",17). truck_pallet_item(2,20,"tomatoes",19). truck_pallet_item(2,20,"nuts",20). truck_pallet_item(2,20,"nuts",22). truck_pallet_item(2,20,"milk",23). truck_pallet_item(2,20,"milk",35).
truck_pallet_item(3,2,"bananas",13). truck_pallet_item(3,2,"bananas",15). truck_pallet_item(3,2,"bananas",19). truck_pallet_item(3,2,"nuts",6). truck_pallet_item(3,2,"nuts",9). truck_pallet_item(3,2,"nuts",19).
truck_pallet_item(3,16,"bananas",20). truck_pallet_item(3,16,"tomatoes",1). truck_pallet_item(3,16,"tomatoes",2). truck_pallet_item(3,16,"candies",1). truck_pallet_item(3,16,"candies",3).
truck_pallet_item(3,17,"tomatoes",5). truck_pallet_item(3,17,"tomatoes",10). truck_pallet_item(3,17,"tomatoes",11). truck_pallet_item(3,17,"tomatoes",12). truck_pallet_item(3,17,"candies",4). truck_pallet_item(3,17,"candies",6).
truck_pallet_item(3,19,"tomatoes",18). truck_pallet_item(3,19,"tomatoes",20). truck_pallet_item(3,19,"candies",8). truck_pallet_item(3,19,"candies",14). truck_pallet_item(3,19,"candies",15). truck_pallet_item(3,19,"candies",17). truck_pallet_item(3,19,"candies",23). truck_pallet_item(3,19,"candies",27).
truck_pallet_item(4,3,"tomatoes",9). truck_pallet_item(4,3,"candies",5). truck_pallet_item(4,3,"candies",12). truck_pallet_item(4,3,"candies",16). truck_pallet_item(4,3,"candies",18). truck_pallet_item(4,3,"candies",19). truck_pallet_item(4,3,"candies",20). truck_pallet_item(4,3,"candies",21).
truck_pallet_item(4,5,"bananas",6). truck_pallet_item(4,5,"bananas",7). truck_pallet_item(4,5,"bananas",8). truck_pallet_item(4,5,"bananas",10). truck_pallet_item(4,5,"nuts",12).
truck_pallet_item(4,9,"bananas",17). truck_pallet_item(4,9,"tomatoes",16). truck_pallet_item(4,9,"candies",22). truck_pallet_item(4,9,"candies",25). truck_pallet_item(4,9,"candies",28). truck_pallet_item(4,9,"candies",29). truck_pallet_item(4,9,"candies",30).
truck_pallet_item(5,4,"bananas",2). truck_pallet_item(5,4,"bananas",12). truck_pallet_item(5,4,"bananas",14). truck_pallet_item(5,4,"bananas",16). truck_pallet_item(5,4,"candies",7). truck_pallet_item(5,4,"candies",10).
truck_pallet_item(5,7,"bananas",18). truck_pallet_item(5,7,"nuts",1). truck_pallet_item(5,7,"nuts",2). truck_pallet_item(5,7,"nuts",3). truck_pallet_item(5,7,"nuts",7). truck_pallet_item(5,7,"nuts",10). truck_pallet_item(5,7,"nuts",11).
truck_pallet_item(5,8,"tomatoes",3). truck_pallet_item(5,8,"nuts",13). truck_pallet_item(5,8,"nuts",14). truck_pallet_item(5,8,"nuts",15). truck_pallet_item(5,8,"nuts",16). truck_pallet_item(5,8,"nuts",17). truck_pallet_item(5,8,"nuts",18).
truck_pallet_item(5,10,"tomatoes",6). truck_pallet_item(5,10,"tomatoes",8). truck_pallet_item(5,10,"tomatoes",15). truck_pallet_item(5,10,"nuts",23). truck_pallet_item(5,10,"nuts",24). truck_pallet_item(5,10,"nuts",25).
%%%%% Rules ---------------------------------
pallet_items_weight(P, Count, Weight) :-
truck_pallet_item(_, P, _, _),
Weight = #sum{Wt, I, Q : truck_pallet_item(_, P, I, Q), item(I, _, Wt)},
Count = #sum{1, I, Q : truck_pallet_item(_, P, I, Q)}.
truck_pallets_items_weight(T, Pallets, Items, Weight) :-
truck_pallet_item(T, _, _, _),
Weight = #sum{Wt, I, P, Q : truck_pallet_item(T, P, I, Q), item(I, _, Wt)},
Items = #sum{1, I, P, Q : truck_pallet_item(T, P, I, Q)},
Pallets = #sum{1, P : truck_pallet_item(T, P, _, _)}.
%%%%% Test ----------------------------------
% --- Total number of items on all trucks must match the global constraint
total_items_on_trucks(TotalItems) :- TotalItems = #sum { Count, T, P : truck_pallets_items_weight(T, P, Count, _) }.
:- total_items_on_trucks(TotalItems), TotalItems != total_quantity.
% --- Total weight of items on all trucks must match the global constraint
total_weight_assigned(TotalWeight) :- TotalWeight = #sum { Wt, T, P, I, Q : truck_pallet_item(T, P, I, Q), item(I, _, Wt) }.
:- total_weight_assigned(TotalWeight), TotalWeight != total_weight.
%%%%% Output --------------------------------
%%% #show pallet_items_weight/3.
%%% #show truck_pallets_items_weight/4.
#show total_weight_assigned/1.
#show total_items_on_trucks/1.
Output: confirms constraints are satisfied …
clingo version 5.7.2 (6bd7584d)
Reading from stdin
Solving...
Answer: 1
total_items_on_trucks(131) total_weight_assigned(145000)
SATISFIABLE
Models : 1
Calls : 1
Time : 0.096s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
CPU Time : 0.000s
Observations:
- same as Kiran:
constraint "milk must be placed only in the fridge trucks" causes the solver to get stuck in a loop (or more precisely: I stopped before solver were able to answer)- same as Axel:
no problem at all ... after adding a symmetry breaking constraint ;-)
Update (April):
I previously felt that the Clingo model above behaved and performed similarly to those shared by other posters, so I hadn’t put much effort into improving it.
However, earlier today, I came up with an idea to simplify the predicate for the items:
item(bananas, 21, 2000). % 2kg each
item(tomatoes, 20, 1800). % 1.8kg each
item(nuts, 25, 1200). % 1.2kg each
item(candies, 30, 1000). % 1kg each
item(milk, 35, 200). % 0.2kg each
- after modifying the item predicate and adjusting the related rules and constraints, the solver produces the same output in under 0.4 sec.
- no symmetry breaking constraint required
Output:
clingo version 5.7.2 (6bd7584d)
Reading from stdin
Solving...
Answer: 1
truck_pallet_item(3,1,candies,3) truck_pallet_item(3,1,candies,5) truck_pallet_item(5,2,bananas,1) truck_pallet_item(5,2,tomatoes,1) truck_pallet_item(5,2,tomatoes,2) truck_pallet_item(4,3,candies,8) truck_pallet_item(4,4,candies,8) truck_pallet_item(1,5,candies,2) truck_pallet_item(1,5,milk,6) truck_pallet_item(2,6,milk,8) truck_pallet_item(1,7,milk,8) truck_pallet_item(5,8,bananas,2) truck_pallet_item(5,8,nuts,5) truck_pallet_item(2,9,milk,8) truck_pallet_item(1,10,tomatoes,3) truck_pallet_item(1,10,milk,5) truck_pallet_item(4,11,tomatoes,5) truck_pallet_item(2,12,tomatoes,2) truck_pallet_item(2,12,nuts,5) truck_pallet_item(2,13,bananas,1) truck_pallet_item(2,13,bananas,4) truck_pallet_item(5,14,tomatoes,5) truck_pallet_item(1,15,tomatoes,2) truck_pallet_item(1,15,bananas,3) truck_pallet_item(5,16,nuts,7) truck_pallet_item(3,17,bananas,3) truck_pallet_item(3,17,candies,4) truck_pallet_item(3,18,nuts,4) truck_pallet_item(3,19,bananas,2) truck_pallet_item(3,19,nuts,4) truck_pallet_item(4,20,bananas,1) truck_pallet_item(4,20,bananas,4)
SATISFIABLE
Models : 1+
Calls : 1
Time : 0.383s (Solving: 0.03s 1st Model: 0.03s Unsat: 0.00s)
CPU Time : 0.000s
Here is my z3py model. It found a solution after 327s. The "sat.threads" parameter does not help here to activate multithreading. A run with a limit of 19 rather than 20 pallets required 204s.
# import essential functions only to keep debugging list tidy
from z3 import (
And,
If,
Int,
Or,
sat,
set_param,
Solver,
Sum)
import time
started = time.time()
# these parameters appear to have no influence
set_param("parallel.enable", True)
set_param("parallel.threads.max", 8)
set_param("sat.threads", 8)
max_trucks = 5
max_pallets = 20
fridge_trucks = 2
items = {
"bananas": (21, 2),
"tomatoes": (20, 1.8),
"nuts": (25, 1.2),
"candies": (30, 1),
"milk": (35, 0.2)
}
debug_output = False
if debug_output:
max_trucks = 3
max_pallets = 2
fridge_trucks = 1
items = {
"bananas": (1, 2),
"tomatoes": (0, 1.8),
"nuts": (2, 1.2),
"candies": (1, 1),
"milk": (1, 0.2)
}
total_quantity = sum([v[0] for v in items.values()])
# Shorthands for commonly used ranges
Trucks = range(max_trucks)
Pallets = range(max_pallets)
Items = range(total_quantity)
Bunches = range(len(items))
s = Solver()
s.set("modelpletion", True)
# define a Z3 Int decision variable and delimit its range
def Var(name, max):
_v = Int(name)
s.add(0 <= _v, _v <= max)
return _v
# palettes are assigned to trucks
pallets_trucks = [ Var(f"pt{p}", max_trucks - 1) for p in Pallets ]
# number of items on any pallet
pallets_items_count = [ Var(f"pc{p}", 8) for p in Pallets]
# weight in grams on any pallet (avoiding non-integers)
pallets_weight = [ Var(f"pw{p}", 10 * 1000) for p in Pallets]
# every bunch is assigned to one pallet
items_pallets = [ Var(f"ip{i}", max_pallets - 1) for i in Items ]
# array to register, which bunch type an items belongs to
items_type = []
bunch_names = []
_bunch = 0
for k, v in items.items():
bunch_names.append(k)
for _ in range(v[0]):
items_type.append(_bunch)
_bunch += 1
def BunchWeight(bunch):
# store the weight in grams to avoid Real math
return int(items[bunch_names[bunch]][1] * 1000)
def ItemName(item):
return bunch_names[ItemType(item)]
def ItemType(item):
return items_type[item]
def ItemWeight(item):
return BunchWeight(ItemType(item))
def Iff(condition, true_val = 1):
return If(condition, true_val, 0)
def B2i(condition):
return If(condition, 1, 0)
# return a range of item indices for a given (string) kind
def KindItems(kind):
return (i for i in Items if ItemName(i) == kind)
# Like KindItems() but by index rather than by kind name
def BunchItems(bunch):
return (i for i in Items if ItemType(i) == bunch)
# Each pallet can carry no more than 8 items, with a weight limit of 10kg (= 10 * 1000g)
# Allowed variable range is delimited in Var()
for p in Pallets:
s.add(pallets_items_count[p] ==
Sum([B2i(p == items_pallets[i])
for i in Items]))
s.add(pallets_weight[p] ==
Sum([Iff(p == items_pallets[i], ItemWeight(i))
for i in Items]))
# Candies and nuts can often mix, so they should not be carried on the same pallet.
for c in KindItems("candies"):
for n in KindItems("nuts"):
s.add(items_pallets[c] != items_pallets[n])
# Each truck can carry no more than 30 items, with a weight limit of 40kg.
for _truck in Trucks:
s.add(30 >= Sum([Iff(pallets_trucks[p] == _truck, pallets_items_count[p])
for p in Pallets]))
s.add(40 * 1000 >= Sum([Iff(pallets_trucks[p] == _truck, pallets_weight[p])
for p in Pallets]))
# Milk must be cooled, so it should be carried by a fridge truck.
# We assume that the fridge_trucks come first in the ordering of trucks
for m in KindItems("milk"):
for p in Pallets:
s.add(Or(p != items_pallets[m], pallets_trucks[p] < fridge_trucks))
# Bananas are valuable, so each truck can carry no more than 5 bunches of bananas.
for t in Trucks:
s.add(5 >= Sum([B2i(And(p == items_pallets[i], t == pallets_trucks[p]))
for p in Pallets for i in KindItems("bananas")]))
# Symmetry breaking to speedup solving process
# Items of the same kind are placed in pallets in sorted order
for _bunch in Bunches:
# Get quantity from dictionary
n = items[bunch_names[_bunch]][0]
if n > 0:
# The first item index for bunch
n0 = next(BunchItems(_bunch))
for i in range(n0, n0 + n - 1):
s.add(items_pallets[i] <= items_pallets[i + 1])
#
#
# Helper functions for solution output
#
def EvalInt(model, var):
# All our variable can be evaluated as_long()
return model[var].as_long()
def PalletBunches(model, pallet, bunch):
return sum([(EvalInt(model, items_pallets[i]) == pallet) for i in BunchItems(bunch)])
def PalletItems(model, pallet):
return sum([(EvalInt(model, items_pallets[i]) == pallet) for i in Items]);
def PalletWeight(model, pallet):
return sum([(EvalInt(model, items_pallets[i]) == pallet) * ItemWeight(i) for i in Items]);
def TruckItems(model, truck):
return sum([(EvalInt(model, pallets_trucks[p]) == truck) * PalletItems(model, p) for p in Pallets]);
def TruckWeight(model, truck):
return sum([(EvalInt(model, pallets_trucks[p]) == truck) * PalletWeight(model, p) for p in Pallets]);
def ShowTruckPallets(model):
print("\nPallets for trucks:")
print("Truck Items Weight Pallets assigned")
for truck in Trucks:
line = ""
if TruckItems(model, truck) == 0:
line = f" [truck {truck+1} is empty and won't be used]"
else:
for pallet in Pallets:
if (EvalInt(model, pallets_trucks[pallet]) == truck) and \
(EvalInt(model, pallets_items_count[pallet]) > 0):
line = line + f"{pallet + 1:3}"
print(f" {truck+1}{TruckItems(model, truck):8}{TruckWeight(model, truck):8}g {line}")
print("")
def ShowPalletBunches(model):
print("\nBunches for pallets: ")
print("Pallet Items Weight Bunches assigned")
for pallet in Pallets:
line = ""
if PalletItems(model, pallet) == 0:
line = f"[pallet {pallet+1} is empty and won't be used]"
else:
for bunch in Bunches:
if PalletBunches(model, pallet, bunch) > 0:
line = line + f"{PalletBunches(model, pallet, bunch)} x {bunch_names[bunch]} "
bunch += 1
print(f"{pallet+1:3}{PalletItems(model, pallet):8}{PalletWeight(model, pallet):8}g {line}")
print("")
def ShowResult(model):
ShowTruckPallets(model)
ShowPalletBunches(model)
res = s.check()
if res == sat:
ShowResult(s.model())
else:
print("No solution. Sorry!")
elapsed = time.time() - started
print(f"Execution time: {int(elapsed)} seconds")
The resulting solution:
Pallets for trucks:
Truck Items Weight Pallets assigned
1 30 26600g 2 10 13 15 16
2 29 16800g 8 9 11 20
3 16 26000g 4 6 18
4 27 37200g 1 3 5 7
5 29 38400g 12 14 17 19
Bunches for pallets:
Pallet Items Weight Bunches assigned
1 7 9600g 1 x bananas 2 x tomatoes 4 x candies
2 4 5600g 3 x tomatoes 1 x milk
3 6 8800g 2 x bananas 4 x nuts
4 6 8000g 1 x bananas 5 x nuts
5 6 9800g 1 x bananas 3 x tomatoes 2 x nuts
6 4 8000g 4 x bananas
7 8 9000g 1 x bananas 7 x candies
8 8 1600g 8 x milk
9 8 1600g 8 x milk
10 8 2600g 1 x nuts 7 x milk
11 8 3600g 2 x nuts 6 x milk
12 7 10000g 2 x bananas 5 x nuts
13 8 8200g 2 x bananas 3 x nuts 3 x milk
14 8 9000g 1 x bananas 7 x candies
15 6 5200g 5 x candies 1 x milk
16 4 5000g 2 x tomatoes 1 x nuts 1 x milk
17 6 9600g 4 x tomatoes 2 x nuts
18 6 10000g 5 x tomatoes 1 x candies
19 8 9800g 1 x bananas 1 x tomatoes 6 x candies
20 5 10000g 5 x bananas
Execution time: 327 seconds
I tackled the problem also with MiniZinc. That appears to be faster und all in all more suitable for this task.
%
% This model was only solved in 4.8s by OR Tools CP-SAT 9.12.4544
% as MiniZinc back-end with 8 threads.
% We could not find other solvers which succeeded in solving this.
%
array[int] of string: bunch_names = ["bananas", "tomatoes", "nuts", "candies", "milk"];
array[int] of int: bunch_counts = [ 21, 20, 25, 30, 35];
array[int] of int: bunch_weights = [ 2000, 1800, 1200, 1000, 200];
int: total_quantity = 131;
int: max_trucks = 5;
int: max_pallets = 20;
int: fridge_trucks = 2;
int: bunches = length(bunch_names);
% Ranges for indices
set of int: Trucks = 1..max_trucks;
set of int: Pallets = 1..max_pallets;
set of int: Items = 1..total_quantity;
set of int: Bunches = 1..bunches;
%
% Integer decision variables
%
array[Pallets] of var Trucks: pallets_trucks;
array[Pallets] of var 0..8: pallets_items_count;
array[Pallets] of var 0..10000: pallets_weights;
array[Items] of var Pallets: items_pallets;
% Recursive hack to translate item index to item type
function Bunches: ItemType(Bunches: bunch, Items: item, int: count) =
if (count + bunch_counts[bunch]) >= item then bunch
else ItemType(bunch + 1, item, count + bunch_counts[bunch])
endif;
function Bunches: ItemType(Items: i) = ItemType(1, i, 0);
% Array reduces the number of calls to ItemType()
% Have not tried if this is actually making a difference
array[Items] of Bunches: items_types = [ItemType(i) | i in Items];
function int: ItemWeight(Items: i) =
bunch_weights[items_types[i]];
function int: Iff(bool: cond, int: true_val) =
if cond then true_val else 0 endif;
function var int: Iff(var bool: cond, var int: true_val) =
if cond then true_val else 0 endif;
% Return all indices of Items matching kind
function array[int] of Items: ItemsKind(string: kind) =
[i | i in Items where bunch_names[items_types[i]] == kind];
%
% Constraints
%
% No pallet can carry more than 8 items, with a weight limit of
% 10kg (= 10 * 1000g)
% Limits are enforced in domain definitions of pallets_items_count[]
% and pallets_weights[]
constraint forall(p in Pallets) (
(pallets_items_count[p] == sum([p == items_pallets[i]
| i in Items])) /\
(pallets_weights[p] == sum([(p == items_pallets[i]) * ItemWeight(i)
| i in Items]))
);
% Candies and nuts can often mix,
% so they should not be carried on the same pallet.
constraint forall(c in ItemsKind("candies")) (
forall(n in ItemsKind("nuts")) (
items_pallets[c] != items_pallets[n]
)
);
% No truck can carry more than 30 items.
constraint forall(t in Trucks) (
30 >= sum([Iff(pallets_trucks[p] == t, pallets_items_count[p])
| p in Pallets])
);
% Weight limit per truck is 40kg = 40,000g
constraint forall(t in Trucks) (
40000 >= sum([Iff(pallets_trucks[p] == t, pallets_weights[p])
| p in Pallets])
);
% Milk must be cooled, so it should be carried by a fridge truck.
constraint forall(m in ItemsKind("milk")) (
forall(p in Pallets) (
(p != items_pallets[m]) \/
(pallets_trucks[p] <= fridge_trucks)
)
);
% Bananas are valuable, so each truck can carry no more than 5 bunches of bananas.
constraint forall(t in Trucks) (
5 >= sum([(p == items_pallets[i]) /\
(t == pallets_trucks[p]) |
p in Pallets, i in ItemsKind("bananas")])
);
% To speed up the solution, we could assign the first milk item
% to the first pallet and this pallet to the first truck,
% which is a fridge truck.
% Experiments show, that this does not give an improvement.
% constraint pallets_trucks[1] == 1;
% constraint items_pallets[ItemsKind("milk")[1]] = 1;
%
% Helper functions for solution output
%
function int: PalletBunches(Pallets: p, Bunches:b) =
count([fix(items_pallets[i]) == p | i in ItemsKind(bunch_names[b])]);
function int: PalletItems(Pallets: p) =
count([fix(items_pallets[i]) == p | i in Items]);
function int: PalletWeight(Pallets: p) =
sum([(fix(items_pallets[i]) == p) * ItemWeight(i) | i in Items]);
function int: TruckItems(Trucks: t) =
sum([(fix(pallets_trucks[p]) == t) * PalletItems(p) | p in Pallets]);
function int: TruckWeight(Trucks: t) =
sum([(fix(pallets_trucks[p]) == t) * PalletWeight(p) | p in Pallets]);
%
% Formatted output of the solution
%
output
[ "\nPallets for trucks: "] ++
[ "\nTruck Items Weight Pallets"] ++
[ if p == 1 then
"\n \(t)" ++
format(8, TruckItems(t)) ++
format(9, TruckWeight(t)) ++ "g"
else ""
endif ++
if (fix(pallets_trucks[p]) == t) /\
(fix(pallets_items_count[p]) > 0) then
format(3, p)
else ""
endif
| t in Trucks, p in Pallets
] ++
[ "\n\nBunches for pallets: "] ++
[ "\nPallet Items Weight Bunches"] ++
[ if b == 1 then
"\n" ++ format(3, p) ++
format(8, PalletItems(p)) ++
format(9, PalletWeight(p)) ++ "g " ++
if PalletItems(p) == 0 then
"[pallet \(p) is empty and won't be used]"
else ""
endif
else ""
endif ++
if PalletBunches(p, b) > 0 then
"\(PalletBunches(p, b)) x " ++ bunch_names[b] ++ " "
else ""
endif
| p in Pallets, b in Bunches
] ++
[ "\n\nPlausibility:"] ++
[ "\nTotal items: \(sum([PalletItems(p) | p in Pallets]))"] ++
[ "\nTotal weight: \(sum([PalletWeight(p) | p in Pallets]))g"]
;
The resulting solution:
I used OR Tools as back-end solver with 8 threads.
Pallets for trucks:
Truck Items Weight Pallets
1 29 27800g 1 9 12 16
2 29 14000g 5 17 18 19
3 27 39200g 2 6 10 11
4 29 34000g 3 13 14 15
5 17 30000g 4 7 8
Bunches for pallets:
Pallet Items Weight Bunches
1 5 10000g 5 x bananas
2 5 10000g 5 x bananas
3 5 10000g 5 x bananas
4 5 10000g 5 x bananas
5 8 9800g 1 x bananas 4 x tomatoes 3 x milk
6 6 10000g 5 x tomatoes 1 x candies
7 6 10000g 5 x tomatoes 1 x candies
8 6 10000g 5 x tomatoes 1 x candies
9 8 9200g 1 x tomatoes 6 x nuts 1 x milk
10 8 9600g 8 x nuts
11 8 9600g 8 x nuts
12 8 4600g 3 x nuts 5 x milk
13 8 8000g 8 x candies
14 8 8000g 8 x candies
15 8 8000g 8 x candies
16 8 4000g 3 x candies 5 x milk
17 8 1600g 8 x milk
18 8 1600g 8 x milk
19 5 1000g 5 x milk
20 0 0g [pallet 20 is empty and won't be used]
Plausibility:
Total items: 131
Total weight: 145000g
----------
==========
Finished in 4s 830msec.
This is my Z3py model for the problem. The model ran in 519 seconds on my machine.
from z3 import (
And, If, IntSort, BoolSort, Function, Solver, Sum, Not, Implies, sat
)
import time
started = time.time()
def get_packing(typ, qty):
packing = {
"bananas": "bunch",
"tomatoes": "bunch",
"nuts": "bag",
"candies": "bag",
"milk": "pack"
}
packing_text = (packing[typ] + "s" if packing[typ] != "bunch" else packing[typ] + "es") if qty > 1 else packing[typ]
return f"{qty} {packing_text}"
items = {
"bananas": (21, 2),
"tomatoes": (20, 1.8),
"nuts": (25, 1.2),
"candies": (30, 1),
"milk": (35, 0.2)
}
total_quantity = 131
max_trucks = 5
max_pallets = 20
# Mapping items to specific ranges
'''
Dictionary to create global mappig for items
{
'bananas': (0, 21),
'tomatoes': (21, 41),
'nuts': (41, 66),
'candies': (66, 96),
'milk': (96, 131)
}
'''
item_ranges = {}
current_index = 0
for t, (count, weight) in items.items():
item_ranges[t] = (current_index, current_index + count)
current_index += count
# Mapping item to corresponding type and weight
'''
Each item is mapped its weight and type for easy reference.
'''
item_type = {}
item_weight = {}
for t, (count, weight) in items.items():
start, end = item_ranges[t]
for i in range(start, end):
item_type[i] = t
item_weight[i] = weight
p = Function('p', IntSort(), IntSort(), BoolSort()) # confirms if item is in pallet
t = Function('t', IntSort(), IntSort(), BoolSort()) # confirms if pallet is in truck
fridge = Function('fridge', IntSort(), BoolSort()) # confirms if it's a fridge truck
s = Solver()
# Each item must be on exactly one pallet.
for i in range(total_quantity):
s.add(Sum([If(p(i, j), 1, 0) for j in range(max_pallets)]) == 1)
# Each pallet used assigned to exactly truck.
for j in range(max_pallets):
s.add(Sum([If(t(j, m), 1, 0) for m in range(max_trucks)]) <= 1) # max 1 truck
s.add(Implies(Sum([If(p(i, j), 1, 0) for i in range(total_quantity)]) > 0,
Sum([If(t(j, m), 1, 0) for m in range(max_trucks)]) == 1))
# Set Fridge Trucks
s.add(Sum([If(fridge(m), 1, 0) for m in range(max_trucks)]) == 2)
# Set Pallet Capacity
'''
Total number of items should be less than 8.
Total weight of items on pallet, derived from the wieght mapping,
should be less than 10.
'''
for j in range(max_pallets):
s.add(Sum([If(p(i, j), 1, 0) for i in range(total_quantity)]) <= 8)
s.add(Sum([If(p(i, j), item_weight[i], 0) for i in range(total_quantity)]) <= 10)
# Candies and nuts cannot be on the same pallet.
'''
Iterated through the candy and nuts indices to check if both of them
are not in the same pallet
'''
candies_range = range(item_ranges["candies"][0], item_ranges["candies"][1])
nuts_range = range(item_ranges["nuts"][0], item_ranges["nuts"][1])
for j in range(max_pallets):
for ci in candies_range:
for ni in nuts_range:
s.add(Not(And(p(ci, j), p(ni, j))))
# Set Truck Capacity
'''
The total quantity and weight of the objects in each pallet that is
assigned to the respective truck is checked to satisfy the constraint.
'''
for m in range(max_trucks):
s.add(Sum([If(t(j, m), Sum([If(p(i, j), 1, 0) for i in range(total_quantity)]), 0)
for j in range(max_pallets)]) <= 30)
s.add(Sum([If(t(j, m), Sum([If(p(i, j), item_weight[i], 0) for i in range(total_quantity)]), 0)
for j in range(max_pallets)]) <= 40)
# Milk must be on a fridge truck.
'''
Directly assigning Milk to Fridge trucks was causing my solver to be heavy.
So I decided on going on with the idea that if milk is present in a pallet,
then the pallet must be assigned to the fridge truck.
'''
milk_range = range(item_ranges["milk"][0], item_ranges["milk"][1])
for j in range(max_pallets):
milk_on_pallet = Sum([If(p(i, j), 1, 0) for i in milk_range])
for m in range(max_trucks):
s.add(Implies(And(milk_on_pallet > 0, t(j, m)), fridge(m)))
# Each truck can carry no more than 5 bunches of bananas.
'''
Sum of all the bananas in all the pallets assigned to the truck is
constrained to fall below 5.
'''
banana_range = range(item_ranges["bananas"][0], item_ranges["bananas"][1])
for m in range(max_trucks):
s.add(Sum([If(t(j, m), Sum([If(p(i, j), 1, 0) for i in banana_range]), 0)
for j in range(max_pallets)]) <= 5)
if s.check() == sat:
model = s.model()
print("Model present")
total_output = {item: 0 for item in items.keys()}
with open("model.txt", "w") as f:
for m in range(max_trucks):
truck_type = "Fridge" if model.evaluate(fridge(m)) else "Normal"
print(f"\n{truck_type} Truck {m+1}:", file=f)
pallet_num = 0
for j in range(max_pallets):
if model.evaluate(t(j, m)):
pallet_num += 1
pallet_items = {item: 0 for item in items.keys()}
for i in range(total_quantity):
if model.evaluate(p(i, j)):
typ = item_type[i]
pallet_items[typ] += 1
total_output[typ] += 1
print(f" Pallet {pallet_num}:", file=f)
for typ, count in pallet_items.items():
if count > 0:
print(f" {typ}: {get_packing(typ, count)}", file=f)
print("\n\nTotal Output:", total_output, file=f)
else:
print("Solver Unsatisfiable")
elapsed = time.time() - started
print(f"Execution time: {int(elapsed)} seconds")
This is the model produced by the solver.
---------------------------- MODEL PRODUCED ----------------------------
Normal Truck 1:
Pallet 1:
bananas: 2 bunches
tomatoes: 1 bunch
nuts: 3 bags
Pallet 2:
bananas: 1 bunch
tomatoes: 1 bunch
candies: 6 bags
Pallet 3:
bananas: 2 bunches
tomatoes: 1 bunch
candies: 4 bags
Pallet 4:
tomatoes: 1 bunch
nuts: 6 bags
Fridge Truck 2:
Pallet 1:
milk: 8 packs
Pallet 2:
nuts: 6 bags
milk: 2 packs
Pallet 3:
milk: 8 packs
Pallet 4:
bananas: 1 bunch
tomatoes: 2 bunches
nuts: 1 bag
milk: 2 packs
Fridge Truck 3:
Pallet 1:
milk: 8 packs
Pallet 2:
candies: 7 bags
milk: 1 pack
Pallet 3:
bananas: 4 bunches
tomatoes: 1 bunch
milk: 1 pack
Pallet 4:
bananas: 1 bunch
tomatoes: 1 bunch
nuts: 1 bag
milk: 5 packs
Normal Truck 4:
Pallet 1:
bananas: 2 bunches
tomatoes: 1 bunch
candies: 1 bag
Pallet 2:
bananas: 1 bunch
tomatoes: 3 bunches
nuts: 2 bags
Pallet 3:
bananas: 2 bunches
tomatoes: 1 bunch
nuts: 3 bags
Normal Truck 5:
Pallet 1:
tomatoes: 2 bunches
candies: 6 bags
Pallet 2:
bananas: 4 bunches
tomatoes: 1 bunch
Pallet 3:
bananas: 1 bunch
tomatoes: 2 bunches
nuts: 3 bags
Pallet 4:
tomatoes: 2 bunches
candies: 6 bags
Total Output: {'bananas': 21, 'tomatoes': 20, 'nuts': 25, 'candies': 30, 'milk': 35}
------------------------------------------------------------------------------------