对于非线性整数问题，z3 处理幂不同于乘法

Question

我正在使用 z3 C++ API 并且在非线性整数运算方面有一些问题，其中 z3 似乎以不同的方式处理幂和乘法。

例如x*x*x > y*y 是 sat，但 x^3 > y^2 是 unknown:

#include <z3++.h>
#include <iostream>
using namespace std;

int main() {
    z3::context c;
    auto x = c.int_const("x");
    auto y = c.int_const("y");

    z3::solver sol(c);
    sol.add(x*x*x > y*y);
    cout << sol << " : " << sol.check() << endl;

    sol.reset();
    sol.add(z3::pw(x,3) > z3::pw(y,2));
    cout << sol << " : " << sol.check() << endl;
}

我已经阅读了一些 python 问题 (Z3 python treats x**2 different than x*x?)，但我使用的是 z3 的 4.4.0 版，应该修复这些问题。

我在尝试求解 x^51 > y^17 时遇到了这个问题。我知道非线性整数运算通常是不可判定的，但我有点惊讶 z3 找不到解决方案（即使重写为乘法）。所以我想知道以上是否是错误，或者对于这些示例，是否有任何方法可以从 C++ 中的 z3 获得更好的结果。

Answer 1

这不是错误，Z3 只是对非线性整数问题没有很好的支持；另见 How does Z3 handle non-linear integer arithmetic?

这个例子不是由任何实际的非线性算术求解器求解的，而是通过一个预处理步骤求解的，该步骤将所有内容转换为位向量，然后进行位爆炸，并运行一个纯 SAT 求解器；参见 nla2bv_tactic。这种策略不支持求幂，因此在第二次求解器调用中，它一直到（最通用的）SMT 求解器，后者立即放弃。

即使我们为 nla2bv 添加对求幂的支持，一般问题仍然存在，并且它还会为大指数生成非常大的 SAT 公式，因此我认为添加它的价值有限。

对于非线性整数问题，z3 处理幂不同于乘法

z3 treats power different than multiplication for nonlinear integer problems

smt

z3