研究している人はいるかもしれませんが、手法の確立に成功したのは、おそらく私のグループが初めてだと思います。
とくに、回路機能や回路仕様を表す代数方程式をZDD形式に変換した際、その記述には一意性があることが重要であり、これをグレブナー基底というのですが、変換後の記述がグレブナー基底ではない場合、ブッフベルガーのアルゴリズムを用いて再度変換する必要があります。つまり、①回路機能の方程式をZDD形式記述で表現→②グレブナー基底であることを確認→違う場合はブッフベルガーのアルゴリズムを用いて再度変換→③得られたZDD表現の等価性を検証、というのが従来の手順です。
しかし、ブッフベルガーのアルゴリズムを用いた変換は、大きな回路ほど計算量が膨れ上がり、かなりの時間を要します。それが最大の課題でした。
ですが、ここで大きなブレークスルーがありました。それはZDD形式記述に変換する際、ある変数順序に従って変換すれば、得られた方程式は必ずグレブナー基底になり、しかも高速変換が可能というものです。この成果は、そうしたブレークスルーが評価され、この分野のトップジャーナルに掲載されました。
ZDDに基づく形式記述に変換することで関数がコンパクトになることと、ある特殊な順序での変換がグレブナー基底に結びつくことは、それぞれ別の分野からヒントを得て構築した




