Python Z3 - Class allocation, how to assign a teacher to a class constraint

Please ensure that your questions or texts are complete and comprehensive. Take a few extra seconds to provide all necessary details. In this particular case, you provided an integer-valued matrix with two rows and 11 columns. While you explained the meaning of each row, you neglected to mention the meaning of the columns. Presumably, the columns represent 11 different classes, but the absence of clarifying information leaves room for alternative interpretations. Additionally, you stated that each teacher should teach exactly one class, but you did not elaborate on the objective beyond assigning classes to teachers. Consequently, the confidence coefficients of the teachers seem irrelevant and unnecessary. Based solely on the information provided, one could simply assign any of the classes to the first teacher and a different class to the second teacher. Probably you missed a sentence like "to optimize the assignment and ensure that teachers are teaching the classes they are most confident in, given the available options". Also with the current setup, it implies that at least nine classes would remain unattended by any teacher. I said at least because your text doesn't exclude the possibility of both teachers teach the same class

Ok, let's go for the two problems closer to your text. 1- Just assigning a class to each teacher. 2- Assigning a class to a teacher with a good outcome.

The first case can be formulated as a simple SAT (satisfiability) problem. Let xi_j a Boolean variable that is True if teacher i is assigned to class j. To say that for each i=1,2, only one xi_j can be True you can consider the following formula.

The inner part of the disjunction, just says that for a fixed i and j, only xi_j is True and for all other k different from j, xi_k is False. Here is one way to write a code in Python to ask Z3 to solve this. It might not be the best way, but I used list comprehension and parsing string.

from z3 import *
for i in range( 1, 2+1 ):
    for j in range( 1, 11+1 ):
        exec( f"x{i}_{j} = Bool( 'x{i}_{j}' )" )
s = Solver()
for i in range( 1, 2+1 ):
    exec( "s.add( Or( " + ", ".join( f"And( x{i}_{j}, " + ", ".join( f"Not( x{i}_{k} )" for k in range( 1, 11+1 ) if k != j ) + " )" for j in range( 1, 11+1 ) ) + " ) )" )
print( f"The problem is {s.check()}. " )
if s.check() == sat:
    print( f"An answer is {s.model()}" )

The result is sat and the model has all variables False except x1_11 and x2_11 which means z3 just let both teachers choose class 11. There's nothing to be surprised, the condition that each teacher only have 1 class is satisfied.

The second case is not just a SAT (satisfiability) problem, it becomes an optimization problem. Denote your matrix with M. The confidence of teacher 1 for all of the classes he teaches is the summation of the product of the confidence coefficients to the Boolean variables x1_j where they are treated as binary instead of True/False. Well, you can use the average instead of summation, but they are scalar multiple of each other so maximizing one of them is maximizing the other one as well. So your two target functions are the followings.

But note none of the two functions obtain negative values so let's combine them into one target function. One way is to just simply add the two target functions.

Instead of calling Solver, we will call Optimize. In addition to .add for giving the constraints, we will use .maximize for giving the target function.

from z3 import *

M = [ [ 5, 0, 4, 1, 1, 2, 5, 1, 2, 5, 4 ], [ 1, 2, 5, 3, 3, 3, 1, 0, 2, 0, 2 ] ]

for i in range( 1, 2+1 ):
    for j in range( 1, 11+1 ):
        exec( f"x{i}_{j} = Bool( 'x{i}_{j}' )" )
o = Optimize()
exec( "o.maximize( " + " + ".join( " + ".join( f"{M[ i-1 ][ j-1 ]} * x{i}_{j}" for j in range( 1, 11+1 ) ) for i in range( 1, 2+1 ) ) + " )" )
for i in range( 1, 2+1 ):
    exec( "o.add( Or( " + ", ".join( f"And( x{i}_{j}, " + ", ".join( f"Not( x{i}_{k} )" for k in range( 1, 11+1 ) if k != j ) + " )" for j in range( 1, 11+1 ) ) + " ) )" )
print( f"The problem is {o.check()}. " )
if o.check() == sat:
    print( f"An answer is {o.model()}" )

It is sat and asks only x1_7 and x2_3 to be True where the confidence coefficient of both teachers are 5 (max). To treat the question as an optimization with multiple objectives, you can add the target functions separately, see the following link.

https://theory.stanford.edu/~nikolaj/programmingz3.html#sec-multiple-objectives

If you are not familiar with how to use z3, other than the above link you can watch the following short video.

https://youtu.be/rTVNvZx83IE

But as an optimization problem you don't need to necessarily use z3. You can treat xi_js as binary not only in the target function, but also in the constraints, then having exactly one of x1_js equal to 1 is equivalent with x1_1+x1_2+...+x1_11=1. So you are dealing with a linear binary optimization as the following.

You can use any optimization package that supports linear binary optimization such as scipy. Not that the scipy.optimize.linprog assumes the problem is a minimization, so you need to multiply the coefficients of your target function to minus one, also remember that you have 2*11=22 variables.

from scipy.optimize import linprog

M = [ [ 5, 0, 4, 1, 1, 2, 5, 1, 2, 5, 4 ], [ 1, 2, 5, 3, 3, 3, 1, 0, 2, 0, 2 ] ]

target = []
for i in range( 2 ):
    target.extend( [ - M[ i ][ j ] for j in range( 11 ) ] )
A = [ [ 0 for j in range( 2 * 11 ) ] for i in range( 2 ) ]
for i in range( 2 ):
    for j in range( 11 ):
        A[ i ][ i * 11 + j ] = 1
b = [ 1 for i in range( 2 ) ]
problem = linprog( c = target, A_eq = A, b_eq = b, integrality = [ 1 for i in range( 2 * 11 ) ], bounds = [ ( 0, 1 ) for i in range( 2 * 11 ) ], method = 'highs' )
print( f"The maximum is {problem.fun} for the assignment {list( problem.x )}." )

The result says teacher 1 teaches class 1 and teacher 2 teaches class 3. Again both got classes where they have confidence coefficient 5.

If you are not familiar with scipy.optimize.linprog, the following short video is a good place to check.

https://youtu.be/GN3N3MEn_ps