命題指向非巡回グラフ

命題有向非巡回グラフ（PDAG）は、ブール関数を表すために使用されるデータ構造です。ブール関数は、次の形式の根付き有向非巡回グラフとして表現できます。

• 葉にはラベルが付けられています${\displaystyle \top }$（真実）、${\displaystyle \bot }$（偽）、またはブール変数。
• 非葉は${\displaystyle \bigtriangleup }$（論理的かつ）${\displaystyle \bigtriangledown }$（論理和）かつ${\displaystyle \Diamond }$（論理否定）。
• ${\displaystyle \bigtriangleup }$- そして${\displaystyle \bigtriangledown }$-ノードには少なくとも1つの子ノードが存在する。
• ${\displaystyle \Diamond }$-ノードは子ノードをちょうど1つ持ちます。

ラベルの付いた葉${\displaystyle \top }$（${\displaystyle \bot }$）は、常に 1 (0) と評価される定数ブール関数を表します。ブール変数でラベル付けされた葉。${\displaystyle x}$割り当てとして解釈される${\displaystyle x=1}$つまり、これは、次の場合にのみ 1 と評価されるブール関数を表します。${\displaystyle x=1}$。ブール関数は、${\displaystyle \bigtriangleup }$-node は、そのすべての子のブール関数が 1 と評価される場合に限り 1 と評価されます。同様に、${\displaystyle \bigtriangledown }$-node は、少なくとも 1 つの子のブール関数が 1 と評価される場合に限り 1 と評価されるブール関数を表します。最後に、${\displaystyle \Diamond }$-node は、その子の補数ブール関数を表します。つまり、その子のブール関数が 0 と評価される場合に限り 1 と評価される関数です。

すべての二分決定図 (BDD)とすべての否定正規形 (NNF)は、特定の特性を持つ PDAG でもあります。以下の図は、ブール関数f(x1, x2, x3) = -x1 * -x2 * -x3 + x1 * x2 + x2 * x3 を表しています。

• 
  関数fのBDD
• 
  BDDから得られた関数fのPDAG
• 
  関数fのPDAG

• データ構造
• ブール充足可能性問題
• 命題
• ブール回路

• M. Wachter & R. Haenni、「命題的DAG：ブール関数を表現するための新しいグラフベースの言語」、KR'06、第10回知識表現と推論の原理に関する国際会議、英国レイクディストリクト、2006年。
• M. Wachter & R. Haenni、「命題DAGを用いた確率的等価性チェック」、技術報告書 iam-2006-001、ベルン大学コンピュータ科学・応用数学研究所、スイス、2006年。
• M. Wachter、R. Haenni、J. Jonczy、「モジュールシステムの信頼性と診断：新しい確率論的アプローチ」、DX'06、第18回診断原理に関する国際ワークショップ、ペニャランダ・デ・ドゥエロ、ブルゴス、スペイン、2006年。