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發現您有：

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

因爲前兩項本輪下跌至0。您可以通過共同點乘扁平化方程，並提出，要Z3。但是這也不太可能發揮作用，因爲你將會有一個非線性Diophantine方程，並且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求解就此而言）根本就不是解決/解決這些問題的正確工具。

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.1Windows下。

修改後的代碼返回"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