z3py optimization as variables chosen from a list

Question

For the example, how to write code in z3py to maximize value of a+b+c+d as a,b,c,d are all chosen from list [1,2,3,4,5,6,7,8], which is given as the input. a, b, c, d are distinct values.

a, b, c, d = Ints("a b c d")
o = Optimize()
list = [1,2,3,4,5,6,7,8]
o.maximize(a+b+c+d)

how to write code corresponding to choose "a b c d" value from list. The correct out value of a+b+c+d is 26 Thanks!

alias alias · Accepted Answer · 2020-02-18T16:44:56

Here's one way:

from z3 import *

a, b, c, d = Ints("a b c d")
o = Optimize()

list = [1,2,3,4,5,6,7,8]
vars = [a, b, c, d]

for v in vars:
    o.add(Or([v == e for e in list]))

o.add(Distinct(*vars))

goal = Int("goal")
o.add(goal == a+b+c+d)

o.maximize(goal)
if o.check() == sat:
    print o.model()
else:
    print "not satisfiable"

When I run this, I get:

$ python a.py
[d = 5, c = 8, b = 6, a = 7, goal = 26]

z3py optimization as variables chosen from a list

1 Answers