Extending Clause Learning of SAT Solvers with Boolean Grobner Bases

We extend clause learning as performed by most modern SAT Solvers by integrating the computation of Boolean Grobner bases into the conflict learning process. Instead of learning only one clause per conflict, we compute and learn additional binary clauses from a Grobner basis of the current conflict. We used the Grobner basis engine of the logic package Redlog contained in the computer algebra system Reduce to extend the SAT solver MiniSAT with Grobner basis learning. Our approach shows a significant reduction of conflicts and a reduction of restarts and computation time on many hard problems from the SAT 2009 competition.