Anzeige
Erschienen in:
2012 | OriginalPaper | Buchkapitel
Cube and Conquer: Guiding CDCL SAT Solvers by Lookaheads
verfasst von : Marijn J. H. Heule, Oliver Kullmann, Siert Wieringa, Armin Biere
Erschienen in: Hardware and Software: Verification and Testing
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
Satisfiability (SAT) is considered as one of the most important core technologies in formal verification and related areas. Even though there is steady progress in improving practical SAT solving, there are limits on scalability of SAT solvers. We address this issue and present a new approach, called
cube-and-conquer
, targeted at reducing solving time on hard instances. This two-phase approach partitions a problem into many thousands (or millions) of cubes using lookahead techniques. Afterwards, a conflict-driven solver tackles the problem, using the cubes to guide the search. On several hard competition benchmarks, our hybrid approach outperforms both lookahead and conflict-driven solvers. Moreover, because
cube-and-conquer
is natural to parallelize, it is a competitive alternative for solving SAT problems in parallel.