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).

See also: https://en.wikipedia.org/wiki/Hungarian_algorithm.

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):
    s.add(And(choice[i]>=0, choice[i]<=2))

s.add(Distinct(choice))
s.add(row_value[0]==
	If(choice[0]==0, 250, 
	If(choice[0]==1, 400, 
	If(choice[0]==2, 350, -1))))

s.add(row_value[1]==
	If(choice[1]==0, 400, 
	If(choice[1]==1, 600, 
	If(choice[1]==2, 350, -1))))

s.add(row_value[2]==
	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:
s.add(final_sum==Sum(*row_value))

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

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


( The source code: https://github.com/dennis714/yurichev.com/blob/master/blog/assign_method/1.py )

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?)


→ [list of blog posts, my twitter/facebook]

Please drop me email about any bug(s) and suggestion(s): dennis(@)yurichev.com.