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.