On Hybrid SAT Solving Using Tree Decompositions and BDDs

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.

tr-2006-28.pdf
PDF file

Details

TypeTechReport
NumberMSR-TR-2006-28
Pages18
InstitutionMicrosoft Research
> Publications > On Hybrid SAT Solving Using Tree Decompositions and BDDs