如何提高z3的优化速度？

Question

我使用Z3求解线性优化，但是随着变量和约束的增加，求解时间难以忍受。未来变量个数约为35940个，约束可能超过十万个。 有没有办法提高速度？

from z3 import *
opt = Optimize()
cost=Int('cost')

[varibles and constraints]

set_option(max_args=1000000)
set_option(max_lines=1000000)
h=opt.minimize(cost)
print(opt.check())
m=opt.model()
print (m)
print(opt.lower(h))
doc=open('result.txt','w')
print(opt.model(),file=doc)

Answer 1

正如所提出的，这个问题是无法回答的。您没有提及约束的性质（它们是线性的、简单的等式，只有 1-0 吗？），也没有提及应用程序域本身。请记住，z3 的优化器是一个非常通用的“锤子”。是的，它会优化你的线性约束，但它的亮点在于理论上的组合，而不是它的速度。如果您的域具有自定义优化算法，则无论如何都应该使用它。使用 40K 变量和 100K 约束，除非它们都是布尔值且相当琐碎，否则我不希望 z3 表现得那么好。但话又说回来，这一切都取决于这些约束的性质。

话虽如此，通读 z3 优化论文是了解其内部工作原理的最佳选择；它至少可以帮助您决定是否应该投资自定义算法。见这里：https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/nbjorner-nuz.pdf