John Sass: Boolean polynomials and Gröbner bases: An Algebraic Approach to solving the SAT-problem

In this seminar we will discuss a method for solving the SAT-problem based on abstract algebra. The first step of the method is to convert the boolean formula to a set of ℤ₂-polynomials, and looking at the ideal generated by these polynomials. If this ideal coincides with the entire polynomial ring, then and only then is the original boolean formula unsatisfiable, and we determine if this is the case by looking at a Gröbner basis for this ideal. Such a basis can be found using the Buchberger algorithm, which in the general case is a double exponential time algorithm.

The seminar will be split into two 45-minute segments, with a ten minute break in between. In the first half of the seminar we will discuss the general method, including an introduction to multivariate polynomial reduction, Gröbner bases and the Buchberger algorithm. In the second half we will discuss the technical details, as well as implementation tricks and heuristic suggestions for the Buchberger algorithm which turn it into an exponential time algorithm. If there is time, we will also discuss how the method can be generalised and developed further.