c++ - 在不简化的情况下在 CUDD 中表示 BDD

Question

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

Answer 1

您可能想尝试 MEDDLY 图书馆。 (https://meddly.sourceforge.io/)。

可以在此库中使用不同类型的归约。例如，准归约从不跳过一个级别(变量)。这听起来像你想要的。

希望对您有所帮助。