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.
Any solution to the problem should satisfy all of the following constraints.
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 = []
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}
------------------------------------------------------------------------------------