Portal de Periódicos da CAPES

BDD-Guided Clause Generation

2015; Springer Science+Business Media; Linguagem: Inglês

10.1007/978-3-319-18008-3_15

1611-3349

Brian Kell, Ashish Sabharwal, Willem‐Jan van Hoeve,

Model-Driven Software Engineering Techniques

Nogood learning is a critical component of Boolean satisfiability (SAT) solvers, and increasingly popular in the context of integer programming and constraint programming. We present a generic method to learn valid clauses from exact or approximate binary decision diagrams (BDDs) and resolution in the context of SAT solving. We show that any clause learned from SAT conflict analysis can also be generated using our method, while, in addition, we can generate stronger clauses that cannot be derived from one application of conflict analysis. Importantly, since SAT instances are often too large for an exact BDD representation, we focus on BDD relaxations of polynomial size and show how they can still be used to generated useful clauses. Our experimental results show that when this method is used as a preprocessing step and the generated clauses are appended to the original instance, the size of the search tree for a SAT solver can be significantly reduced.