33

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

4

1 回答 1

36

是的，非线性整数算术的决策问题是不可判定的。我们可以用非线性整数算法对图灵机的停机问题进行编码。我强烈向任何对此问题感兴趣的人推荐这本美丽的希尔伯特第十题。

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

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

此外，只有在存在非常小的解决方案（需要对少量比特进行编码的解决方案）时，减少到命题逻辑才有效。我在下面的帖子中讨论了这一点：

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

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

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

(check-sat)

和

(check-sat-using qfnra-nlsat)

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

于 2012-12-16T04:07:33.623 回答