BDD to CNF in linear time I have a book from my university that claims:


  There is an linear algorithm that can convert BDD to CNF in linear time, and generate CNF in linear length of the BDD size (number of nodes).


Then they wrote an exercise to find one...  

Actually I tried to do so, I thought to find the paths that brings me to 0, and then translate them to clause (with the opposite value of the variables), and use Tseytin transformation to create linear length of CNF.

The problem are:


How can I find all the paths to 0? I thought about DFS but it seems to be complex task for DFS because I need the variables value (the naive algorithm is exponential)
The other problem is the variables to add, when should I create a new variable, every move? It can cause an exponential number of variables, which is not good.


So what is the correct algorithm to do that?
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?