Chapter 7
Program Termination

Consider the constraint x [-2,2]x2 - 1 0. This constraint certainly is true. Now replace the zero on the right-hand side of the equality by a very small real number ε. Certainly this does not change the truth value. Hence we call such a constraint robust. On the other hand, consider the constraint x [-2,2]x2 0. It is also true, but changes its truth value to false if we replace the zero by a very small negative constant. Hence we call such a constraint fragile.

The algorithm in RSolver uses approximation. So it will usually not use the exact value of constants, but can only enclose them into small intervals. Therefore, it will in general not be able to compute the truth value of fragile constraints. But it will always terminate for robust constraints. So in that case you will always get an answer, provided you are willing to wait long enough.

Note that in practice, especially for constraints that are almost fragile, it might also happen that floating point precision is not sufficient to compute an answer. In that case, the system will terminate with an according error message.

For more information on the property of being robust or fragile, you can read some articles for the case of quantified constraints [13] or general books on numerical analysis (under the terms “well-posed”, “ill-posed”, “well-conditioned”, “ill-conditioned”).