z3在非线性约束下超时

Question

当使用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() 

Answer 1

在第一种情况下，Z3用真代数数字“卡住”计算。如果我们几分钟后

valgrind --tool=callgrind python nl.py 

中断执行脚本，并运行

kcachegrind 

我们将看到，Z3被卡内algebraic_numbers::isolate_roots。 nlsat求解器使用的当前实数代数包非常低效。 我们有一个用代数数字计算的new package，但它还没有与nlsat集成。

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

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中实现的当前算法效率非常低。这也可以修复。

• Subresultant computations。这一点很棘手，因为据我所知Z3使用了非常有效的实现。性能与Mathematica等先进系统的实现类似。当Z3回溯搜索时使用此操作。好的属性是我们可以证明Z3总是会使用这种方法终止。另一种选择是考虑不保证终止但更便宜的近似方法。不幸的是，这不是像前两个那样的小改变。