Z3 Prover returns wrong decision

Question

I am trying to solve an equation with Z3 Thoerem Prover in Python. But the solution I get is wrong.

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())

I get this solution:

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

But when you fill in these values ​​for this equation, the result will be as follows: 10.09735182849937. But what I want to find is the exact solution. What am I doing wrong?

Thank you for your help:)

Answer 1

The short answer is that the division is rounded, and therefore the answer is correct, but not what you expected. Please note that with the appointment of Z3 you will find:

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 !

gory: 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, ) - / .

Answer 2

, (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())

Z3 4.4.1 Windows.

"unknown", Z3 . , , MiniZinc Excel.

[x=1, y=1, z=20], , :

x/(y+z) = 1/(1+20) is 0 for integer division
y/(x+z) = 1/(1+20) is 0 for integer division
z/(x+y) = 20/(1+1) is 10