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 (Boolean satisfiability) 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.