python – Z3 Prover返回错误的解决方案

我正试图用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.但我想要找到的是一个确切的解决方案.
我究竟做错了什么？

谢谢你的帮助 ：)

解决方法:

简短的回答是该部门正在逐渐缩小,因此答案是正确的,但不是你所期望的.请注意,通过分配Z3,您发现：

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

因为前两个项向下舍入到0.您可以乘以公分母来平坦化方程式,然后将其置于z3.但这也极不可能,因为你将有一个非线性Diophantine方程,而Z3没有该片段的决策程序.事实上,众所周知,非线性整数运算是不可判定的.有关详细信息,请参阅希尔伯特的第10个问题：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

还有一个quora讨论肯定更容易遵循：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求解器)根本不是解决/处理此类问题的正确工具.

标签：python,z3,z3py
来源： https://codeday.me/bug/20190527/1163182.html