Z3 如何处理非线性整数算法? [英] How does Z3 handle non-linear integer arithmetic?
问题描述
我知道乘法整数的理论通常是不可判定的.尽管如此，在某些情况下，Z3 确实会返回一个模型.我很想知道这是如何完成的.它与实数非线性算术的新决策程序有关吗?哪些特定实例(例如:有限模数下的整数等)已被识别为 Z3 返回乘法查询的模型?非常感谢任何帮助.
I am aware that the theory of integers with multiplication is generically undecidable. Nevertheless, in certain instances, Z3 does return a model. I am curious to know how this is done. Does it have something to do with the new decision procedure for non-linear arithmetic over reals? What specific instances (eg: Integers under finite modulus etc) have been recognized for which Z3 returns a model for a multiplication query? Any help is much appreciated.
推荐答案
是的，非线性整数算法的决策问题是不可判定的.我们可以用非线性整数算法对图灵机的停机问题进行编码.我强烈推荐这本漂亮的书希尔伯特的第十个问题给任何人对这个问题感兴趣.
Yes, the decision problem for nonlinear integer arithmetic is undecidable. We can encode the Halting problem for Turing machines in nonlinear integer arithmetic. I strongly recommend the beautiful book Hilbert's tenth problem for anybody interested in this problem.
请注意，如果公式有解，我们总是可以通过蛮力找到它.也就是说，我们不断枚举所有可能的赋值，并测试它们是否满足公式.这与尝试通过运行程序并检查程序是否在给定的步骤数后终止来解决停机问题没有什么不同.
Note that, if a formula has a solution, we can always find it by brute force. That is, we keep enumerating all possible assignments, and testing whether they satisfy the formula or not. This is not that different from trying to solve the Halting problem by just running the program and checking whether it terminates after a given number of steps.
Z3 不执行简单的枚举.给定一个数字 k，它使用 k 位对每个整数变量进行编码，并将所有内容简化为命题逻辑.然后，使用 SAT 求解器来寻找解决方案.如果找到解，它会将其转换回原始公式的整数解.如果命题形式没有解决方案，那么它会尝试增加k，或者切换到不同的策略.这种对命题逻辑的简化本质上是一个模型/解决方案寻找过程.它不能表明问题没有解决方案.实际上，对于每个整数变量都有下限和上限的问题，它可以做到.因此，Z3 必须使用其他策略来表明不存在解决方案.
Z3 does not perform a naive enumeration. Given a number k, it encodes every integer variable using k bits and reduces everything into Propositional logic. Then, a SAT solver is used to find a solution. If a solution is found, it converts it back into an integer solution for the original formula. If there is no solution for the Propositional formal, then it tries to increase k, or switches to a different strategy. This reduction to Propositional logic is essentially a model/solution finding procedure. It can't show that a problem does not have a solution. Actually, for problems where every integer variable has a lower and upper bound, it can do it. So, Z3 has to use other strategies for showing no solution exists.
此外，只有在有一个非常小的解决方案(需要少量编码的解决方案)时，才可以简化为命题逻辑.我在以下帖子中讨论了这一点:
Moreover, the reduction into Propositional logic only works if there is a very small solution (a solution that needs a small number of bits to be encoded). I discuss that in the following post:
Z3 对非线性整数算法没有很好的支持.上面描述的方法非常简单.在我看来，Mathematica 似乎拥有最全面的技术组合:
Z3 does not have good support for nonlinear integer arithmetic. The approach described above is very simplistic. In my opinion, Mathematica seems to have the most comprehensive portfolio of techniques:
http://reference.wolfram.com/legacy/v5_2/functions/AdvancedDocumentationDiophantinePolynomialSystems
最后，对于非线性整数问题，默认情况下不使用非线性实数算术 (NLSat) 求解器.它通常对整数问题非常无效.尽管如此，即使对于整数问题，我们也可以强制 Z3 使用 NLSat.我们只需要替换:
Finally, the nonlinear real arithmetic (NLSat) solver is not used by default for nonlinear integer problems. It is usually very ineffective on integer problems. Nonetheless, we can force Z3 to use NLSat even for integer problems. We just have to replace:
(check-sat)
与
(check-sat-using qfnra-nlsat)
使用此命令时，Z3 会将问题作为真正的问题来解决.如果没有找到实解，我们就知道没有整数解.如果找到解决方案，Z3 将检查该解决方案是否真的将整数值分配给整数变量.如果不是这种情况，它将返回 unknown 表示它未能解决问题.
When this command is used, Z3 will solve the problem as a real problem. If no real solution is found, we know there is no integer solution. If a solution is found, Z3 will check if the solution is really assigning integer values to integer variables. If that is not the case, it will return unknown to indicate it failed to solve the problem.
这篇关于Z3 如何处理非线性整数算法?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
