加快 Z3Py 中的公式构建

Posted 2023-03-06

【中文标题】加快 Z3Py 中的公式构建

【英文标题】：Speed up formula building in Z3Py

【发布时间】：2019-04-27 21:31:52

【问题描述】：

我使用 Z3Py 构建大型公式（~1500 Bool 变量，~90k 断言），我目前正在使用 Solver.add 添加断言，这些断言大多很小（例如，对 2 个变量的影响）。

我的代码看起来像这样，大约有 10 个外部 for 循环依次排列。循环嵌套深度从 2 到 6 不等。

s = Solver()

for i in range(A):
  for j in range(B):
    ...
      s.add(Implies(vars[i,j,...], vars[k,l,...]))

问题是构建求解器需要大约 11 秒（使用 __debug__ == False），而找到解决方案只需要大约 8 秒。

分析表明，很多时间都花在了Z3_sort_to_ast、z3code.Elementaries.Check（由前者调用）和其他似乎可以内联的方法上，如果不能以某种方式消除的话。

如何优化 Z3 Solver 的创建？也许有一个更底层的内部接口可以加快速度？

【问题讨论】：

Python API 没有针对速度进行优化，很有可能它在不必要的深度嵌套函数和断言/异常/类型检查中浪费了大量时间。为了在构建过程中获得最佳性能，最好直接使用 C API。

【参考方案1】：

我看到了 3 个选项：

使用 SMT-LIB 接口 跳过 Z3 的高级 API 直接使用 C API 重写代码

如果与 Z3 的交互很少（求解并获得模型），SMT-LIB 可能是最佳选择。

如果用 C 重写 python 代码相当复杂，请尝试 pySMT。我们与 Z3 集成的方式跳过了高级 API，直接调用了在 python 级别公开的底层 C 函数。 pySMT 本身会产生开销，但通常它会付出代价。您可以查看 [1] 以了解有关我们如何做到这一点的一些想法。

[1]https://github.com/pysmt/pysmt/blob/master/pysmt/solvers/z3.py#L853