binary-decision-diagram - 将 BDD 转换为 CNF

Question

我有使用JavaBDD的 BDD 表示，我需要将其转换为连接范式，以便能够将它与另一个工具结合使用。我想知道实现转换的最佳方法是什么。提取 DNF 似乎很简单（只需提取到“1”的所有路径），但我不确定什么是解决 CNF 的最佳方法。任何想法将不胜感激。

Answer 1

将所有路径提取到 0。它们中的每一个都必须翻译成一个子句。

让 ¬A、B、C 成为您的 0 路径之一。相对子句将是 (A ∨ ¬B ∨ ¬C)。

一旦你有了所有的子句，只需在它们之间放一个∧！

该算法与您用于从真值表计算 CNF的算法相同。

Answer 2

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