将BDD转换为CNF

Question

我有使用JavaBDD的BDD表示，我需要将它转换成连接正常形式，以便能够与另一个工具结合使用。我想知道实现转换的最佳方式是什么。提取一个DNF看起来很简单(只需提取到“1”的所有路径)，但我不确定什么是最好的方式来绕过CNF。任何想法都将不胜感激。

Answer 1

等效CNF的大小可以是BDD的指数大小。根据您的应用程序，可以引入辅助变量，例如使用将军澳变换。结果的CNF是可满足的当且仅当BDD是可满足的，但由于附加变量，它在逻辑上不是等价的。