Chapter 1
Introduction

Take the expression x2 + y2 + z2 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]x2 + y2 + z2 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 x2 + y2 + z2 1 holds. Clearly this is a disc, that is, the projection of the solution set of x2 + y2 + z2 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 [1723]. 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]x2 + y2 + z2 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.


PIC


Figure 1.1: Solution for z [-2,2]x2 + y2 + z2 1


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 [1723]. 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 [10119] and constraint programming [18].