据我所知，整数乘法与理论是一般判定的。 然而，在某些情况下，Z3并返回一个模型。 我很好奇地想知道如何做到这一点。 它有事情做与非线性算法在实数的新的决策程序？ 有什么具体的实例（例如：在有限的模数整数等）已认识到这Z3返回乘法查询模式？ 任何帮助深表感谢。
Answer 1:
是的，非线性整数运算的决策问题是不可判定。 我们可以编码停机问题，在非线性整数运算图灵机。 我强烈建议本美丽的书希尔伯特第十问题对任何人有兴趣在这个问题上。
需要注意的是，如果一个公式有一个解决方案，我们可以随时通过蛮力找到它。 也就是说，我们不断列举所有可能的任务，并测试它们是否满足公式与否。 这是不是来自试图通过只是运行该程序，并检查是否步指定次数后，终止于解决停机问题不同。
Z3不执行天真枚举。 给定一个号码k ，它使用编码的每一个整数变量k比特和降低到一切命题逻辑。 然后，SAT解算器来寻找解决方案。 如果找到一个解决方案，它将其转换回原始式整数解。 如果没有为命题形式无解，那么它试图增加k ，或者切换到不同的策略。 这种减少在命题逻辑本质上是一个模型/溶液的发现过程。 它不能显示的问题没有解决。 实际上，对于问题，每一个整数变量有一个上限和下限，它可以做到这一点。 所以，Z3具有使用其他策略显示无解的存在。
此外，还原成命题逻辑，如果有一个非常小的溶液（即需要较少的比特数中的溶液，以进行编码）才有效。 我讨论的是，在下面的帖子：
- 需要帮助了解公式
Z3不具有非线性整数运算很好的支持。 上面描述的方法是非常简单的。 在我看来，数学似乎有技术最全面的产品组合：
http://reference.wolfram.com/legacy/v5_2/functions/AdvancedDocumentationDiophantinePolynomialSystems
最后，非线性实际运算（NLSat）求解器不使用默认的非线性整数问题。 它通常是在整数的问题非常无效。 然而，我们可以强制Z3使用NLSat甚至整的问题。 我们只需要更换：
(check-sat)
同
(check-sat-using qfnra-nlsat)
当使用此命令，Z3将解决这个问题作为一个真正的问题。 如果没有找到真正的解决办法，我们知道有没有整数解。 如果找到一个解决方案，Z3将检查的解决方案是真正将整数值指派到整数变量。 如果不是的话，它将返回unknown ，以表明它没能解决问题。
文章来源: How does Z3 handle non-linear integer arithmetic?
