Z3 Prover가 잘못된 솔루션을 반환합니다.

Question

저는 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. 그러나 내가 찾고자하는 것은 정확한 해결책입니다. 내가 뭘 잘못하고 있니? 당신의 도움 :)

Answer 1

짧은 대답은 부문 내림되고 있음, 따라서 대답은 예상하지 무엇을 정확하지만. 할당과 Z3는 당신이 발견 주 : 처음 두 용어가 0으로 내림

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

때문에 당신은 식을 평평하게하는 공통 분모를 곱 및 Z3에 있음을 제기 할 수 있습니다. 그러나 이것은 비선형 Diophantine 방정식을 가지며 Z3에는 해당 단편에 대한 결정 절차가 없으므로 작업 할 가능성이 극히 낮습니다. 실제로, 비선형 정수 연산은 결정 불가능하다는 것이 잘 알려져 있습니다. 자세한 내용은 Hilbert의 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 해결사

여기에 모든 피투성이의 세부 사항이 매우 방정식에 좋은 기사입니다 그러한 문제를 해결하는 데는 적절한 도구가 아닙니다.

Answer 2

에 대한

덕분에 나는 코드를 시도하고 내가 분할을 제거하기 위해 (x+y)*(x+z)*(y+z)으로 전체 방정식을 곱 어디 하나를 수정 : 나는 Windows에서 Z3 4.4.1을 사용하고

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으로 해결할 수 없기 때문에 수정 된 코드는 "unknown"을 반환합니다. 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