Alexander Dreyer: Basics on Boolean Groebner Basis and Algebraic SAT solving

On Tuesday November 6 Alexander Dreyer from Fraunhofer ITWM, one of the leading experts world-wide on using algebraic methods for solving the SAT problem, will give a lunch seminar at KTH CSC. Please register for a light lunch served at 12 noon at doodle.com/p3cp59cc46hyc9ey . The seminar starts at 12:15 pm. We need your registration by Sunday 6 pm.

This will be a regular 45-60 minute lunch seminar with slides, and then after a break those interested have the opportunity to stay for a more detailed technical presentation.

Abstract

We will give a short introduction into the topic of Groebner basis, in particular we will scratch the surface of Boolean polynomials, i.e. those polynomials with coefficients in {0,1} and a fixed degree bound (per variable) of one.

This is accompanied with a brief presentation of the data structure proposed for Boolean polynomials in our software framework PolyBoRi for computing wit POlynomials in BOolean RIngs. These polynomials are the algebraic representation of Boolean function. This enables us to use techniques (like the Groebner basis formalism) from computational algebra for solving Boolean problems. Their special properties allow for representing them effectively as binary decision diagrams, but this will need for new heuristics and algorithms.

Finally, the talk will connect Groebner basis with the classical SAT solver approach for solving satisfiability problem of propositional logic.