On Hybrid SAT Solving Using Tree Decompositions and BDDs

Sathiamoorthy Subbarayan, Lucas Bordeaux, and Youssef Hamadi

Abstract

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.

Details

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