## Assignment problem and Z3

I've found this at http://www.math.harvard.edu/archive/20_spring_05/handouts/assignment_overheads.pdf and took screenshot:

As in my previous examples, Z3 and SMT-solver may be overkill for the task. Simpler algorithm exists for this task (Hungarian algorithm/method).

But again, I use it to demonstrate the problem + as SMT-solvers demonstration.

Here is what I do:

#!/usr/bin/env python

from z3 import *

# this is optimization problem:
s=Optimize()

choice=[Int('choice_%d' % i) for i in range(3)]
row_value=[Int('row_value_%d' % i) for i in range(3)]

for i in range(3):

If(choice[0]==0, 250,
If(choice[0]==1, 400,
If(choice[0]==2, 350, -1))))

If(choice[1]==0, 400,
If(choice[1]==1, 600,
If(choice[1]==2, 350, -1))))

If(choice[2]==0, 200,
If(choice[2]==1, 400,
If(choice[2]==2, 250, -1))))

final_sum=Int('final_sum')

# final_sum equals to sum of all row_value[] values:

# find such a (distinct) choice[]'s, so that the final_sum would be minimal:
s.minimize(final_sum)

print s.check()
print s.model()



In plain English this means "choose such columns, so that their sum would be as small as possible.

Result is seems to be correct:

sat
[choice_0 = 1,
choice_1 = 2,
choice_2 = 0,
z3name!12 = 0,
z3name!7 = 1,
z3name!10 = 2,
z3name!8 = 0,
z3name!11 = 0,
z3name!9 = 0,
final_sum = 950,
row_value_2 = 200,
row_value_1 = 350,
row_value_0 = 400]


Again, as it is in the corresponding PDF presentation:

(However, I've no idea what "z3name" variables mean, perhaps, some internal variables?)