z3 实指数答案

【问题标题】：z3 Real Exponentiationz3 实指数
【发布时间】：2016-04-07 22:13:40
【问题描述】：

我遇到了一个奇怪的情况，z3py 为逻辑上相同的问题生成了两个不同的答案。

版本 1：

>>> import z3
>>> r, r2, q = z3.Reals('r r2 q')
>>> s = z3.Solver()
>>> s.add(r > 2, r2 == r, q == r2 ** z3.RealVal(0.5))
>>> s.check()
unknown

第 2 版

>>> import z3
>>> r, r2, q = z3.Reals('r r2 q')
>>> s = z3.Solver()
>>> s.add(r > 2, r2 == r, q * q == r2)
>>> s.check()
sat

如何更改我对版本 1 所做的操作，以便它产生准确的结果？这些约束是即时生成的，如果我试图即时重写它们，可能会显着增加应用程序的复杂性。此外，如果根是真正的符号，Python 本身根本不可能解决这个问题。

编辑：我发现如果我为我的求解器使用以下设置，它将成功求解（虽然有点慢）：

z3.Then("simplify","solve-eqs","smt").solver()

然而，我并不完全清楚指定它而不仅仅是默认求解器的含义。

【问题讨论】：

标签： python python-3.x z3 z3py

【解决方案1】：

Z3 在非线性实际问题上的开箱即用性能不是很好，它肯定需要一些摆弄才能找到你需要的所有解决方案。我的第一次尝试总是切换到 NLSAT 求解器（应用qfnra-nlsat 策略，或从中制作求解器）。该求解器通常在 QF_NRA 问题上要好得多，但它不支持任何理论组合，即，如果您有其他类型的变量，它会退出。

此外，在 stackoverflow 中搜索“Z3”和“非线性”，其中的各个方面都有大量的问题和答案。

【讨论】：