Z3 如何处理非线性整数运算？

Posted 2023-02-25

【中文标题】Z3 如何处理非线性整数运算？

【英文标题】：How does Z3 handle non-linear integer arithmetic?

【发布时间】：2012-12-03 14:31:40

【问题描述】：

我知道整数乘法的理论通常是不可判定的。然而，在某些情况下，Z3 确实返回了一个模型。我很想知道这是怎么做到的。它与实数非线性算术的新决策程序有关吗？哪些特定实例（例如：有限模下的整数等）已被识别，Z3 会为其返回乘法查询的模型？非常感谢任何帮助。

【问题讨论】：

这是一个有效的问题。请不要投反对票，或投票关闭它。谢谢。

【参考方案1】：

是的，非线性整数算术的决策问题是不可判定的。 我们可以用非线性整数算法对图灵机的停机问题进行编码。 我强烈推荐这本漂亮的书Hilbert's tenth problem 给任何对此问题感兴趣的人。

请注意，如果公式有解，我们总是可以通过蛮力找到它。也就是说，我们不断枚举所有可能的赋值，并测试它们是否满足公式。这与通过运行程序并检查它是否在给定数量的步骤后终止来尝试解决停机问题并没有什么不同。

Z3 不执行简单的枚举。给定一个数字k，它使用k 位对每个整数变量进行编码，并将所有内容简化为命题逻辑。然后，使用 SAT 求解器来寻找解决方案。如果找到解决方案，它会将其转换回原始公式的整数解决方案。如果 Propositional 形式没有解决方案，那么它会尝试增加 k，或者切换到不同的策略。这种对命题逻辑的简化本质上是一个模型/解决方案查找过程。它不能表明一个问题没有解决方案。实际上，对于每个整数变量都有下限和上限的问题，它可以做到。因此，Z3 必须使用其他策略来表明不存在解决方案。

此外，仅当存在非常小的解决方案（需要对少量比特进行编码的解决方案）时，才能简化为命题逻辑。我将在以下帖子中讨论：

Need help understanding the equation

Z3 对非线性整数运算没有很好的支持。上述方法非常简单。在我看来，Mathematica 似乎拥有最全面的技术组合：

http://reference.wolfram.com/legacy/v5_2/functions/AdvancedDocumentationDiophantinePolynomialSystems

最后，非线性实数算术 (NLSat) 求解器默认情况下不用于非线性整数问题。它通常在整数问题上非常无效。 尽管如此，即使是整数问题，我们也可以强制 Z3 使用 NLSat。我们只需要替换：

(check-sat)

有

(check-sat-using qfnra-nlsat)

当使用该命令时，Z3 会将问题作为一个真正的问题来解决。如果没有找到真正的解决方案，我们就知道没有整数解决方案。如果找到解决方案，Z3 将检查解决方案是否真的将整数值分配给整数变量。如果不是这样，它会返回unknown 表示它未能解决问题。