使用Python Z3求解物流调度SAT问题时遇到困惑，请求建模指导

问题描述 #

有5辆卡车（包含2辆冷藏车）需要向布里斯班的一家杂货店运送总计131件商品，最多使用20个托盘。具体商品明细如下：

• 21串香蕉，每串2kg
• 20串番茄，每串1.8kg
• 25袋坚果，每袋1.2kg
• 30袋糖果，每袋1kg
• 35包牛奶，每包0.2kg

所有解决方案必须满足以下约束条件：

• 每个托盘最多装8件商品，重量上限为10kg
• 糖果和坚果不能放在同一个托盘上
• 每辆卡车最多装30件商品，重量上限为40kg
• 牛奶必须由冷藏车运输
• 香蕉价值高，每辆卡车最多装5串香蕉

我的困惑与当前尝试 #

我很难找到这个问题的可行求解器，现在特别困惑：应该把每件商品单独映射为对象来建模，还是只聚焦于托盘和卡车的整体分配逻辑？我是Z3和可满足性问题的纯新手。

以下是我目前写的代码片段：

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 = []

备注：内容来源于stack exchange，提问作者Kiran CJ