Boolean Gröbner bases in SAT solving
Christoph Zengler, Wolfgang Küchlin · ACM communications in computer algebra · 2011
We want to incorporate the reasoning power of Boolean Gröbner bases into modern SAT solvers. There are many starting points where to plug in the Gröbner bases engine in the SAT solving process. As a first step we chose the learning part where new consequences (lemmas) of the original formula are deduced. This paper shows first promising results, also published at the CASC 2010 in Armenia [1].