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:
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]x2 + y2 ≤ 1, where the variable x ranges over the interval [-2,2]. Here we just have one atomic sub-constraint—x2 + y2 ≤ 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]x2 + y2 ≤ 1 to the equivalent constraint ∃y ∈ [-2,0]x2 + y2 ≤ 1 ∨∃y ∈ [0,2]x2 + y2 ≤ 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*.