Why is non-linear real arithmetic decidable while non-linear integer arithmetic is not?

Question

I understand that nonlinear integer arithmetic is basically Hilbert's tenth problem and is proven to be undecidable. However the Z3 solver is able to provide a complete solution for nonlinear real arithmetic. I was just curious what is the fundamental difference between the two problems so that there is a definitive algorithm for nonlinear real arithmetic?

Seems like there is a paper on Z3's implementation of nonlinear polynomial real arithmetic. I do not have a strong formal methods/math background. Any intuition behind this issue is appreciated!

Answer 1

Considering that you know that nonlinear real arithmetic is decidable while nonlinear integer arithmetic is not, the best you can hope for is better intuition and some examples to help you understand how different QF_NRA is from QF_NIA.

I give a few example in this answer. I'll give one more: consider the equation y = x². If x and y are real numbers, then y is plus or minus the square-root of x (assuming x is non-negative). If however you say x and y have to be integers, then y = x² may or may not have a solution, depending on the value of x.

The fundamental fact is that there are a lot of math problems that are very easy to solve if your variables are real numbers, but much more difficult if your variables have to be integers, and in may cases they may not even have a solution.