Introduction

Take the expression x^{2} + y^{2} + z^{2} ≤ 1, where the variables x, y and z range
over the real numbers. This expression represents a set of values—its
solution set, which is a ball. We call such an expression a constraint.
Solving a constraint means to find some interesting information about
its solution set, where the definition of “interesting” depends on the
application. For example, we might want to find a point in the solution
set, or we might want to find an approximation of the solution set by
hyper-rectangles.

This software package solves a special type of constraints, namely quantified
constraints. Take the following example: ∃z ∈ [-2,2]x^{2} + y^{2} + z^{2} ≤ 1. Here we
encounter the symbol ∃—an existential quantifier. The solution set of
this constraint is the set of all x and y such that there is a z such that
x^{2} + y^{2} + z^{2} ≤ 1 holds. Clearly this is a disc, that is, the projection of the
solution set of x^{2} + y^{2} + z^{2} ≤ 1 onto the two-dimensional real space. Such a
projection can be very convenient, because one can easily visualize sets in
two-dimensional real space.

A quantified constraint can also contain the symbol ∀, that is, universal quantifiers. This can be very useful for dealing with uncertain values. These occur, for example, in robust control [4], where one studies notions such as the stability of systems under uncertain values.

A quantified constraint can also contain the Boolean symbols for conjunction and disjunction. In general, it is a formula in the first-order predicate language [5] over the reals.

Traditionally, such constraints have been solved by symbolic methods [17, 2, 3]. However, these methods suffer from various drawbacks—especially for inputs that model real-world problems. Instead of symbolic solutions, the algorithm [12] employed in this software computes solutions that are approximate but correct.

For example, in Figure 1.1 you can see a visualization of the solution
computed for the constraint ∃z ∈ [-2,2]x^{2} + y^{2} + z^{2} ≤ 1. Here you can see a
green area—elements that are guaranteed to be within the solution set, a read
area—elements that are guaranteed to be out of the solution set, and a white
area—elements for which we do not have any information.

The user can specify an error bound—the maximum allowed fraction of the white area wrt. the total area. For example, the error bound used for Figure 1.1, was 0.05.

The software packages solves quantified constraints, that is, formulae in the first order predicate language over the reals. Classically such constraints have been solved by symbolic methods [17, 2, 3]. However, these methods suffer from various drawbacks—especially for inputs that model real-world problems. The algorithm [12] employed in this software computes solutions that are approximate up to a user-provided error bound. It uses various sub-algorithms from the area of interval computation [10, 11, 9] and constraint programming [18].