c++ - 不简化地在 CUDD 中表示 BDD

Question

是否可以使用 CUDD 获得 (x0 ∧ x1 ) ∨ (x0 ∧!x1 ) ∨ (!x0 ∧ x1 ) ∨ (!x 0 ∧!x 1 ) 的 bdd，它仍然具有代表变量 x0 和 x1 的节点? 我知道上面的布尔公式简化为常数函数 1。但我仍然想要一个不简化公式但将其表示为对应于 x0 和 x1 的 BDD“包含”节点的 BDD。如果不在 CUDD 中，是否可以使用其他工具来执行此操作？

Answer 1

您可能想试试 MEDDLY 图书馆。（https://meddly.sourceforge.io/）。

在这个库中可以使用不同类型的归约。例如，准归约永远不会跳过一个级别（变量）。这听起来像你想要的。

希望，这有帮助。

Answer 2

好吧，这可能不是有用的答案，但是如果您使用 ZDD（也称为 0-sup-BDD）并且表示常数 1，您将得到一个包含所有变量的图表 - 使用不同的缩减规则。我已经通过其他工具生成了它，但 CUDD 也支持 ZDD。