Constraint Solving

Constraint Solving

We are developing software, theory, and algorithms that can solve mathematical constraints consisting of non-linear equalities and inequalities, conjunctions, disjunctions, and logical quantifiers (forall , exist ).

For example, we produce as the solution of the constraint x²+x²-1 <= 0 /\2y <= x²:

See also the demo at http://rsolver.sourceforge.net.

We apply the constraint solving technology in several areas (e.g., hybrid systems, computation of Lyapunov functions).

We offer a large range of thesis topic in the area for students with a background in computer science, control, or mathematics. According to the interest and background of the student, the thesis can be done in an application-oriented context, in a more theoretical/mathematical direction, or in the direction of software-development.

I will be happy to provide more information. Just contact me!

Examples for specific topic in the area include:

Applying the constraint solver to a special application area (e.g., parameter or state estimation, robust control, model predictive control) and optimizing it for the application.
We have a special algorithm for computing Lyapunov-like functions (in fact, one of world-wide only two completely automatic algorithms in the area). The topic of the thesis would be to apply this algorithm to new problem classes with a similar structure (e.g., termination of term-rewrite systems, Lyapunov functions of hybrid systems, functions that prove that certain states in dynamical systems are not reachable, program verification), and to adapt the algorithm to these areas.

Constraint Solving