抽象的なハードウェア設計の検証において、uninterpreted functions(UIFs)を含む 等号付論理が利用されているが、このとき充足可能性を高速に判定できることが必要 とされる。今回、二分決定グラフ(BDD)を用いた2つの充足可能性判定手続きとその実験 的評価に関する論文を紹介する。
Back