Improving Gröbner-based Clause Learning for SAT Solving Industrial-sized Boolean Problems

In this paper, we refine an approach of Zengler and Küchlin. For generating additional binary clauses, they had proposed to use reduced Boolean Gröbner bases (BGB) during the conflict analysis phase of Conflict Driven Clause Learning (CDCL) Boolean Satisfiability Problem (SAT) solvers. For this purpose, they had selected a set of clauses for computing a Gröbner basis of the system of corresponding polynomials. But their selection strategy is not well-suited for generating binary clauses of typical SAT problems. In contrast, we will present an approach for selecting clauses of shorter length. In addition, our clauses share more common variables. Both properties improve SAT solving significantly. Finally, we evaluate this new strategy by solving 90 benchmarks from the SAT competition 2009. Here, our hybrid solver can learn much more binary clauses and save much time compared to hybrid solver of Zengler and Küchlin.