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 = [] Continue reading...
