The Algorithm

A detailed description of the algorithm employed by this software can be found in other papers [15]. Some preprints are available from the author’s webpage.

For using the software it is not necessary to grasp all its internal details. However—for using it efficiently—it can be useful to understand roughly, how the algorithm works:

The basic idea is, to compute some information for the atomic sub-constraints (e.g., the occurring inequalities), and using it to compute some information of the total constraint. If this procedure fails, we decompose the variable space into pieces, until some new information can be deduced.

In the simplest case, we use the following test on atomic constraints:

- Given:
- An atomic constraint ϕ,
- a box B

- Find: An element of the set {T,F,U} such that
- T implies that ϕ is true for all elements of B, and
- F implies that ϕ is false for all elements of B.

Such a test is provided by techniques of interval analysis [11, 8]. Of course, the test should return T or F as often as possible. Except for degenerate cases, such tests succeed to do this for sufficiently small boxes.

Consider the example ∃y ∈ [-2,2]x^{2} + y^{2} ≤ 1, where the variable
x ranges over the interval [-2,2]. Here we just have one atomic
sub-constraint—x^{2} + y^{2} ≤ 1—on which to do the test. Of course, for the box
[-2,2] × [-2,2] it can only fail. Therefore the algorithm will do branching: it will
either split the interval corresponding to a free variable into two parts,
or it will rewrite ∃y ∈ [-2,2]x^{2} + y^{2} ≤ 1 to the equivalent constraint
∃y ∈ [-2,0]x^{2} + y^{2} ≤ 1 ∨∃y ∈ [0,2]x^{2} + y^{2} ≤ 1. In a similar way it can split
universal quantifiers into a conjunction of several universally quantified
constraints.

This splitting can be prohibited by using starred versions of the quantifiers, that is, by using FORALL*, and EXISTS*.