二分決定図 (BDD / ZDD)
論理関数を表現する DAG 型データ構造。変数を順に分岐させ、同型な部分木を共有することで論理関数を圧縮表現する。
ZDD
Zero-suppressed BDD。集合族（組合せ集合）を表すバリアント。
- 圧縮表現のまま union / intersection / difference といった集合演算を計算できる
- ただし演算が正しく行えるには 簡約化 されている必要がある（冗長な節点が無く、表現が一意であること）
簡約化と並列化
トップダウンに構築した BDD は冗長性が生じやすく、演算ごとに簡約化が必要。
- Knuth09 の簡約化アルゴリズムは
- これをさらに高速化したい → ハードウェアによる高速化、本研究では 並列準簡約化と追駆簡約化 による新しい並列化（先行研究の並列化手法と直交＝因果関係のない別軸の手法）
SAT と同じく論理関数を扱うが、BDD は関数全体を一意な正規形として保持する点が異なる。
関連: boolean-satisfiability-sat / parallel-computing / _moc-algorithm