## Chapter 7

Program Termination

Consider the constraint ∃x ∈ [-2,2]x^{2} - 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]x^{2} ≤ 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”).