3

将 z3 用于非线性实数算术时，我遇到了超时问题。下面的代码是检查 4 维超矩形的体积是否大于 50000 并且还满足一些约束。但是z3不能在1分钟内给出答案。如何让它更快？

a0min = Real('a0min')
a0max = Real('a0max')
a1min = Real('a1min')
a1max = Real('a1max')
a2min = Real('a2min')
a2max = Real('a2max')
a3min = Real('a3min')
a3max = Real('a3max')
volume = Real('volume')

s = Tactic('qfnra-nlsat').solver()

s.add(-a0min * (1.0 - a1max) + a2max * a3max <= -95000.0,
a0min >  0.0,
a0min < a0max,
a0max < 1000000.0,
a1min > 0.0,
a1min < a1max,
a1max < 1.0,
a2min > 1.0,
a2min < a2max,
a2max < 1000.0,
a3min > 1.0,
a3min < a3max,
a3max < 50.0,
(a0max - a0min) * (a1max -  a1min) * (a2max -  a2min) * (a3max - a3min) > 50000.0,
volume == (a0max - a0min) * (a1max -  a1min) * (a2max -  a2min) * (a3max - a3min))
print s.check()

还有一个有趣的事情：如果用“<=”和“>=”替换一些“>”和“<”，z3求解器可以在两秒钟内返回答案。对应的代码如下。有谁知道为什么会这样？

a0min = Real('a0min')
a0max = Real('a0max')
a1min = Real('a1min')
a1max = Real('a1max')
a2min = Real('a2min')
a2max = Real('a2max')
a3min = Real('a3min')
a3max = Real('a3max')
volume = Real('volume')

s = Tactic('qfnra-nlsat').solver()

s.add(-a0min * (1.0 - a1max) + a2max * a3max <= -95000.0,
a0min >=  0.0,
a0min <= a0max,
a0max <= 1000000.0,
a1min >= 0.0,
a1min <= a1max,
a1max <= 1.0,
a2min >= 1.0,
a2min <= a2max,
a2max <= 1000.0,
a3min >= 1.0,
a3min <= a3max,
a3max <= 50.0,

(a0max - a0min) * (a1max -  a1min) * (a2max -  a2min) * (a3max - a3min) > 50000.0,
volume == (a0max - a0min) * (a1max -  a1min) * (a2max -  a2min) * (a3max - a3min))
print s.check()
4

1 回答 1

2

在第一种情况下，Z3 用实代数数“卡住”了计算。如果我们执行您的脚本

 valgrind --tool=callgrind python nl.py

几分钟后中断，然后运行

 kcachegrind

我们会看到 Z3 卡在里面了algebraic_numbers::isolate_roots。目前求解器使用的实数代数包nlsat效率很低。我们有一个新的代数计算包，但它还没有集成nlsat。

避免代数数计算的一个技巧是只使用严格的不等式。等式volume == ...是无害的，因为它在预处理期间被消除。如果我们用 替换第一个约束-a0min * (1.0 - a1max) + a2max * a3max < -95000.0，那么 Z3 也会快速终止（也可以在此处在线获得）。

a0min = Real('a0min')
a0max = Real('a0max')
a1min = Real('a1min')
a1max = Real('a1max')
a2min = Real('a2min')
a2max = Real('a2max')
a3min = Real('a3min')
a3max = Real('a3max')
volume = Real('volume')

s = Tactic('qfnra-nlsat').solver()

s.add(-a0min * (1.0 - a1max) + a2max * a3max < -95000.0,
a0min >  0.0,
a0min < a0max,
a0max < 1000000.0,
a1min > 0.0,
a1min < a1max,
a1max < 1.0,
a2min > 1.0,
a2min < a2max,
a2max < 1000.0,
a3min > 1.0,
a3min < a3max,
a3max < 50.0,
(a0max - a0min) * (a1max -  a1min) * (a2max -  a2min) * (a3max - a3min) > 50000.0,
volume == (a0max - a0min) * (a1max -  a1min) * (a2max -  a2min) * (a3max - a3min))
print s.check()
print s.model()

顺便说一句，当您将所有内容替换为 时<=，nlsat仍然必须使用实数代数计算，但是更改会影响nlsat搜索树，并且它设法在陷入实数代数数计算之前找到解决方案。

以下是我们尝试/检查的示例中 nlsat 被“卡住”的三个地方

  • 实数代数计算（如您的示例）。当我们用新的包替换当前包时，这将得到解决。

  • 多项式分解。目前在 Z3 中实现的算法效率非常低。这也可以修复。

  • 子结果计算。这很棘手，因为据我所知 Z3 使用了一种非常有效的实现。性能类似于 Mathematica 等最先进系统中的实现。该操作在 Z3 回溯搜索时使用。好的特性是我们可以证明 Z3 将始终使用这种方法终止。一种替代方法是考虑不保证终止但更便宜的近似方法。不幸的是，这不是像前两个那样的微小变化。

于 2013-05-10T18:22:56.150 回答