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!

Rieth

Late to the party, but it may be interest to note that Linear Programming is an $O(n^4)$ problem, while Integer Linear Programming is NP-complete. – Orientation

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.

Tort

What's the intuition behind solving things like y = x**2 in Real? – Rieth

You can solve all problems of the form y=ax^2 + bx + c for real x using the quadratic equation. There is no equivalent for the integers. Basically integer problems are often harder because you're asking to solve the same equations, but adding the restriction that the result has to be an integer. Typically the same techniques do not work as for the reals. – Tort