今日の内容: 二分決定グラフの利用 (1)
Today's lecture: Using Binary Decision Diagrams (1)

• 二分決定グラフ (BDD) / Binary Decision Diagram (BDD)
• 2つの BDD の論理演算 / Logic operations with two BDDs
• Shared BDD: 処理系内で、関数を一意に表す
  / Shared BDD: Uniquely represent Boolean functions in a BDD management system
• 2つのハッシュを利用して、演算を高速化
  / Two hash techniques for faster logical operations
  • 節点テーブル : 等価な節点を何個も作らない
    / Node table: reducing equivalent nodes
  • 演算結果テーブル : 同じ演算を何回も実行しない
    / Operation result table: reducing the repetition of the same operations

今日の資料 / Materials

• Slides
  • 授業スライド (in Japanese) (PDF)
  • Slides (in English) (PDF)
• 最後の練習問題は、以前の「論理関数の表現方法」の資料と同じBDDを、 Apply 演算で作ってみようという問題です。 できあがった BDD は、以前に作ったものと同じです。 (変数順序を定めれば、BDD は一意に定まりますので。)

補足資料 / Supplementary Materials

• R. E. Bryant, Graph-Based Algorithms for Boolean Function Manipulation, IEEE Transactions on Computers, Vol. C-35, No. 8 (August, 1986), pp. 677–691.
  (Reprinted in M. Yoeli, Formal Verification of Hardware Design, IEEE Computer Society Press, 1990, pp. 253–267.)
  Electronic version with annotations available as PDF
• S. Minato, N. Ishiura, and S. Yajima, Shared Binary Decision Diagram with Attributed Edges for Efficient Boolean Function Manipulation, In Proc. of the 27th ACM/IEEE Design Automation Conference, Orlando, June 1990, pp. 52-57.
  (Available as PDF).
• R. E. Bryant, Binary Decision Diagrams: An Algorithmic Basis for Symbolic Model Checking, Handbook of Model Checking, E. M. Clarke, T. A. Henzinger, H. Veith, and R. Bloem, eds., Springer, 2018, pp. 191–218.
  (Available as PDF)
• R. Yoshinaka, J. Kawahara, S. Denzumi, H. Arimura, S. Minato, Counterexamples to the long-standing conjecture on the complexity of BDD binary operations, Information Processing Letters, 112(16): 636-640 (2012).
  (Available as PDF)

Created 2026.1.22, Takashi Horiyama