You have come to an old website. Our new URL is ths.rwth-aachen.de. Please update your bookmarks!




On Gröbner Bases in SMT-Compliant Decision Procedures

Bachelor (contact: Ulrich Loup)

Given a set of polynomials of arbitrary degree and in several variables, we are interested in its set of common zeros, i.e. the solutions to the corresponding system of polynomial equations, called variety. A Gröbner basis of a set of polynomials is another set of polynomials which have the same common zeros, but reduced with respect to division by each other. Well-established algorithms can compute a Gröbner basis which is also minimal in the sense that none of its elements is redundant, i.e., it can not be reduced to zero by means of the other basis elements.

Gröbner bases have many important applications, e.g., the ideal membership, equality or emptiness problems. Most importantly in our context is Hilbert's Nullstellensatz. This famous result from algebraic geometry entails that if a set of polynomials has an empty variety, its Gröbner basis contains exclusively a constant. Moreover, the converse is also true: If the respective Gröbner basis is nonempty, the corresponding variety is likewise. However, this result considers all possible zeros of polynomials, in particular, the complex ones.

Hilbert's Nullstellensatz, a famous result from algebraic geometry, entails that if a set of polynomials has an empty variety, its Gröbner basis contains exclusively a constant. Moreover, the converse is also true: If the respective Gröbner basis is nonempty, the corresponding variety is likewise. However, this result considers all possible zeros of polynomials, in particular, the complex ones.

Our special interest lies in real varieties. Hence, we need to make use of the Real Nullstellensatz, a variant of Hilbert's Nullstellensatz specialized to real solutions, in order to use the Gröbner-basis approach for solving a polynomial equation system.

This thesis topic comprises two major aspects: First, an application of the Real Nullstellensatz shall be implemented on the basis of existing methods for Gröbner basis computations. Second, our implementation of algorithms to compute Gröbner bases shall be enhanced to speed up the whole computation.