Z3 Prover返回错误的解决方案

Question

我正在尝试使用Python中的Z3 Thoerem Prover解决一个方程式。但是我得到的解决方案是错误的。

from z3 import *    
solv = Solver()
x = Int("x")
y = Int("y")
z = Int("z")
s = Solver()
s.add(x/(y+z)+y/(x+z)+z/(x+y)==10, x>0, y>0, z>0)
s.add()
print(s.check())
print(s.model())

我得到这个解决方案：

[z = 60, y = 5, x = 1]

但是，当您将这些值填写到给定的方程式中时，结果为：10.09735182849937。但是我想找到的是一个精确的解决方案。我究竟做错了什么？

谢谢你的帮助 ：）

Answer 1

简短的答案是该部门正在四舍五入，因此答案是正确的，但并非您所期望的。请注意，找到作业Z3后，您将拥有：

1/65 + 5/61 + 60/6 = 10

因为前两项向下舍入为0。您可以乘以公分母来展平方程式，并将其置于z3处。但这也不可能实现，因为您将拥有一个非线性Diophantine方程，并且Z3没有针对该片段的决策程序。实际上，众所周知，非线性整数算法是不确定的。有关详细信息，请参阅希尔伯特的第十个问题：https : //en.wikipedia.org/wiki/Hilbert%27s_tenth_problem

实际上，关于这种方程式我们已经知道很多：它定义了一条椭圆曲线。奇怪的N是，没有解决方案。对于甚至N（即您的案例N=10）解决方案可能存在也可能不存在，如果存在，它们可能会很大。当我说大时，我的意思是真的：因为N=10众所周知，有一个解决方案，其中令人满意的值具有190位数字！

这是一篇很好的文章，包含了所有细节：http : //ami.ektf.hu/uploads/papers/finalpdf/AMI_43_from29to41.pdf

还有一个法定人数讨论绝对更容易遵循：https : //www.quora.com/How-do-you-find-the-positive-integer-solutions-to-frac-x-y+z-+- frac-y-z + x-+-frac-z-x + y-4

长话短说，z3（或与此相关的任何SMT求解器）根本不是解决/解决此类问题的正确工具。