Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Z3 Prover returns wrong solution

Tags:

python

z3

z3py

I'm 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 those values to the given equation the result is: 10.09735182849937. But what I want to find is an exact solution. What am I doing wrong?

Thanks for your help :)

like image 969
Peter234 Avatar asked Jan 29 '23 10:01

Peter234


1 Answers

The short answer is that the division is being rounded down, and thus the answer is correct but not what you expected. Note that with the assignment Z3 found you have:

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

since the first two terms round down to 0. You can multiply by the common denominator to flatten the equation, and pose that to z3. But that is extremely unlikely to work either, since you will have a nonlinear Diophantine equation, and Z3 doesn't have a decision procedure for that fragment. In fact, it is well-known that non-linear integer arithmetic is undecidable. For details, see Hilbert's 10th problem: https://en.wikipedia.org/wiki/Hilbert%27s_tenth_problem

In fact, quite a bit is known about this sort of an equation: It defines an elliptic curve. For odd N, it is known that there are no solutions. For even N (i.e., your case with N=10) solutions may or may not exist, and when they do, they can be really large. And when I say large, I really mean it: For N=10 it is known that there is a solution where the satisfying values have 190 digits!

Here's a good article on this very equation with all the gory details: http://ami.ektf.hu/uploads/papers/finalpdf/AMI_43_from29to41.pdf

There's also a quora discussion that is definitely easier to follow: 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

Long story short, z3 (or any SMT solver for that matter) is simply not the right tool to solve/approach such problems.

like image 111
alias Avatar answered Feb 14 '23 08:02

alias