binary-decision-diagram - CUDD (C インターフェイス) で画像を計算した後、BDD のすべての変数を取得します。

Question

CUDD (C インターフェイス) の BDD での操作に行き詰まっています。イメージの計算 (BDD の状態から別の状態へ) を行うときにいくつかの変数を削除できるかどうか、および結果の BDD (最終 BDD) を移動する方法がわかりません。 ) すべての変数を取得するには、CUDD でそれができるかどうか誰か教えてください。乾杯

Answer 1

CUDD を使用したことはありませんが、BDD で使用される変数のリストは通常​​、そのサポートと呼ばれます。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)