Abstract
This paper presents an integrated infrastructure of CNF and BDD based tools to solve the Boolean Satisfiability problem. We use both CNF and BDDs not only as a means of representation, but also to efficiently analyze, prune and guide the search. We describe a method to successfully re-orient the decision making strategies of contemporary CNF tools in a manner that enables an efficient integration with BDDs. Keeping in mind that BDDs suffer from memory explosion problems, we describe learning-based search space pruning techniques that augment the already employed conflict analysis procedures of CNF tools. Our infrastructure is targeted towards solving those hard-to-solve instances where contemporary CNF tools invest significant search times. Experiments conducted over a wide range of benchmarks demonstrate the promise of our approach.