Assignment problem and Z3

I've found this at 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:

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:

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

	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 equals to sum of all row_value[] values:

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

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

( The source code: )

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

Result is seems to be correct:

[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(@)