练习:
求集合 Z 中加起来为 4285 的最小元素数。
哪里Z = { w(i): w(n) - n^2 - n + 1, i = 1,2,...,30 }
我创建了一个解决方案:
def f(t):
return t ** 2 - t + 1
opt = z3.Optimize()
x = IntVector('x', 30)
x_val = [And(x[i] >= 0, x[i] <= 1) for i in range(30)]
opt.add(x_val)
m = [x[i] * f(i + 1) for i in range(30)]
m_sum = z3.Sum(m)
opt.add(m_sum == 4285)
opt.minimize(z3.Sum(x))
if z3.sat == opt.check():
model = opt.model()
print(model)
但是运行速度太慢了。仅适用于少量。我该如何改进?
最佳答案
在 z3 中用整数表示 bool 值几乎总是一个坏主意。因此,不要使用您所说的项目介于 0-1 之间的整数向量,而只需使用 bool 向量和 If
构造即可。像这样的事情:
from z3 import *
def f(t):
return t ** 2 - t + 1
opt = z3.Optimize()
x = BoolVector('x', 30)
m = [If(x[i], f(i + 1), 0) for i in range(30)]
m_sum = z3.Sum(m)
opt.add(m_sum == 4285)
opt.minimize(z3.Sum([If(x[i], 1, 0) for i in range(30)]))
if z3.sat == opt.check():
model = opt.model()
print(model)
当我运行它时,它运行得非常快并找到解决方案:
[x__0 = False,
x__1 = False,
x__2 = False,
x__3 = False,
x__4 = False,
x__5 = False,
x__6 = False,
x__7 = False,
x__8 = False,
x__9 = False,
x__10 = False,
x__11 = False,
x__12 = False,
x__13 = True,
x__14 = False,
x__15 = False,
x__16 = False,
x__17 = True,
x__18 = False,
x__19 = False,
x__20 = False,
x__21 = False,
x__22 = False,
x__23 = False,
x__24 = False,
x__25 = True,
x__26 = True,
x__27 = True,
x__28 = True,
x__29 = True]
我没有检查这是否是正确的解决方案,但至少它应该让您开始!
关于python - 使用 z3py 查找集合中元素的最小数量,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/61545360/