z3py 优化作为从列表中选择的变量

Question

例如，如何在 z3py 中编写代码以最大化 a+b+c+d 的值，因为 a,b,c,d 都是从列表 [1,2,3,4,5,6, 7,8]，作为输入给出。 a、b、c、d 是不同的值。

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)

如何编写对应于从列表中选择“a b c d”值的代码。 a+b+c+d 的正确输出值为 26 谢谢！

Answer 1

这是一种方法：

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"

当我运行它时，我得到：

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