BDD to CNF in linear time
This is a nice exercise.  I'll give you a series of hints.  Click on each hint only after you've spent a good amount of time thinking on the previous one.  You'll get the most value by solving this on your own.

Hint #1:


   Add extra variables.


Hint #2:


   Use the Tseitin transform.  Review to convert CircuitSAT to SAT.


Hint #3:


   Introduce a boolean variable $x_v$ for each node $v$ in the BDD.


Hint #4:


   The idea is that $x_v$ should be true iff the path you follow goes through $x_v$.  Can you write clauses to ensure all of this?