On Hybrid SAT Solving Using Tree Decompositions and BDDs
- Sathiamoorthy Subbarayan ,
- Lucas Bordeaux ,
- Youssef Hamadi
MSR-TR-2006-28 |
The goal of this paper is to study the benefits of hybridizing the CNF SAT Solvers with BDDs. Towards this we define a metric for the level of hybridization based on a tree decomposition of an input CNF. We also present a new linear time algorithm on BDDs, which is useful for efficient conflict analysis in any BDD-based hybrid SAT solver. Experiments on an implementation of our hybrid solver shows when to use such a hybridization.