The problem of solving quantified constraints over real numbers is, in general, undecidable when allowing function symbols such as sin or cosine. However, Ratschan presents an algorithm that nevertheless almost always terminates, except in some pathological (unstable) inputs. It is stable in the sense that the truth value of the input does not change under small perturbations of the occurring constants. For example, the constraint “for every x, x.x +1 ≥ 0” is stable, whereas “for every x, x.x ≥ 0” is not. This is because a small perturbation on the constant 1 would basically render a polynomial with the same number of powers of x, including the zeroth, whereas adding a free constant to x square, however small, adds a further term to the polynomial.

The algorithm Ratschan proposes replaces exhaustive search as much as possible with methods for pruning elements from the search space. This idea is extended to quantified inequality constraints for which all (free and bound) variables are bounded to a closed interval. When no more elements can be pruned, a branching is done by splitting a bound into pieces (for quantified variables, this means replacing subconstraints of the form “for every x that belongs to I” with “for every x that belongs to I1 and for every x that belongs to I2,” where “I = I1 Union I2,” or the corresponding existential case). This provides new possibilities for pruning. The aforementioned two steps are repeated until all elements have been pruned (or the constraint has been disproved). For computing elements of the bounds that contain solutions, the negation of the input constraint is taken and again is applied to the above branch-and-prune approach. Ratschan claims that as a side effect, this approach improves the current methods for numerical constraint satisfaction problems in the case where the solution set does not consist of finitely many isolated solutions.

Ratschan’s exposition is very clear and convincing. He admits one case (“robust-6”) in which the algorithm took longer. Ratschan also observes that although one can get even better runtimes by symbolically eliminating linearly quantified variables before applying his algorithm, in some cases the result can be very large, destroying the positive effects of the eliminated variable. Admittedly, more work is needed to investigate this behavior in detail. I strongly recommend this paper to any developer of computer algebra systems.