Convert BDD to CNF

Question

I have BDD representation using JavaBDD which I need to convert to conjunctive normal form to be able to use it in combination with another tool. I wonder what would be the best way to implement the conversion. Extracting a DNF seems simple enough (just extract all paths to "1") but I am not sure what would be the best way to go bout CNF. Any ideas would be greatly appreciated.

Answer 1

Extract all the paths to 0. Each of them must be translated into a clause.

Let ¬A, B, C be one of your 0-paths. The relative clause will be (A ∨ ¬B ∨ ¬C).

Once you have all the clauses, simply put an ∧ between them!

The algorithm is the same that you use to calculate a CNF from a truth table.

Answer 2

An equivalent CNF can have a size that is exponential in the size of the BDD. Depending on your application it may be OK to introduce auxiliary variables e.g. by using the Tseitin transformation. The resulting CNF will be satisfiable if and only if the BDD is satisfiable, but it is not logically equivalent due to the additional variables.