Z3PY 非常慢，有很多变量？

问题描述

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

我创建了 26 个 Z3-int。然后我添加了硬约束，它不应小于 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)

解决方法

每个基准都是独一无二的，不可能想出一个在所有情况下都同样适用的好策略。但是你描述的场景很简单，可以处理。性能问题来自这样一个事实：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

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

smt solver z3 z3py