非線形整数演算が非線形整数演算ではないのに、非線形実演算可能と判定されるのはなぜですか？

Question

私は非線形整数算術は基本的にヒルベルトの10番目の問題であり、決めることができないことが分かっています。しかし、Z3ソルバーは、非線形実数演算のための完全なソリューションを提供することができます。私は、2つの問題の根本的な違いは何かが不思議に思っていたので、非線形実数演算のための決定的なアルゴリズムがありますか？

Z3の非線形多項式実数演算の実装にはpaperがあるようです。私は強力な正式な方法/数学の背景がありません。この問題の背後にある直観は感謝しています！

Answer 1

非線形整数演算が非線形演算ではなく非線形実数演算が決定可能であることを知っていることを考慮すると、QF_NIAとはどのように違うのかを理解するのに役立ちます。

this answerにいくつかの例を示します。私はもう一つ与えます：方程式を考えてくださいy = x。 XとYは実数である場合、Yは（Xが非負であると仮定して）プラスまたはマイナスXの平方根です。場合あなたがXとYは整数でなければならないと言うしかし、その後、Y = Xは、またはのxの値に応じて、解決策を持っていない可能性があります。

基本的な事実は、変数が実数であれば解決するのは非常に簡単ですが、変数が整数でなければならない場合は非常に困難であり、場合によっては解決策。