On Gröbner Bases in SMT-Compliant Decision Procedures


Modern satisfiability solvers are able to determine satisfiability of a
given propositional logic formula very efficiently. Satisfiability Modulo
Theories (SMT) is an approach to use solvers to determine the satisfiability
of formulae from the first order logic over some theories.
This thesis aims at the development of methods for deciding consistency of
sets of polynomial constraints over the real numbers, which have a decent
performance when embedded into an SMT solver.
Gröbner bases and the Weak Nullstellensatz allow deciding consistency over the
complex numbers. Since Gröbner basis are frequently used and are subject to a
lot of active research, the existing algorithms are highly optimised. In this
thesis a well-known algorithm is implemented and extended to make the
method SMT-compliant.
To decide the unsatisfiability over the real numbers, an application of
the Real Nullstellensatz is implemented, in which existing methods for
semidefinite programming are combined with Gröbner bases to find sums
of squares, which are potential witnesses for unsatisfiability.
The experimental results show some promising applications, which
could be further improved by the implementation of the ideas from the
thesis’ comprehensive overview over both theoretical and technical
enhancements.