Home | Quick Search | Advanced Search | Bibliography submission | Bibliography submission using bibtex | Bibliography submission using bibtex file | Links | Help | Internal


TitleExtending clause learning of SAT solvers with Boolean Gr\"obner bases.
Author(s) Zengler Christoph, Wolfgang Küchlin
TypeBook, Chapter in Book, Conference Proceeding
AbstractWe extend clause learning as performed by most modern SAT Solvers by integrating the computation of Boolean Gröbner bases into the conflict learning process. Instead of learning only one clause per conflict, we compute and learn additional binary clauses from a Gröbner basis of the current conflict. We used the Gröbner basis engine of the logic package Redlog contained in the computer algebra system Reduce to extend the SAT solver MiniSAT with Gröbner 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.
URL http://link.springer.com/chapter/10.1007%2F978-3-642-15274-0_26
PublisherBerlin: Springer
Translation No
Refereed No