Python Z3 - 班级分配，如何将教师分配给班级约束

Question

我有一个矩阵看起来像

[[5, 0, 4, 1, 1, 2, 5, 1, 2, 5, 4],

[1, 2, 5, 3, 3, 3, 1, 0, 2, 0, 2]]

每一行是一位老师，数字代表他们对课堂教学的信心。应该添加的约束是老师只能教一门课。

我试过这样做：

def Allocation(matrix, class, teacher, k):
  solver = Solver()
  teacherConfidence = {}
  for i in range(class):
    teacher = f"Teacher{i+1}"
    teacherConfidence[teacher] = matrix[i]
  print (teacherConfidence)

但我不知道如何告诉求解器说“每个老师应该只教一门课”