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?