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.
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.