Integrating CNF and BDD based SAT solvers

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