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)

как написать код, соответствующий выбору значения "ab 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]