我有使用JavaBDD的BDD表示，我需要将其转换为合取范式才能将其与其他工具结合使用。我想知道实施转换的最佳方法是什么。提取 DNF 似乎很简单（只需提取所有路径到"1"），但我不确定回合 CNF 的最佳方法是什么。任何想法将不胜感激。
将所有路径提取为 0。它们中的每一个都必须翻译成一个子句。
让 ¬A、B、C 成为您的 0 路径之一。相关子句将是 （A ∨ ¬B ∨ ¬C）。
一旦你有了所有的子句，只需在它们之间放一个∧！
该算法与您用于根据真值表计算 CNF 的算法相同。
等效的 CNF 的大小可以是 BDD 大小的指数级。根据您的应用，可以引入辅助变量，例如通过使用 Tseitin 变换。当且仅当 BDD 满足时，生成的 CNF 将满足，但由于附加变量，它在逻辑上不等效。