Z3PY 非常慢，有很多变量？

Question

我一直在使用 Z3PY 中的优化器，并且在我的项目中只使用 Z3 ints 和 (x

我创建了 26 个 Z3 整数。然后我添加了硬约束，它不应小于 1 或大于 26。此外，所有数字都必须是唯一的。根本没有添加其他约束。 换句话说，求解器将找到的解决方案是一个简单的顺序 [1,2,3,4,5....最多 26]。以求解器发现的方式排序。

我的意思是这是一件简单的事情，除了我提到的那些之外，真的没有任何限制。求解器在 0.4 秒或类似的时间内解决了这个问题，快速且足够。这是预期的。但是如果我将变量的数量增加到 49（当然现在的约束是它不应低于 1 或超过 49），求解器大约需要 1 分钟才能求解。对于这么简单的任务，这似乎真的很慢？应该是这样吗，有人知道吗？时间复杂度真的大大增加了吗？

（我知道我可以在这个特定的实验中使用 Solver() 而不是 Optimizer()，它会在一秒钟内解决，但实际上我需要使用 Optimizer 来完成，因为我有很多软限制工作。）

编辑：为我的示例添加一些代码。

I declare an array with Z3 ints that I call "reqs".
The array is consisting of 26 variables in one example and 49 in the other example I am talking about.

solver = Optimize()

 for i in (reqs):
     solver.add(i >= 1)

for i in (reqs):
    solver.add(i <= len(reqs))

    d = Distinct(reqs)
    solver.add(d)

res = solver.check()
print(res)

Answer 1

每个基准测试都是独一无二的，不可能想出一个在所有情况下都同样适用的好策略。但是您描述的场景很简单，可以处理。性能问题来自以下事实：Distinct 为求解器创建了太多不等式（数量为二次方），并且随着变量数量的增加，优化器很难处理它们。

根据经验，您应该尽可能避免使用Distinct。对于这种特殊情况，对变量施加严格的排序就足够了。 （当然，根据您的其他限制，这可能并不总是可行，但您所描述的似乎可以从这个技巧中受益。）所以，我会这样编码：

from z3 import *

reqs = [Int('i_%d' % i) for i in range(50)]

solver = Optimize()

for i in reqs:
  solver.add(i >= 1, i <= len(reqs))

for i, j in zip(reqs, reqs[1:]):
  solver.add(i < j)

res = solver.check()
print(res)
print(solver.model())

当我运行它时，我得到：

$ time python a.py
sat
[i_39 = 40,
 i_3 = 4,
 ...
 i_0 = 1,
 i_2 = 3]
python a.py  0.27s user 0.09s system 98% cpu 0.365 total

这很简短。希望您可以将其推广到您的原始问题。