通过CUDD计算图像后获取BDD的所有变量（C接口）答案

【问题标题】：Get all the variables of BDD after doing compute image by CUDD (C interface)通过CUDD计算图像后获取BDD的所有变量（C接口）
【发布时间】：2014-04-28 23:59:34
【问题描述】：

卡在CUDD的BDD上的操作（C接口），不知道在做计算图像时是否可以移除一些变量（从BDD的一个状态到另一个状态）以及如何传递结果BDD （最终 BDD）获取所有变量，谁能告诉我我们是否可以通过 CUDD 做到这一点？干杯

【问题讨论】：

标签： binary-decision-diagram cudd

【解决方案1】：

我从未使用过 CUDD，但 BDD 中使用的变量列表通常称为它的 support。从 BDD 中移除变量通常是通过存在量化来完成的。

抓取源代码，我找到了

/**Function********************************************************************

  Synopsis    [Finds the variables on which a DD depends.]

  Description [Finds the variables on which a DD depends.
  Returns a BDD consisting of the product of the variables if
  successful; NULL otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_VectorSupport Cudd_ClassifySupport]

  ******************************************************************************/
DdNode *
Cudd_Support(
  DdManager * dd /* manager */,
  DdNode * f /* DD whose support is sought */)

和

/**Function********************************************************************

  Synopsis [Existentially abstracts all the variables in cube from f.]

  Description [Existentially abstracts all the variables in cube from f.
  Returns the abstracted BDD if successful; NULL otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_bddUnivAbstract Cudd_addExistAbstract]

******************************************************************************/
DdNode *
Cudd_bddExistAbstract(
  DdManager * manager,
  DdNode * f,
  DdNode * cube)

【讨论】：

可爱，谢谢，我会试试的，另外，你能告诉我这里的“抽象”这个词到底是什么意思吗？我真的不明白，干杯。
a&b 是a&b&c 的抽象，您不关心c。相反，a&b&c 是a&b 的改进。
存在量化不能用于计算 BDD 中的变量。例如，在两个变量之间进行简单的 XOR。如果您使用 top 变量进行存在量化，您将丢失两个变量，即所需的存在量化的数量与变量的数量不同。事实上，CUDD 报告了正确的结果，但它没有使用存在量化。