Sciweavers

Share
ISQED
2002
IEEE

On the Relation between SAT and BDDs for Equivalence Checking

11 years 10 months ago
On the Relation between SAT and BDDs for Equivalence Checking
State-of-the-art verification tools are based on efficient operations on Boolean formulas. Traditional manipulation techniques are based on Binary Decision Diagrams (BDDs) and SAT solvers. In this paper, we study the relation between the two procedures and show how the number of backtracks obtained in the Davis-Putnam (DP) procedure is linked to the number of paths in the BDD. We utilize this relation to devise a method that uses BDD variable ordering techniques to run the DP procedure. Experimental results confirm that the proposed method results in a dramatic decrease in the number of backtracks and in the time needed to prove the Boolean satisfiability problem as well.
Sherief Reda, Rolf Drechsler, Alex Orailoglu
Added 15 Jul 2010
Updated 30 Aug 2010
Type Conference
Year 2002
Where ISQED
Authors Sherief Reda, Rolf Drechsler, Alex Orailoglu
Comments (0)
books