使用Z3实现教师班级分配：单教师仅授一门课约束问题

首先修正你代码里的问题：class是Python关键字，不能用作参数名，改成num_classes；teacher参数同理改成num_teachers，避免命名冲突。

接下来要实现"每位教师仅教授一门课"的约束，需要先定义布尔变量矩阵x[i][j]，表示第i位教师是否教授第j个班级，然后给Z3求解器添加以下核心约束：

• 对每一位教师i，所有班级对应的布尔变量之和必须等于1（确保每位教师恰好选一门课）
• 可选约束：如果置信度为0，教师不能教授该班级（避免分配无置信度的课程）

完整代码如下：

from z3 import *

def Allocation(matrix, num_classes, num_teachers):
    solver = Solver()
    # 定义布尔变量矩阵：x[i][j] 表示第i位教师是否教授第j个班级
    x = [[Bool(f"x_{i}_{j}") for j in range(num_classes)] for i in range(num_teachers)]
    
    # 约束1：每位教师恰好教授一门课
    for i in range(num_teachers):
        solver.add(Sum([If(x[i][j], 1, 0) for j in range(num_classes)]) == 1)
    
    # 可选约束：置信度为0的班级，教师不能教授
    for i in range(num_teachers):
        for j in range(num_classes):
            if matrix[i][j] == 0:
                solver.add(Not(x[i][j]))
    
    # 最大化总置信度的优化逻辑（可选，符合实际分配需求）
    total_confidence = Sum([If(x[i][j], matrix[i][j], 0) for i in range(num_teachers) for j in range(num_classes)])
    optimizer = Optimize()
    optimizer.add(solver.assertions())
    optimizer.maximize(total_confidence)
    
    # 求解并输出结果
    if optimizer.check() == sat:
        model = optimizer.model()
        print("分配结果：")
        for i in range(num_teachers):
            for j in range(num_classes):
                if is_true(model[x[i][j]]):
                    print(f"教师{i+1} 教授班级{j+1}，置信度：{matrix[i][j]}")
        print(f"总置信度：{model.eval(total_confidence)}")
    else:
        print("无解")

# 你的置信度矩阵
confidence_matrix = [
    [5, 0, 4, 1, 1, 2, 5, 1, 2, 5, 4],
    [1, 2, 5, 3, 3, 3, 1, 0, 2, 0, 2]
]
# 调用函数：传入矩阵、班级数、教师数
Allocation(confidence_matrix, 11, 2)

代码说明 #

1. 布尔变量矩阵x用来建模教师和班级的分配关系
2. 核心约束通过Sum和If函数实现，确保每位教师仅选一门课
3. 可选的0置信度约束避免无效分配
4. 额外添加的最大化总置信度逻辑，更贴合实际授课分配的优化需求

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