Hier finden Sie wissenschaftliche Publikationen aus den Fraunhofer-Instituten.

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

: Dreyer, A.

Balle, Frank; Schryver, Christian de; Gerwalin, Sylvia; Kowalke, Thorsten; Kuhn, Thomas; Liebscher, André; Redenbach, Claudia; Steiner, Konrad ; Fraunhofer-Institut für Techno- und Wirtschaftsmathematik -ITWM-, Kaiserslautern; TU Kaiserslautern; Fraunhofer-Institut für Experimentelles Software Engineering -IESE-, Kaiserslautern:
Young Researcher Symposium, YRS 2013. Proceedings : 8. November 2013, Fraunhofer-Zentrum Kaiserslautern
Stuttgart: Fraunhofer Verlag, 2013
ISBN: 3-8396-0628-4
ISBN: 978-3-8396-0628-5
Young Researcher Symposium (YRS) <2, 2013, Kaiserslautern>
Fraunhofer ITWM ()

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.