OBDDにおける入力反転エッジの応用に関する研究

摘要

本研究ではOBDD と呼ばれる論理関数を表すグラフ表現について，より効率的な構造を構成する方法について検討した.OBDD とはordered binary decision diagram の略称で, 二分順序決定ダイアグラムと訳され, 論理関数を表すグラフ表現である. OBDD では非終端ノードが命題変数を, 終端ノードが論理関数の真理値を表しており, エッジにはラベルとして,0 ないし1 が記載されている. 論理式を表したOBDD と, 各命題変数への真偽の割り当てが与えられると, 与論理式の真偽を計算することができる.