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は、あなたが持っていことに注意してください：最初の2つの項が0に切り捨て

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

ので、あなたは、方程式を平らにするために、共通の分母を掛け、およびZ3にすることを提起することができます。しかし、あなたは非線形のディオファンタス方程式を持ち、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)で全体の方程式を掛け改訂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()) 

私はWindows下Z3 4.4.1を使用しています。

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