我了解到非线性整数算术基本上是希尔伯特的第十个问题，并且被证明是不确定的。但是Z3求解器能够为非线性实数运算提供完整的解决方案。我只是好奇两个问题之间的根本区别是什么，所以对于非线性实数运算有一个确定的算法？
似乎在Z3的非线性多项式实数运算的实现上有一个paper。我没有很强的正式方法/数学背景。对此问题的任何直觉表示赞赏!
最佳答案
考虑到您知道非线性实数运算是可判定的，而非线性整数算术则不可判定，因此您所希望的最好是更好的直觉，并提供一些示例来帮助您了解QF_NRA与QF_NIA有何不同。
我在this answer中举几个例子。我再给出一个:考虑方程y = x2。如果x和y为实数，则y为正负x的平方根(假设x为非负数)。但是，如果您说x和y必须是整数，则y = x2可能有也可能没有解决方案，具体取决于x的值。
基本事实是，如果您的变量是实数，有很多数学问题很容易解决，但是如果您的变量必须是整数，则困难得多，在某些情况下甚至可能没有解决方案。