Z3 Prover返回错误的解决方案

Question

我试图用Python中的z3thoerem 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())

我得到这样的解决方案：

^{pr2}$

但是当你把这些值填到给定的方程中，结果是：10.09735182849937。但我想找到一个精确的解。 我做错什么了？在

感谢您的帮助：）

Answer 1

我尝试了你的代码和一个修改后的代码，我用(x+y)*(x+z)*(y+z)乘以整个方程来消除除法：

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(x*(x+z)*(x+y) + y*(y+z)*(x+y) + z*(y+z)*(x+z) == 10*(x+y)*(x+z)*(y+z), x > 0, y > 0, z > 0)
s.add()
print(s.check())
print(s.model())

我在Windows下使用Z3 4.4.1。在

修改后的代码返回"unknown"，因为Z3无法解决它。 可能没有解决方案，正如其他解算器如MiniZinc和{}所证实的那样。在

如果假定使用整数除法，则原始代码返回[x=1, y=1, z=20]，这是正确的：

^{pr2}$

Answer 2

简单的回答是除法被舍入，因此答案是正确的，但不是您期望的那样。请注意，在作业Z3中，您有：

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

因为前两项四舍五入到0。你可以乘以公分母来展平方程，然后把它放在z3。但这也不太可能奏效，因为你将有一个非线性的丢番图方程，而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解决方案）根本不是解决/解决此类问题的正确工具。在