Z3 Prover возвращает неверное решение

Question

Я пытаюсь решить уравнение с Z3 Thoerem Prover в Python. Но решение, которое я получаю, неверно.

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. Но это также вряд ли сработает, поскольку у вас будет нелинейное диофантово уравнение, а у 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 решатель в этом отношении) просто не является правильным инструментом для решения / решения таких проблем.

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