如何修改Z3优化代码以基于代理索引而非值做分配优化？

问题描述 #

4个代理对应4类工作，initial矩阵为代理执行各工作的价格（行代表代理，列代表工作）。现有Z3 Optimize代码能求解最小总执行价格，但输出结果是工作价格值，需求改为输出代理对应的工作索引分配（即每个代理被分配到哪类工作的列索引），同时保证总价格最小。

现有代码（输出价格值，不符合需求） #

import itertools
from z3 import *

initial = (  # Row - agent, Column - work
    (7, 7, 3, 6),
    (4, 9, 5, 4),
    (5, 5, 4, 5),
    (6, 4, 7, 2)
)

opt = Optimize()    

agent = [Int(f"a_{i}") for i, _ in enumerate(initial)]
opt.add(And(*(a != b for a, b in itertools.combinations(agent, 2))))

for w, row in zip(agent, initial):
    opt.add(Or(*[w == val for val in row]))

minTotal = Int("minTotal")
opt.add(minTotal == sum(agent))
opt.minimize(minTotal)
print(opt.check())
print(opt.model())

当前输出示例：[a_2 = 4, a_1 = 5, a_3 = 2, a_0 = 3, minTotal = 14]，其中a_i的值是工作价格，而非需要的工作索引。

修改后的代码（输出工作索引分配） #

from z3 import *

initial = (  # Row - agent, Column - work
    (7, 7, 3, 6),
    (4, 9, 5, 4),
    (5, 5, 4, 5),
    (6, 4, 7, 2)
)

num_agents = len(initial)
num_works = len(initial[0])

opt = Optimize()

# 每个变量代表对应代理分配到的工作索引（0~3）
agent_work = [Int(f"agent_{i}_work") for i in range(num_agents)]

# 约束1：每个代理的工作索引在合法范围内
for work_idx in agent_work:
    opt.add(And(work_idx >= 0, work_idx < num_works))

# 约束2：所有代理分配的工作互不重复（每个工作仅一个代理负责）
opt.add(Distinct(agent_work))

# 计算总执行价格：每个代理执行对应工作的价格之和
total_cost = sum(initial[i][agent_work[i]] for i in range(num_agents))

# 最小化总价格
opt.minimize(total_cost)

# 求解并输出结果
if opt.check() == sat:
    model = opt.model()
    print("代理-工作索引分配：")
    for i in range(num_agents):
        work_idx = model.eval(agent_work[i])
        print(f"代理 {i} → 工作 {work_idx}，价格：{initial[i][int(work_idx)]}")
    print(f"最小总价格：{model.eval(total_cost)}")
else:
    print("无解")

关键修改说明 #

1. 变量定义变更：将原来存储工作价格的变量，改为存储工作索引，直接对应需求的分配结果。
2. 约束调整：
   • 新增索引范围约束，确保工作索引在合法的列范围内；
   • 使用Distinct约束保证所有代理分配的工作互不重复，符合一对一分配规则。
3. 总价格计算：通过索引从initial矩阵中取出对应价格求和，替代原来直接对价格变量求和的逻辑。
4. 结果输出：直接提取每个代理对应的工作索引，并展示对应价格，结果更直观。

内容的提问来源于stack exchange，提问作者Dewfy