我知道乘法的整数理论通常是不可判定的.然而,在某些情况下,Z3确实返回了一个模型.我很想知道这是怎么做到的.它是否与用于实数的非线性算术的新决策程序有关？已经识别出哪些特定实例(例如:有限模数下的整数等),Z3为其返回乘法查询的模型？任何帮助深表感谢.
Leo*_*ura 30
是的,非线性整数算术的决策问题是不可判定的.我们可以用非线性整数算法对图灵机的Halting问题进行编码.对于任何对这个问题感兴趣的人,我强烈推荐美丽的书希尔伯特的第十个问题.
请注意,如果公式有解决方案,我们总能通过蛮力找到它.也就是说,我们会一直列举所有可能的任务,并测试它们是否满足公式.这与尝试通过仅运行程序并检查它是否在给定步数之后终止来解决停止问题没有什么不同.
Z3不执行天真的枚举.给定一个数字k,它使用k位对每个整数变量进行编码,并将所有内容简化为命题逻辑.然后,使用SAT求解器来找到解.如果找到解决方案,它会将其转换回原始公式的整数解.如果没有针对Propositional formal的解决方案,那么它会尝试增加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以表明它未能解决问题.