"n個n≧2の変数を有する関数を表現する二分決定図BDDであって、前記n個の変数にそれぞれ対応するn個のレイヤを有するBDDにアクセスするステップと、前記n個の変数の1つの順序付けされた集合の1つのグループを構成するステップと、既存の各グループがk個以下1≦k<nの変数の1以上の順序付けされた集合を有するまで、1以上の変数の1以上の順序付けされた集合の1以上の新たなグループを再帰的に構成し、1以上の変数の1以上の順序付けされた集合の1以上の既存のグループを置換するステップと、前記1以上の既存のグループのそれぞれについて、前記グループ内で取得される前記BDDの複数の異なる変数順序において最小のサイズをもたらすローカルに最適な変数順序を決定するステップと、前記1以上の既存のグループに対応する1以上のローカルに最適な変数順序から、前記1以上の既存のローカルに最適な変数順序において最小のサイズをもたらす前記BDDの最適な変数順序を選択するステップと、を有する1以上の計算装置により実行される方法であって、各繰り返しは、既存の各グループについて、n’個の変数を現在有する前記既存のグループの順序付けされた各集合に対して、n’>kである場合、部分集合の各ペアについて、第1部分集合が前記集合のn’個の変数の個を有し、第2部分集合が前記集合のn’個の変数の個を有する、部分集合の1以上のペアに前記集合を分離するステップと、前記既存のグループの順序付けされた各集合を対応する前記順序付けされた集合を分離することによって構成される部分集合の1以上のペアとそれぞれ置換することによって、前記既存のグループを置換するための1以上の新たなグループを構成するステップと、を有する方法。k=4である、請求項1記載の方法。各繰り返しはさらに、既存の各グループについて、n’個の変数を現在有する前記既存のグループの順序付けされた各集合に対して、n’=5である場合、部分集合の各ペアについて、第1部分集合が前記集合の5個の変数の4個を有し、第2部分集合が前記集合の5個の変数の1個を有する、前記部分集合の1以上のペアに前記集合を分離するステップを有する、請求項2記載の方法。前記BDDの最適な変数順序に従って前記BDDのn個の変数をリオーダするステップをさらに有する、請求項1記載の方法。前記BDDにより表現される関数は、電子回路が充足すべき前記電子回路の性質を規定する、請求項1記載の方法。前記BDDにより表現される関数は、システムのフォーマルベリフィケーションに使用される1以上の遷移関係又は1以上の到達可能な状態空間を規定する、請求項1記載の方法。1以上のプロセッサにより実行可能な命令を有するメモリと、前記メモリに接続され、前記命令を実行するよう動作可能な前記1以上のプロセッサと、を有するシステムであって、前記1以上のプロセッサは、前記命令が実行されると、n個n≧2の変数を有する関数を表現する二分決定図BDDであって、前記n個の変数にそれぞれ対応するn個のレイヤを有するBDDにアクセスするステップと、前記n個の変数の1つの順序付けされた集合の1つのグループを構成するステップと、既存の各グループがk個以下1≦k<nの変数の1以上の順序付けされた集合を有するまで、1以上の変数の1以上の順序付けされた集合の1以上の新たなグループを再帰的に構成し、1以上の変数の1以上の順序付けされた集合の1以上の既存のグループを置換するステップと、前記1以上の既存のグループのそれぞれについて、前記グループ内で取得される前記BDDの複数の異なる変数順序において最小のサイズをもたらすローカルに最適な変数順序を決定するステップと、前記1以上の既存のグループに対応する1以上のローカルに最適な変数順序から、前記1以上の既存のローカルに最適な変数順序において最小のサイズをもたらす前記BDDの最適な変数順序を選択するステップと、を実行するよう動作可能であり、各繰り返しは、既存の各グループについて、n’個の変数を現在有する前記既存のグループの順序付けされた各集合に対して、n’>kである場合、部分集合の各ペアについて、第1部分集合が前記集合のn’個の変数の個を有し、第2部分集合が前記集合のn’個の変数の個を有する、部分集合の1以上のペアに前記集合を分離するステップと、前記既存のグループの順序付けされた各集合を対応する前記順序付けされた集合を分離することによって構成される部分集合の1以上のペアとそれぞれ置換することによって、前記既存のグループを置換するための1以上の新たなグループを構成するステップと、を有するシステム。n個n≧2の変数を有する関数を表現する二分決定図BDDであって、前記n個の変数にそれぞれ対応するn個のレイヤを有するBDDにアクセスするステップと、前記n個の変数の1つの順序付けされた集合の1つのグループを構成するステップと、既存の各グループがk個以下1≦k<nの変数の1以上の順序付けされた集合を有するまで、1以上の変数の1以上の順序付けされた集合の1以上の新たなグループを再帰的に構成し、1以上の変数の1以上の順序付けされた集合の1以上の既存のグループを置換するステップと、前記1以上の既存のグループのそれぞれについて、前記グループ内で取得される前記BDDの複数の異なる変数順序において最小のサイズをもたらすローカルに最適な変数順序を決定するステップと、前記1以上の既存のグループに対応する1以上のローカルに最適な変数順序から、前記1以上の既存のローカルに最適な変数順序において最小のサイズをもたらす前記BDDの最適な変数順序を選択するステップと、を1以上のコンピュータシステムに実行させるソフトウェアを格納する非一時的なコンピュータ可読記憶媒体であって、各繰り返しは、既存の各グループについて、n’個の変数を現在有する前記既存のグループの順序付けされた各集合に対して、n’>kである場合、部分集合の各ペアについて、第1部分集合が前記集合のn’個の変数の個を有し、第2部分集合が前記集合のn’個の変数の個を有する、部分集合の1以上のペアに前記集合を分離するステップと、前記既存のグループの順序付けされた各集合を対応する前記順序付けされた集合を分離することによって構成される部分集合の1以上のペアとそれぞれ置換することによって、前記既存のグループを置換するための1以上の新たなグループを構成するステップと、を有する記憶媒体。n個n≧2の変数を有する関数を表現する二分決定図BDDであって、前記n個の変数にそれぞれ対応するn個のレイヤを有するBDDにアクセスする手段と、前記n個の変数の1つの順序付けされた集合の1つのグループを構成する手段と、既存の各グループがk個以下1≦k<nの変数の1以上の順序付けされた集合を有するまで、1以上の変数の1以上の順序付けされた集合の1以上の新たなグループを再帰的に構成し、1以上の変数の1以上の順序付けされた集合の1以上の既存のグループを置換する手段と、前記1以上の既存のグループのそれぞれについて、前記グループ内で取得される前記BDDの複数の異なる変数順序において最小のサイズをもたらすローカルに最適な変数順序を決定する手段と、前記1以上の既存のグループに対応する1以上のローカルに最適な変数順序から、前記1以上の既存のローカルに最適な変数順序において最小のサイズをもたらす前記BDDの最適な変数順序を選択する手段と、を有するシステムであって、各繰り返しは、既存の各グループについて、n’個の変数を現在有する前記既存のグループの順序付けされた各集合に対して、n’>kである場合、部分集合の各ペアについて、第1部分集合が前記集合のn’個の変数の個を有し、第2部分集合が前記集合のn’個の変数の個を有する、部分集合の1以上のペアに前記集合を分離する手段と、前記既存のグループの順序付けされた各集合を対応する前記順序付けされた集合を分離することによって構成される部分集合の1以上のペアとそれぞれ置換することによって、前記既存のグループを置換するための1以上の新たなグループを構成する手段と、を有するシステム。本発明の課題は、上記問題点に鑑み、再帰を利用してBDDの最適な変数順序を決定する方法及びシステムを提供することである。本開示の一実施例では、計算装置が、n個n≧2の変数を有する関数を表現する二分決定図BDDであって、前記n個の変数にそれぞれ対応するn個のレイヤを有するBDDにアクセスし、前記n個の変数の1つの順序付けされた集合の1つのグループを構成し、既存の各グループがk個以下1≦k<nの変数の1以上の順序付けされた集合を有するまで、1以上の変数の1以上の順序付けされた集合の1以上の新たなグループを再帰的に構成し、1以上の変数の1以上の順序付けされた集合の1以上の既存のグループを置換し、前記1以上の既存のグループのそれぞれについて、前記グループ内で取得される前記BDDの複数の異なる変数順序において最小のサイズをもたらすローカルに最適な変数順序を決定し、前記1以上の既存のグループに対応する1以上のローカルに最適な変数順序から、前記1以上の既存のローカルに最適な変数順序において最小のサイズをもたらす前記BDDの最適な変数順序を選択する。各繰り返しは、既存の各グループについて、n’個の変数を現在有する前記既存のグループの順序付けされた各集合に対して、n’>kである場合、部分集合の各ペアについて、第1部分集合が前記集合のn’個の変数の1/2n’/2が整数でない場合は切り上げ個を有し、第2部分集合が前記集合のn’個の変数のn’/2が整数でない場合は切り下げ個を有する、部分集合の1以上のペアに前記集合を分離し、前記既存のグループの順序付けされた各集合を対応する前記順序付けされた集合を分離することによって構成される部分集合の1以上のペアとそれぞれ置換することによって、前記既存のグループを置換するための1以上の新たなグループを構成することを有する。本発明によると、再帰を利用してBDDの最適な変数順序を決定する方法及びシステムを提供することができる。以下、図面に基づいて本発明の実施の形態を説明する。二分決定図BDDは、ブール関数を表現するのに使用されるデータ構造である。BDDは、1以上の内部の決定ノードと2つの終端ノードとを有するルートのある有向アサイクリックグラフとしてグラフ表現されてもよい。各決定ノードは、ブール関数の異なる変数を表し、典型的にはグラフ内で丸の記号により示される。2つの終端ノードである0終端ノードと1終端ノードとは、典型的には、グラフ内で正方形の記号により示される。各決定ノードは、典型的には、グラフ内で破線として示される0エッジと、グラフ内で実線として示される1エッジとを有する。各エッジは、他の決定ノード又は終端ノードの1つに接続されてもよい。グラフ内の各パスは、1以上の決定ノードとそれらに関連するエッジとによって形成され、最終的に0終端ノード又は1終端ノードに導かれる。あるパスを形成する各決定ノードは、ブール関数の異なる変数を表す。すなわち、1つのパス上の何れの2つの決定ノードも同一の変数を表すものでない。0終端ノードに導かれるパスは、当該パス上の決定ノードにより表される変数に割り当てられた各値に対してブール関数がFALSEとなることを示し、1終端ノードに導かれるパスは、当該パス上の決定ノードにより表される変数に割り当てられた各値に対してブール関数がTRUEとなることを示す。図1は、4つの変数x1,x2,x3,x4を有するブール関数を表現する一例となるBDD100を示す。BDD100により表現されるブール関数は4つの変数を有するため、BDD100は、高々4つの決定ノードレイヤ、すなわち、レイヤ1~4を有する。すなわち、BDD100には各レイヤが少なくとも1つの決定ノードを有する高々4つのレイヤがある。より詳細には、図1において、変数x1を表す決定ノードはBDD100のレイヤ1にあり、変数x2を表す決定ノードはBDD100のレイヤ2にあり、変数x3を表す決定ノードはBDD100のレイヤ3にあり、変数x4を表す決定ノードはBDD100のレイヤ4にある。決定ノードとそれらの関連するエッジとにより形成されるBDD100の各パスは、0終端ノード又は1終端ノードの何れかに導かれ、それぞれがブール関数がFALSE又はTRUEと評価されることを示す。理解を容易にするため、図1では、0終端ノードと1終端ノードは複数示されることに留意されたい。実際、BDD100は、BDD100のノードのいくつかが冗長であり、BDD100の一部が同型的isomorphicであるとき、ブール関数の最適化された表現とはならない。例えば、0終端ノードで終了するパス102,104を考える。パス102,104上の決定ノードを検討することによって、変数x3を表す決定ノード152がそれの1エッジに沿って分岐する限り、変数x4を表す決定ノード154が何れの分岐に進むかにかかわらず、ブール関数はFALSEとなることが判断される。従って、決定ノード154は、0終端ノードと置換されてもよい。同様に、パス112,114,116,118はすべて1終端ノードで終端する。これら4つのパス上の決定ノードを検討することによって、変数x2を表す決定ノード162がそれの1エッジに沿って分岐する限り、変数x3を表す決定ノード164と、変数x4を表す決定ノード166,168とが何れの分岐に進むかにかかわらず、ブール関数はTRUEになることが判断される。従って、決定ノード164,166,168は、1終端ノードと置換されてもよい。他の例として、変数x4を表す決定ノード172,174を考える。決定ノード172,174は共に、0エッジが0終端ノードに導かれ、1エッジが1終端ノードに導かれる。従って、それらは互いに重複する、すなわち、同型的である。従って、それらの一方はBDD100から削除されてもよい。図2は、BDD100により表現されるものと同一のブール関数を表現する、BDD100より最適化された一例となるBDD200を示す。BDD200は、BDD100の冗長な決定ノードと同型的な部分とを削除した結果として、より少ないノードを使用して同一のブール関数を表現している。冗長な決定ノードと同型的な部分グラフとが削除され、BDDのすべてのパスに沿ってルートから終端ノードまで同じ順序で決定ノードが出現するBDDは、既約順序付け二分決定図ROBDDと呼ばれる。ROBDDの効果は、それがある関数と変数の順序についてカノニカルcanonicalであり、関数等価性チェックや関数テクノロジーマッピングなどの各種の実際的なアプリケーションにおいて有用であることである。ROBDDは、2つの重要な性質を有する。第1に、ROBDDは順序付けされている。すなわち、任意の非終端ノードvに対して、lowv及びhighvもまた非終端ノードである場合、indexlowv=πkとindexhighv=πqが成り立つようなただし、k>π-1indexv、q>π-1indexvである固定的な順序π{1,...,n}→{x1,...,xn}が存在する。第2に、ROBDDは既約である。すなわち、lowv=highvとなるような非終端ノードが存在せず、v及びv’をルートとする部分BDDが同型的なものとなるような2つの非終端ノードv,v’が存在しない。ここで、非終端ノードとは決定ノードである。例えば、図2において、BDD200は、それが4つの変数を有するブール関数を表現するとき、4つのレイヤを有する。BDD200は順序付けされているため、各レイヤはある変数に対応する決定ノードを含む。例えば、レイヤ2は、変数x2のみに対応する決定ノードを有し、他の変数x1,x3又はx4などに対応する決定ノードを有さない。ブール関数fx1,...,xnは、2以上のブール関数f1x1,...,xnからfmx1,...,xnに分割又はパーティションpartitionされてもよい。各ブール関数f1からfmは、オリジナルのブール関数fのパーティションとみなされてもよい。各ブール関数f1からfmがBDDにより表現される場合、オリジナルのブール関数fを表すBDDは、fのパーティションすなわち、f1からfmを表すすべてのBDDの論理ORをとることによって取得されてもよい。ある実施例では、ブール関数f1からfmを表すBDDのそれぞれはROBDDであってもよく、オリジナルのブール関数fを表すBDDに関するパーティションされた既約順序付け二分決定図POBDDと呼ばれてもよい。[BDD変数の順序]BDDのサイズは、それが表現するブール関数と当該関数の変数の選択された順序との双方によって決定される。BDDのサイズは、それの各レイヤのすべてのサイズの合計である。ある実施例では、BDDのサイズは、BDDの決定ノードの個数に関して表されてもよい。同様に、BDDのレイヤのサイズは、当該レイヤにおける決定ノードの個数に関して表されてもよい。変数x1,...,xnの順序付けに応じてBDDにより表現されるブール関数fx1,...,xnが与えられると、グラフのノードの個数は、nに関してベストケースでは線形であり、ワーストケースでは指数的である。例えば、変数順序x1<x3<<x2n-1<x2<x4<<x2nを用いたブール関数fx1,...,xn=x1x2x3x4x2n-1x2nに対して、図3に示されるように、BDDは、ブール関数を表現するため2n1個のノードを必要とする。他方、変数順序x1<x2<x3<x4<<x2n-1<x2nを用いると、図4に示されるように、BDDは、同じブール関数を表現するのに2n個のノードしか必要としない。この例が示すように、変数順序は、BDDのサイズがそれの変数順序の変化に従ってしばしば大きく変動するため、BDDに対して決定的な最適化問題を示す。BDDのあるレイヤが与えられると、第1変数x1などが当該レイヤに配置されるとき、当該レイヤは1つのサイズを有する。第2変数x2などが同じレイヤに配置されると、当該レイヤは他の異なるサイズを有する。さらに、あるレイヤレイヤ3などに配置されるある変数x3などを有するBDDの当該レイヤが与えられると、変数に関するレイヤのサイズは、当該レイヤより上位のレイヤレイヤ1及び2など及び下位のレイヤレイヤ4などに配置される特定の変数に依存する。従って、例えば、変数x3がレイヤ3に配置される場合、変数x1,x2がレイヤ1,2に配置され、変数x4がレイヤ4に配置されると、変数x3に関するレイヤ3は1つのサイズを有する。しかしながら、変数x4,x1がレイヤ1,2に配置され、変数x2がレイヤ4に配置されると、変数x3に関するレイヤ3は、変数x3がレイヤ3にあっても、他の異なるサイズを有する可能性がある。BDD変数の順序付けに関する研究がなされてきた。BDD変数の順序付けの目標は、一般に必要とされるBDDノードの個数が最小化され、関数を表現するBDDのサイズを低減できるように、関数の変数の最適な又は実質的に最適な変数順序を求めることである。一般に、BDDのサイズが最小となるBDDの最適な変数順序を求めるため、BDDのサイズが最小となる変数の順序置換が求められるように、BDDの変数の必ずしも可能な全てではないが多数の順序の置換を調べることが必要であるかもしれない。この順序の置換は、BDDの最適な変数順序をもたらす。変数の具体的な各順序の置換はBDDの異なる変数順序を示すことに留意されたい。しかしながら、実際には、BDDの変数の可能性のある全ての順序の置換を求め、BDDの可能性のある全ての変数の順序を求めることは、n個の変数の関数を表現するBDDに対してこれらの変数の可能性のある順序の置換はnnの階乗であり、n=1×2××n通り存在するため、要求される時間とリソースに関して大変コストのかかるものとなる。BDDの変数の異なる順序の置換を調べるため、BDDの変数が、適切なリオーダアルゴリズムReorderingAlgorithmを用いてリオーダされてもよい。それらの最もシンプルな形式では、リオーダアルゴリズムは、BDDの変数の現在の順序の置換を他の異なる順序の置換に変換する。BDDの最後の順序の置換は、例えば、ある人によって指定されてもよいし例えば、ある設計仕様又はパフォーマンス基準などに従って、又はBDDが使用されるアプリケーションに基づき決定されてもよい。BDD変数のリオーダアルゴリズム又は処理に関する研究の大多数は、BDDの2つの連続するレイヤはBDDの残りに影響を与えることなく効率的にスワップ又は交換可能であるという性質を利用する。BDDの2つのレイヤを交換することによって、これら2つのレイヤにおける2つの対応する変数の順序はまた交換され、これにより、各交換によってBDDの変数の2つをリオーダすることができる。従って、変数リオーダアルゴリズムは、あるターゲット目標に到達するまで、ローカルな交換を適用することによって所与のBDDを変換する。図5は、BDDのための一例となる変数リオーダ処理を示す。これは、最も一般的に使用されるリオーダアルゴリズムの1つであり、BDDの2つの連続するレイヤの交換を繰り返し実行することによって、各変数をそれの正しい最終位置に移動させるものである。説明の簡単化のため、リオーダアルゴリズムは、任意数の変数を有する関数を表現するBDDに適用されてもよいが、4つの変数を有する関数を表現するBDD500を用いて説明される。以降において、図面の水平方向のラインはBDDレイヤを表し、垂直方向のラインはレイヤの交換を表す。4つの変数があるため、BDD500は、レイヤ1~4に対応する4つの水平方向のラインを示す。まず、BDD500は、変数1がレイヤ1にあり、変数2がレイヤ2にあり、変数3がレイヤ3にあり、変数4はレイヤ4にある第1変数順序を有する。初期的な第1変数順序と異なって、変数1がレイヤ4にあり、変数2がレイヤ3にあり、変数3がレイヤ2にあり、変数4がレイヤ1にある第2変数順序を実現するため、BDD500の4つの変数をリオーダすることが所望されると仮定する。変数1をレイヤ4に移すため、リオーダアルゴリズムはまず、レイヤ1とレイヤ2とを交換するすなわち、スワップ501。スワップ501の後、変数2はレイヤ1にあり、変数1はレイヤ2にある。次に、レイヤ2とレイヤ3とが交換されすなわち、スワップ502、その後、変数3がレイヤ2にあり、変数1がレイヤ3にある。最後に、レイヤ3とレイヤ4とが交換されるすなわち、スワップ503。この時点では、変数1は所望の位置であるレイヤ4にあり、変数4はレイヤ3にある。変数2をレイヤ3に移すためここで、スワップ501によって、変数2は現在レイヤ1にある、レイヤ1とレイヤ2とが再び交換されすなわち、スワップ504、その後に、変数3がレイヤ1にあり、変数2がレイヤ2にある。次に、レイヤ3とレイヤ4とが交換されるすなわち、スワップ505。この時点では、変数2が所望の位置であるレイヤ3にあり、変数4がレイヤ2にある。変数3をレイヤ2に移すためここで、変数3は現在レイヤ1にある、レイヤ1とレイヤ2とが交換されるすなわち、スワップ506。この時点では、変数3はレイヤ2にあり、変数4はレイヤ1にある。所望の第2変数順序がBDD500に対して実現され、リオーダアルゴリズムが終了される。図5に示されるように、BDD500の4つの変数を第1変数順序から第2変数順序にリオーダするためにすなわち、BDDを第1変数順序置換から第2変数順序置換に変換するため、合計で6回のレイヤスワップを要する。BDDの2つの連続するレイヤはBDDの残りに影響を与えることなく交換可能である。従って、連続するレイヤの分離されたペアは、連続するレイヤの1つのペアの交換が他の何れのレイヤにも影響を与えず、従って他の何れの連続するレイヤのペアにも影響を与えないため、同時に交換されてもよい。BDDの連続するレイヤのペアは、互いに隣り合う何れか2つのレイヤである例えば、1≦i≦n-1に対して、レイヤiとレイヤi1など。連続するレイヤの2つの互いに素であるペアは、共通するレイヤを共有しない連続するレイヤの2つのペアである例えば、一方のペアがレイヤiとレイヤi1であり、他方のペアがレイヤi2とレイヤi3など。図5において、レイヤ3とレイヤ4との間のスワップ503は、レイヤ1とレイヤ2との間のスワップ504に続く。レイヤ3,4とレイヤ1,2とは、これら2つのレイヤのペアが共通するレイヤを共有しないため、連続するレイヤの互いに素である2つのペアである。従って、スワップ503と504とは、これらのスワップが互いに影響を与えないためすなわち、これら2つのスワップは互いの結果に依存しない、同時にすなわち、パラレルに実行されてもよい。他方、レイヤ1とレイヤ2との間のスワップ501は、レイヤ2とレイヤ3との間のスワップ502に続く。レイヤ1,2とレイヤ2,3とは、これら2つのペアが共通するレイヤ2を共有するため、連続するレイヤの2つの互いに素なペアでない。従って、スワップ501と502とは、スワップ502がその実行前にスワップ501の結果を必要とするため、同時には実行できない。[変数リオーダアルゴリズム]BDDの変数順序は、BDDにより表現される関数の何れの変数がBDDの何れのレイヤに配置されるか示す。BDDの最適な変数順序は、BDDの変数の可能性のある全ての変数の順序の置換に対してBDDのサイズが最小となる、BDDにより表現される関数の変数の順序付けである。一般に、BDDは、1以上の最適な変数順序を有する可能性がある。n個の変数を有する関数を表現するBDDが与えられると、それの最適な変数順序を求めるのに利用可能な異なるアルゴリズム又は処理が存在する。単純変更アルゴリズムBDDの最適な変数順序を決定するのに一般的に使用されるアルゴリズムは、単純変更plainchangeと呼ばれる転置ネットワークアルゴリズムに基づく。これは、当該アルゴリズムが所与のBDDに対して正確に最適な変数順序を決定可能であるという理由のためすなわち、最小サイズを有するBDDをもたらすBDDの変数順序、イグザクトアルゴリズムexactalgorithmである。単純変更アルゴリズムによって、BDDの変数の可能性のある全ての順序の置換が取得され、これにより、BDDが最小サイズを有する変数順序を検出することができる。この変数順序は、BDDの最適な変数順序とみなされる。n個の変数の関数を表現するBDDに対して、単純変更アルゴリズムは、可能性のある全てのn個の変数順序の置換をカバーするため、BDDの連続する2つのレイヤの間のn-1回のスワップが実行されることを要求する。BDDは常に初期的な変数順序を有し、1つの変数順序の置換はレイヤスワップを要することなくすでに取得されていることに留意されたい。その後、BDDのn個の変数は、適切なリオーダアルゴリズムを用いて最適な変数順序を実現することによってリオーダされる。図6は、2,3及び4個の変数をそれぞれ有する関数を表現するBDDに適用される、レイヤスワップが実行される単純変更アルゴリズムを示す。図6において、BDD610は、2つの変数すなわち、n=2に対応する2つのレイヤを有する。BDD610の2つの変数に対して2つの可能性のある変数順序の置換がありすなわち、2、2つの変数の2つの可能性のある順序の置換を取得するのに1回のレイヤスワップを要する。BDD610に対して最適な変数順序を決定するため、初期的な第1変数順序を有するBDD610のサイズが決定及び記録される。2つのレイヤは、第2の可能性のある変数順序を取得するため交換される。第2変数順序を有するBDD610のサイズがまた決定及び記録される。その後、これら2つのサイズが比較され、より小さなサイズをもたらす変数順序が、BDD610の最適な変数順序として選択される。BDD620は、3つの変数すなわち、n=3に対応する3つのレイヤを有する。BDD620の3つの変数に対して6つの可能性のある変数順序の置換がありすなわち、3、3つの変数の6つの可能性のある変数順序の置換を取得するため、5回のレイヤスワップを要する。BDD620に対して最適な変数順序を決定するため、6つの異なる変数順序に対応するBDD620の6つのサイズが個別に決定及び記録される。その後、6つのサイズが比較され、最小サイズをもたらす変数順序が、BDD620の最適な変数順序として選択される。BDD630は、4つの変数すなわち、n=4に対応する4つのレイヤを有する。BDD630の4つの変数に対して24個の可能性のある変数順序の置換があるすなわち、4。BDD610,620に関して説明されるものと同様の処理が、BDD630に対して最適な変数順序を決定するために適用される。この場合、24個の異なる変数順序に対応するBDD630の24個のサイズがあり、最小サイズをもたらす変数順序が、BDD630の最適な変数順序として選択される。単純変更アルゴリズムは、n-1個の変数のレイヤスワップシーケンスからn個の変数のレイヤスワップシーケンスを構成することによって帰納的に実行される。n個の変数に対して、レイヤスワップ1,2,2,3,...,n-1,n及びn-1,n,n-2,n-1,...,1,2が、n-1個の変数のレイヤスワップのシーケンスからのレイヤスワップ間に交互に加えられる。従って、3つの変数のレイヤスワップシーケンスは、2つの変数のレイヤスワップシーケンスから構成される。レイヤ1とレイヤ2との間のBDD620のスワップ623は、BDD610のスワップ611に対応する。また、BDD620において、レイヤ1とレイヤ2との間のスワップすなわち、スワップ621と、レイヤ2とレイヤ3との間のスワップすなわち、スワップ622とがスワップ621の前に加えられ、レイヤ2とレイヤ3との間のスワップすなわち、スワップ624と、レイヤ1とレイヤ2との間のスワップすなわち、スワップ625とがスワップ621の後に加えられる。同様に、4つの変数のレイヤスワップシーケンスが、3つの変数のレイヤスワップシーケンスから構成される。BDD630のスワップ631,632,633,634,635はそれぞれ、BDD620のスワップ621,622,623,624,625に対応する。また、BDD630において、レイヤ1とレイヤ2との間のスワップ、レイヤ2とレイヤ3との間のスワップ、レイヤ3とレイヤ4との間のスワップ、レイヤ3とレイヤ4との間のスワップ、レイヤ2とレイヤ3との間のスワップ及びレイヤ1とレイヤ2との間のスワップが、スワップ631,632,633,634,635の間に交互に加えられる。図6に示されるように、実行されるレイヤスワップの大部分は、それらの直前のレイヤスワップに依存するため、単純変更アルゴリズムは効率的にパラレル化することができない。シフトアルゴリズムBDDの実質的に最適な変数順序を決定するヒューリスティックなアルゴリズムがある。ヒューリスティックアルゴリズムは、BDDのサイズがそれの最小値となるBDDの最適な変数順序を常に決定することができるとは限らないが、BDDのサイズが、所望の閾値以下など十分小さなBDDの実質的に最適な変数順序を決定することができる。広く利用されるヒューリスティックアルゴリズムは、シフトアルゴリズムShiftingAlgorithmである。それは、BDDの各変数に対して最適な位置を独立に求めることによって実行される。BDDの各変数は、当該変数が配置される初期的なレイヤにより近いエンドレイヤに移動シフトされる。その後、変数は、BDDの反対のエンドレイヤに移動される。変数が新たなレイヤに移動させる毎に、変数が現在配置されているレイヤのサイズ例えば、当該レイヤ上の決定ノードの個数に関するが決定及び記録される。従って、変数をBDDの1つのエンドレイヤから他のエンドレイヤに移動させることによって、これらのレイヤにおける変数による全てのレイヤのサイズが決定される。最小のサイズを有するレイヤが、当該変数に対する最適なレイヤすなわち、位置とみなされる。その後、変数は、当該変数に関してBDDのサイズがローカルに最小となる最適なレイヤに移される。図7は、8つの変数を有する関数を表現するBDD700の変数の1つである変数5に適用されるシフト処理を示す。BDD700は、8つのレイヤを有することになる。初期的には、変数5はレイヤ5にある。BDD700の2つのエンドレイヤは、BDD700が合計で8つのレイヤを有するため、レイヤ1とレイヤ8とになる。レイヤ8がレイヤ5により近い。従って、変数5は、それがレイヤ8上にくるまで、1回に1つのレイヤずつ下方にまず移動される。その後、変数5は、レイヤ1上にくるまで、再び1回に1つのレイヤずつ上方に移動される。変数5をあるレイヤから他の隣接するレイヤに移動させるため、これら2つのレイヤが交換されることに留意されたい。例えば、変数5をレイヤ5からレイヤ6に移動させるため、レイヤ5とレイヤ6とが交換される。変数5がレイヤ8にまず移動し、その後にレイヤ1に戻るのに10回のレイヤスワップを要する。これを実行することによって、変数5が配置された各レイヤのサイズが決定され、最小サイズを有するレイヤが変数5の最適なレイヤとして選択される。変数5の最適レイヤがレイヤ4であると仮定する。このとき、変数5はレイヤ1からレイヤ4まで移動され、さらに3回のレイヤスワップを要することになる。同一の処理が、各変数に適用され、当該変数の最適な位置が決定される。各変数は、初期的にそれに従属する決定ノードの個数に基づき選択されてもよい。例えば、アルゴリズムは、それに従属する決定ノードの個数が初期的に最大となる変数から開始され、上述した処理を用いてこの最初の変数に対してBDDにおける最適な位置すなわち、レイヤを決定し、最初の変数をそれの最適レイヤに移動させるようにしてもよい。その後、アルゴリズムは、初期的にそれに従属する決定ノードの個数が2番目に最大となる他の変数に対して上記処理を繰り返してもよい。以下同様にして、すべての変数が各自の最適レイヤに移動されるまで、又はBDDの合計サイズが所望又は所定の閾値より小さくなるまで、又は変数位置の調整がもはやBDDの合計サイズを有意に減少させなくなるまで例えば、2つの連続する変数位置の調整の間のBDDのサイズの差分が所定の閾値未満になるなど、続けられる。シフトアルゴリズムもまた、所与の変数のシフトに要する各レイヤスワップがその直前のものに依存するため、パラレル化することができない。[ウィンドウアルゴリズム]他のヒューリスティックアルゴリズムは、ウィンドウアルゴリズムWindowAlgorithmである。一般に、ウィンドウアルゴリズムは、BDDに対するグローバルに最適な変数順序を検出することはできないが、高速な実行時間という所望の性質を有する。n個の変数を有する関数を表現するBDDに対して、サイズkのウィンドウが使用されるただし、2≦k<n。アルゴリズムは、レイヤの最適な順序付け[1...k],[2...k1],[3...k2],...,[n-k1...n]を繰り返しかつ順次に検出する。すなわち、各ウィンドウに対して、ウィンドウ内のk個の連続するレイヤの最適な順序が決定され、ウィンドウ内のk個の連続するレイヤが各自の最適な順序に従ってリオーダされる。これは、図6に関して上述された単純変更アルゴリズムを用いて実行されてもよい。当該処理は、BDDの合計サイズが所望又は所定の閾値未満になるまで、又はウィンドウ内の変数のさらなる調整がBDDの合計サイズをもはや有意に減少させなくなるまで、又はさらなるサイズの改善が可能でなくなるまで、各ウィンドウに繰り返しかつ順次に適用される例えば、単純変更アルゴリズムを繰り返し用いて。図8は、8つの変数を有する関数を表現するBDD800に適用されるウィンドウアルゴリズムを示す。BDDは、8つのレイヤを有することになる。本例では、ウィンドウサイズkは3となるよう選択される。従って、まずレイヤ1からレイヤ3が、それらの最適な順序に従ってリオーダされる単純変更アルゴリズムなどを用いて。次に、レイヤ2からレイヤ4が、それらの最適な順序に従ってリオーダされる。以下同様に実行される。ウィンドウがレイヤ6からレイヤ8まで下方に移動すると、必要に応じて、ウィンドウは再びレイヤ1から再開されてもよい。ウィンドウアルゴリズムはサブセットとして単純変更アルゴリズムを利用するため、それは、典型的にはパラレル化できない。パラレル変数リオーダアルゴリズムBDDに対して最適な又は実質的に最適な変数順序を決定し、その最適な又は実質的に最適な変数順序に従ってBDDの変数をリオーダするいくつかの既存の変数リオーダアルゴリズムが存在するが、図6~8に示されるように、それらは何れも効率的にパラレル化することができない。他方、最適な又は実質的に最適な変数順序に従ってBDDの変数をリオーダすることは、特にBDDの変数の個数が十分多いときには、大変コストのかかるものとなる例えば、時間及びヒューマンリソース又はマシーンリソースなどに関して。例えば、単純変更アルゴリズムが示すように、n個の変数を有する関数を表現するBDDに対して、それの最適な変数順序を決定するには合計でn-1回のレイヤスワップを要する。実際のアプリケーションでは、BDDはしばしば数百又は数千のレイヤを有している。このため、本開示の各種実施例は、リオーダ処理を効率的にパラレル化することによって、既存のアルゴリズムに対して有意に改善する、BDDのための複数の変数リオーダアルゴリズムを提供する。各種実施例で説明されるパラレル変数リオーダアルゴリズムの設計の基礎には、2つの主要なコンセプトがある。n個のレイヤを有する所与のBDDに対して、2つの連続するレイヤ例えば、レイヤjとレイヤj1などの間でローカルスワップを実行することは、BDDのその他のレイヤすなわち、レイヤ1~レイヤj-1,レイヤj2~レイヤnを変更したり、又は影響を与えない。この性質は、再帰的に適用可能である。ある実施例では、互いに依存しない全てのレイヤスワップが、同時に実行されてもよい。例えば、8つのレイヤを有するBDD900を示す図9を検討する。8つのレイヤは、連続するレイヤの複数の互いに素であるペアにグループ化されてもよい。ある実施例では、あるタイプのグループ化に従って、レイヤ1とレイヤ2とがペアとされ、レイヤ3とレイヤ4とがペアとされ、レイヤ5とレイヤ6とがペアとされ、レイヤ7とレイヤ8とがペアとされてもよい。このタイプのグループ化によると、BDD900の8つのレイヤは、連続するレイヤの4つの互いに素であるペアにグループ化される。連続するレイヤの2つのペアは、それらが共通のレイヤを共有しない場合に互いに素であるdisjointとみなれる。例えば、レイヤ1とレイヤ2のペアと、レイヤ3とレイヤ4のペアとは、共通のレイヤを共有していない。レイヤ1とレイヤ2との交換は、レイヤ3~レイヤ8に影響を与えない。同様に、レイヤ3とレイヤ4との交換は、レイヤ1~レイヤ2とレイヤ5~レイヤ8とに影響を与えない。以下同様である。このため、連続するレイヤの4つの互いに素であるペアは、各ペア間に相互依存性がないため、同時に交換されてもよい。あるいは、他のタイプのグループ化によると、レイヤ2とレイヤ3とがペアとされ、レイヤ4とレイヤ5とがペアとされ、レイヤ6とレイヤ7とがペアとされてもよい。このタイプのグループ化によると、BDD900の8つのレイヤが、連続するレイヤの3つの互いに素であるペアにグループ化される。再び、レイヤ2とレイヤ3との交換は、レイヤ1とレイヤ4~レイヤ8に影響を与えない。レイヤ4とレイヤ5との交換は、レイヤ1~レイヤ3とレイヤ6~レイヤ8とに影響を与えない。以下同様である。このため、連続するレイヤの3つの互いに素なペアは、各ペアの間に相互依存性がないため、同時に交換されてもよい。一般化のため、n個の変数に対応するn個のレイヤを有する任意のBDDが与えられるとただし、nは3以上の任意の偶数又は奇数、n個のレイヤを連続するレイヤの互いに素なペアにグループ化するのに少なくとも2つの方法がある。例えば、n=4である場合、4つのレイヤは{1,2}及び{3,4}としてグループ化されてもよい。他方、n=5である場合、5つのレイヤをグループ化する1つの方法は、{1,2}及び{3,4}であり、他の方法は、{1,2}及び{4,5}であり、第3の方法は、{2,3}及び{4,5}である。第1タイプのグループ化によると、各ペアは、奇数レイヤjoddと偶数レイヤjevenとを含むただし、1≦jodd≦n-1に対して、jeven=jodd1。このようにグループ化された全てのペアは、奇数グループ化ペア又は第1グループ化ペアと呼ばれ、同時に交換されてもよい。第2タイプのグループ化によると、各ペアは、偶数レイヤjevenと奇数レイヤjoddとを含むただし、2≦jeven≦n-1に対して、jodd=jeven1。このようにグループ化された全てのペアは、偶数グループ化ペア又は第2グループ化ペアと呼ばれ、同様に同時に交換されてもよい。ある実施例では、第1タイプのグループ化に従って取得された全ての第1グループ化ペアと、第2タイプのグループ化に従って取得された全ての第2グループ化ペアとが、繰り返しかつ交互に交換されてもよい。例えば、図9において、第1の繰り返し中t=1、全ての奇数グループ化ペアすなわち、第1グループ化ペアがパラレルにすなわち、同時に交換される。第2の繰り返し中t=2、全ての偶数グループ化ペアすなわち、第2グループ化ペアがパラレルに交換される。第3の繰り返し中t=3、全ての奇数グループ化ペアが再びパラレルに交換される。当該処理が、所望の結果が取得されるまで、全ての奇数グループ化ペアと全ての偶数グループ化ペアとの交換が交互に続けられる。一般化のため、ある実施例では、上記処理は、奇数の各繰り返し繰り返し1,3,5,...など中に全ての奇数グループ化ペアを同時に交換し、偶数の各繰り返し繰り返し2,4,6,...など中に全ての偶数グループ化ペアを同時に交換する。あるいは、他の実施例では、上記処理は、奇数の各繰り返し中に全ての偶数グループ化ペアを同時に交換し、偶数の各繰り返し中に全ての奇数グループ化ペアを同時に交換してもよい。第2のコンセプトは、置換の非明示的列挙implicitenumerationofpermutationsと呼ばれてもよい。6つのレイヤを有するBDD1000を示す図10を検討する。これら6つのレイヤは、レイヤ1とレイヤ2、レイヤ3とレイヤ4及びレイヤ5とレイヤ6の連続するレイヤの3つの互いに素なペアにグループ化されると仮定する。これらの連続するレイヤの互いに素なペアは、順次又は同時に交換されてもよい。3回のレイヤスワップの前に、BDD1000の変数順序が{1,2,3,4,5,6}である場合すなわち、変数1がレイヤ1にあり、変数2がレイヤ2にあり、変数3がレイヤ3にあるなど、3回のレイヤスワップ後には、BDD1000の変数順序は{2,1,4,3,6,5}になるすなわち、変数2がレイヤ1にあり、変数1がレイヤ2にあり、変数4がレイヤ3にあり、変数3がレイヤ4にあり、変数6がレイヤ5にあり、変数5がレイヤ6にある。ある実施例では、以下の観察ができる。すなわち、各レイヤスワップの実行はBDD1000の残りの構成とサイズとに影響を与えないため、これらのスワップの何れか一部を実行することにより取得される置換のサイズは、BDD全体に対して対応する完全な変数順序を明示的に生成することなく計算できる。例えば、BDD1000によると、3回のレイヤスワップ前に、変数1がレイヤ1にあり、変数2がレイヤ2にあり、変数3がレイヤ3にあり、変数4がレイヤ4にあり、変数5がレイヤ5にあり、変数6がレイヤ6にある6つのレイヤのサイズが個別に決定される。3回のスワップの後、変数2はレイヤ1にあり、変数1がレイヤ2にあり、変数4がレイヤ3にあり、変数3がレイヤ4にあり、変数6がレイヤ5にあり、変数5がレイヤ6にある6つのレイヤのサイズが再び決定される。従って、連続するレイヤの互いに素な各ペアに対して、2つのレイヤが交換される前のサイズと、2つのレイヤが交換された後のサイズとの2つのサイズが存在する。BDD1000の6つのレイヤに対して、連続するレイヤの3つの互いに素なペアが存在する。より詳細には、レイヤ1とレイヤ2に対して、レイヤ1とレイヤ2とが交換される前に、変数1及び2を有するレイヤ1及び2のサイズが決定されてもよい。レイヤ1とレイヤ2とが交換された後、変数2及び1を有するレイヤ1及び2のサイズが決定されてもよい。同様に、レイヤ3とレイヤ4に対して、レイヤ3とレイヤ4とが交換される前に、変数3及び4を有するレイヤ3及び4のサイズが決定されてもよい。レイヤ3とレイヤ4とが交換された後、変数4及び3を有するレイヤ3及び4のサイズが決定されてもよい。また、レイヤ5とレイヤ6に対して、レイヤ5とレイヤ6とが交換される前に、変数5及び6を有するレイヤ5及び6のサイズが決定されてもよい。レイヤ5とレイヤ6とが交換された後、変数6及び5を有するレイヤ5及び6のサイズが決定されてもよい。連続するレイヤの3つの互いに素なペアのサイズの異なる組み合わせは、対応する変数順序を明示的に生成することなく、BDD1000の異なる変数順序のサイズをもたらす。例えば、変数順序{1,2,4,3,5,6}すなわち、変数1がレイヤ1にあり、変数2がレイヤ2にあり、変数4がレイヤ3にあり、変数3がレイヤ4にあり、変数5がレイヤ5にあり、変数6がレイヤ6にあるのサイズを非明示的に決定するため、ある実施例は、1変数1及び2をそれぞれ有するレイヤ1及び2のサイズレイヤ1とレイヤ2とを交換する前に取得された、2変数4及び3をそれぞれ有するレイヤ3及び4のサイズレイヤ3とレイヤ4とを交換した後に取得された、及び3変数5及び6をそれぞれ有するレイヤ5及び6のサイズレイヤ5とレイヤ6とを交換する前に取得されたの和を計算してもよい。3つのレイヤスワップの前後の何れにおいて3つ全てのサイズが決定される。他の例として、変数順序{2,1,3,4,6,5}のサイズを非明示的に決定するため、ある実施例は、1変数2及び1をそれぞれ有するレイヤ1及び2のサイズレイヤ1とレイヤ2とを交換した後に取得される、2変数3及び4をそれぞれ有するレイヤ3及び4のサイズレイヤ3とレイヤ4とを交換した後に取得される、及び3変数6及び5をそれぞれ有するレイヤ5及び6のサイズレイヤ5とレイヤ6とを交換した後に取得されるの和を計算してもよい。BDD100のケースでは、レイヤスワップの前後に取得された連続するレイヤの3つの互いに素なペアのサイズを合成することによって、7つのさらなる変数順序のサイズが、連続するレイヤの3つの互いに素なペアに関する3つのレイヤスワップにより計算されてもよい。BDD1000は初期的には変数順序{1,2,3,4,5,6}を有するため、この変数順序のサイズは既知であり、計算される必要がないことに留意されたい。図10は、3つのスワップの前後に取得される連続するレイヤの3つの互いに素なペアの異なるサイズを合成することによってサイズが決定されるBDD1000の8つ全ての異なる変数順序を示す。6つの変数すなわち、連続するレイヤの3つの互いに素なペアに対して、8つの組み合わせが存在するここで、変数順序の1つ{1,2,3,4,5,6}がレイヤスワップ前の初期的な順序である。一般化するため、n個の変数に対応するn個のレイヤを有する任意のBDDが与えられると、k個のレイヤスワップがパラレルに実行される場合すなわち、連続するレイヤのk個の互いに素なペアが存在する、2k-1個の変数順序のサイズが非明示的に計算可能である。ここで、レイヤスワップ前のBDDの初期的な変数順序のサイズは非明示的な計算を要することなく直接的に取得できるため、-1が存在することに留意されたい。しかしながら、一般には、連続するレイヤのk個の互いに素なペアが与えられると、2k個の異なる変数順序のサイズは、連続するレイヤのk個の互いに素なペアを交換することによって決定されてもよい。各種実施例において説明されるBDDのパラレル変数リオーダアルゴリズムは、パラレル化の最大化と置換の非明示的列挙とのコンセプトに依拠する。BDDのための既存の変数リオーダアルゴリズムは、実行されるスワップの大部分が相互依存しているため、パラレル化できない。従って、ある実施例は、交換が不要な連続するレイヤのペアの間の相互依存が最小限になるように例えば、連続するレイヤの互いに素なペアを形成するなどによって、レイヤスワップ処理を構成しようとし、これにより、連続するレイヤの複数のペアをパラレルに交換する可能性を増加させることができる。[パラレル置換アルゴリズム]ある実施例では、スワップネットワークの深さが最小となるスワップのスケジュールが所望される。n個の変数に対応するn個のレイヤを有する所与のBDDが初期的に第1の変数順序を有すると仮定すると、異なる第2の変数順序に従ってBDDのn個の変数をリオーダすることが所望される。第2の変数順序は、何れか適切な手段によって取得されてもよい例えば、ある人により指定されたり、設計仕様要求やアプリケーション基準に従って決定されるなど。ある実施例では、所与の置換すなわち、変数順序を現在の変数置換に適用することが、変数の識別子に課されるトータルの順序が所望される最終的な置換によって定義される場合、ソーティングの問題と等価になる。ある実施例では、BDDの第1の変数順序すなわち、BDDが現在有する変数順序が恒等置換である、すなわち、各変数i1≦i≦nがレイヤiにあると仮定する。所望される第2の変数順序は、πiとして規定され、すなわち、各変数i1≦i≦nがレイヤπiにある。BDDが最終的に第2の変数順序を有するように、BDDのn個の変数をリオーダすることが目標である。図11Aは、第1の変数順序を初期的に有するBDDのn個の変数を第2の変数順序に従ってリオーダするパラレル置換アルゴリズムの一例を示す。図11Bは、6つの変数に対応する6つのレイヤを有するBDD1100に適用されるパラレル置換アルゴリズムを示す。図11Aに示されるステップは、一例としてBDD1100を用いて説明される。図9に関して上述されたように、n個の変数に対応するn個のレイヤを有する任意のBDDが与えられると、n個のレイヤを連続するレイヤの互いに素なペアにグループ化するための2つの方法がある。第1には、n個のレイヤが、各ペアが奇数レイヤに続いて偶数レイヤを含む奇数グループ化ペア第1グループ化ペアとも呼ばれるにグループ化されてもよい。第2に、n個のレイヤが、各ペアが偶数レイヤに続いて奇数レイヤを含む偶数グループ化ペア第2グループ化ペアとも呼ばれるにグループ化されてもよい。全ての奇数グループ化ペアは、それらが互いに素であるためすなわち、共通のレイヤを共有しない、同時に交換されてもよい。同様に、全ての偶数グループ化ペアは、それらが互いに素であるため、同時に交換されてもよい。パラレル置換アルゴリズムは、この性質を利用する。ある実施例では、BDDのn個のレイヤは、奇数グループ化ペアと偶数グループ化ペアに繰り返しかつ交互にグループ化され、現在の繰り返し中の2つのレイヤの現在の順序が第2の変数順序により指定される順序と異なる場合、各レイヤペアは交換される。より詳細には、一例として図11Bの6つの変数に対応する6つのレイヤを有するBDD1100を利用する。BDD1100は、初期的には恒等置換{1,2,3,4,5,6}すなわち、各変数i1≦i≦6がレイヤiにあるである第1の変数順序を有する。所望される第2の変数順序は{6,3,4,5,1,2}すなわち、変数6がレイヤ1にあり、変数3がレイヤ2にあり、変数4がレイヤ3にあると仮定する。これは、π6<π3<π4<π5<π1<π2を意味する。ある実施例では、第1の繰り返し中すなわち、t=1、BDD1100の6つのレイヤは、図11Aのステップ1101に示されるように、レイヤ1とレイヤ2、レイヤ3とレイヤ4及びレイヤ5とレイヤ6の3つの奇数グループ化ペアにグループ化される。これらは、ペア間で共通のレイヤを共有していないため、連続するレイヤの互いに素なペアである。従って、3つの奇数グループ化ペアは、図11Aのステップ1102に示されるように、同時に交換されてもよい。レイヤ1とレイヤ2に対して、変数1は現在レイヤ1にあり、変数2は現在レイヤ2にある。従って、レイヤ1及び2にある2つの変数の現在の順序は{1,2}であり、変数1及び2について第2の変数順序によって指定される順序とすでに一致しているすなわち、変数2の前に変数1があり、π1<π2を意味する。従って、この繰り返し中にはレイヤ1とレイヤ2とを交換する必要はない。同様に、レイヤ3とレイヤ4に対して、変数3は現在レイヤ3にあり、変数4は現在レイヤ4にある。従って、レイヤ3及び4にある2つの変数の現在の順序は{3,4}であり、変数3及び4について第2の変数順序により指定された順序にすでに一致しているすなわち、π3<π4。従って、この繰り返し中にレイヤ3とレイヤ4とを交換する必要はない。他方、レイヤ5とレイヤ6に対して、変数5は現在レイヤ5にあり、変数6は現在レイヤ6にある。レイヤ5及び6における2つの変数の現在の順序は{5,6}であり、変数5及び6について第2の変数順序により指定される順序と異なっているすなわち、π5>π6。従って、レイヤ5とレイヤ6とはこの繰り返し中に交換され、その後、変数6はレイヤ5にあり、変数5はレイヤ6にある。第1の繰り返し中に1つのみのレイヤスワップしか必要でなかったため、パラレル化の必要はない。しかしながら、複数のレイヤスワップが繰り返し中に必要とされる場合、それらはパラレルに実行されてもよい。レイヤのグループ化は、結果として得られる連続するレイヤのペアが互いに素であることを保障するためである。各繰り返し後、当該処理は、図11Aのステップ1103に示されるように、第2の変数順序が実現されたか決定する。実現された場合、当該処理は成功し終了される。そうでない場合、当該処理は次の繰り返しに続く。BDD1100に対して、第1の繰り返し後、変数順序は{1,2,3,4,6,5}になる。従って、所望される第2の変数順序は実現されず、もう1回繰り返しが必要とされる。ある実施例では、第2の繰り返し中すなわち、t=2、BDD1100の6つのレイヤが、図11Aのステップ1104に示されるように、レイヤ2とレイヤ3、及びレイヤ4とレイヤ5の2つの偶数グループ化ペアにグループ化される。再び、これらは、ペア間で共通のレイヤを共有していないため、連続するレイヤの互いに素なペアである。従って、2つの偶数グループ化ペアは、図11Aのステップ1105に示されるように、同時に交換されてもよい。レイヤ2とレイヤ3について、変数2が現在レイヤ2にあり、変数3が現在レイヤ3にある。レイヤ2及び3の2つの変数の現在の順序は、{2,3}であり、変数2及び3について第2の変数順序により指定されている順序すなわち、π2>π3と異なっている。このため、レイヤ2とレイヤ3とは当該繰り返し中に交換され、その後に、変数3はレイヤ2にあり、変数2はレイヤ3にある。同様に、レイヤ4とレイヤ5について、変数4が現在レイヤ4にあり、変数6が現在レイヤ5にある。レイヤ4及び5の2つの変数の現在の順序は、{4,6}であり、変数4及び6について第2の変数順序により指定された順序すなわち、π4>π6と異なっている。このため、レイヤ4とレイヤ5とは当該繰り返し中に交換され、その後に、変数6はレイヤ4にあり、変数4はレイヤ5にある。2つのレイヤスワップが当該繰り返し中に必要とされるため、ある実施例では、それらはパラレルに実行されてもよい。再び各繰り返し後、当該処理は、図11Aのステップ1106に示されるように、第2の変数順序が実現されたか判断する。実現された場合、当該処理は成功し終了する。そうでない場合、当該処理は次の繰り返しを続ける。BDD1100に対して、第2の繰り返し後、変数順序は{1,3,2,6,4,5}になる。従って、所望される第2の変数順序は実現されず、もう1回繰り返しが必要とされる。第3及び第5の繰り返し中に実行されるステップは、第1の繰り返しのものと同様であり、第4及び第6の繰り返し中に実行されるステップは、第2の繰り返しのものと同様である。図11Bに示されるように、BDD1100に対して、第2の変数順序が実現されるまで6つの変数をリオーダするのに合計で6回の繰り返しを要する。奇数の各繰り返し中すなわち、繰り返し1,3,5、BDD1100の6つのレイヤは、互いに素である連続するレイヤの奇数グループ化ペアにグループ化される。偶数の各繰り返し中すなわち、繰り返し2,4,6、6つのレイヤは、互いに素である連続するレイヤの偶数グループ化ペアにグループ化される。第3の繰り返し中すなわち、t=3、レイヤ1とレイヤ2、及びレイヤ3とレイヤ4が同時に交換される。第4の繰り返し中すなわち、t=4、レイヤ2とレイヤ3、及びレイヤ4とレイヤ5は同時に交換される。第5の繰り返し中すなわち、t=5、レイヤ1とレイヤ2、レイヤ3とレイヤ4、及びレイヤ5とレイヤ6が同時に交換される。第6の繰り返し中すなわち、t=6、レイヤ4とレイヤ5とが交換される。しかしながら、BDD1100は、パラレル置換アルゴリズムの一例である。あるいは、奇数の各繰り返し中に、6つのレイヤが互いに素である連続するレイヤの偶数グループ化ペアにグループ化され、偶数の各繰り返し中に、6つのレイヤが互いに素である連続するレイヤの奇数グループ化ペアにグループ化されてもよい。レイヤのグループ化が連続する繰り返しにおいて交互に実行される限り、アルゴリズムはそれの目標を実現することができる。各繰り返し中に、レイヤのペアは、レイヤに現在ある変数の順序が所望される第2の変数順序により指定される対応する変数の順序と異なっているか、又は一致しているかに依存して、交換されてもよい。一般化のため、n個の変数に対応するn個のレイヤを有するBDDが与えられ、BDDは初期的には、各変数i1≦i≦nがレイヤiにある第1の変数順序を有し、各変数i1≦i≦nがレイヤπiにある、πiとして規定されるBDDの第2の変数順序が与えられると、第2の変数順序に従ってBDDのn個の変数をリオーダするため、ある実施例では、パラレル置換アルゴリズムは繰り返し処理を実行する。奇数の各繰り返し中、n個のレイヤは、第1のグループ化スキームに従って第1のタイプの連続するレイヤの互いに素なペアにグループ化される。偶数の各繰り返し中、n個のレイヤは、第2のグループ化スキームに従って第2のタイプの連続するレイヤの互いに素なペアにグループ化される。各繰り返し中、2つのレイヤに現在ある2つの変数の順序が第2の変数順序により指定される2つの変数の順序と異なっている場合に限って、連続するレイヤのペアが交換される。すなわち、2つの連続するレイヤj1,j2について、ある繰り返し中に、変数i1が現在レイヤj1にあり、変数i2が現在レイヤj2にあると仮定する。このとき、πi1>πi2である場合に限って、レイヤj1とレイヤj2とが当該繰り返し中に交換される。ある実施例では、各繰り返し中に実行される全てのレイヤスワップは、パラレルにすなわち、同時に実行される。ある実施例では、n個の変数に対応するn個のレイヤを有する任意のBDDに対して、BDDが初期的には第1の変数順序を有するとき、パラレル置換アルゴリズムを利用して、第2の変数順序を実現するためにBDDのn個の変数をリオーダするため、高々n回のレイヤスワップの繰り返し各繰り返しはまた、レベルと呼ばれてもよいを要する。さらに、n回の繰り返し中に、高々すなわち、nn-1/2に等しいn個から2つを選ぶ回のレイヤスワップを要する。パラレル置換アルゴリズムは、n回未満の繰り返しにおいて何れかの置換を実現可能な他のレイヤ交換スケジュールがないとき、パラレルに最適である。比較において、既存の変数リオーダアルゴリズムはまた、高々回のレイヤスワップを必要とするが、回の繰り返しを必要とするかもしれない。図11Aに関して上述されたパラレル置換アルゴリズムは、BDDと特にROBDDとの異なるパーティション又は分割の間の置換を変換するのに利用されてもよい。実際のアプリケーションでは、BDD又は通常はROBDDはしばしば、数千又は数百万のノードを有する。従って、このような大規模なBDD又はROBDDを格納することは、大きな記憶スペースを必要とする。この問題を解決するため、大規模なBDD又はROBDDはしばしば2以上のサブBDDに分割され、各サブBDDが実質的にBDDとなる。オリジナルのBDDは、サブBDDの論理ORをとることによって取得されてもよい。記憶スペースの必要をさらに減少させるため、各サブBDDの変数は、当該サブBDDの最適な又は実質的に最適な変数順序に従ってリオーダされてもよい。そのようにして、サブBDDが格納される。しかしながら、各サブBDDは実質的にBDD自体であるため、あるサブBDDの最適な又は実質的に最適な変数順序は、他のサブBDDの最適な又は実質的に最適な変数順序と異なる可能性がある。BDDに関して処理が実行される必要があるとき、サブBDDは、オリジナルのBDDを構成するため合成されてもよい。あるいは、個々のサブBDDに関してこれらの処理が実行されてもよい。何れのケースでも、これらの処理を実行するとき、関係する全てのサブBDDは同じ変数順序を有する必要がある。それぞれが異なる変数順序を有する合計でm個m≧2のサブBDDが存在する場合、m-1個のサブBDDの変数がリオーダされる必要がある。ある実施例では、各BDDがn個の変数に対応するn個のレイヤを有する第1BDDと第2BDDとの2つのBDDがあると仮定する。第1BDDは、現在第1の変数順序を有する。第2BDDは、第1BDDの第1の変数順序と異なる第2の変数順序を現在有する。さらに、第1BDDと第2BDDとが第3BDDの2つのパーティションすなわち、2つのサブBDDであると仮定するすなわち、第1BDDと第2BDDとが一緒になって第3BDDを構成する。必要に応じて、第1BDDのn個の変数が、図11Aに関して上述されたパラレル置換アルゴリズムを用いて、第2BDDの第2の変数順序に従ってリオーダされてもよい。あるいは、第2BDDのn個の変数が、パラレル置換アルゴリズムを用いて第1BDDの第1の変数順序に従ってリオーダされてもよい。何れのケースでも、変数のリオーダ後、第1BDDと第2BDDは共に同じ変数順序を有する。その後、それらは第3BDDを構成するため合成されるか、又は第1BDDと第2BDDに関して個別に処理が実行されてもよい。当該処理は、BDDが3以上のサブBDDに分割される場合も同様に適用されてもよい。1つのサブBDDが、所望される変数順序を有するサブBDDとして選択される。その他のサブBDDのそれぞれの変数が、パラレル置換アルゴリズムを用いて選択されたサブBDDの変数順序に従ってリオーダされる。[4つの変数を有するBDDの最適なレイヤ交換スケジュール]図9に示されるように、n個の変数に対応するn個のレイヤを有する任意のBDDが与えられると、高々n/2回のレイヤスワップが各繰り返し中にパラレルに実行可能であるため、実現可能な最大パラレル化はn/2である。従って、各繰り返し中にすなわち、各レベルにおいてn/2回のレイヤスワップを配置することが所望される。これは置換アルゴリズムのケースに対して可能であるが、同時に、当該処理がイグザクト又はヒューリスティックアルゴリズムのセマティックを尊重する必要があるときは、常に可能であるとは限らない。イグザクトリオーダのケースでは、ある実施例では、最適な変数順序を決定するために可能性のある全ての変数の置換を実行するために、n-1回のレイヤスワップを実行するのにn-1回未満の繰り返しを必要とする交換スケジュールを決定することが望ましい例えば、単純変更アルゴリズムのケースなど。ある実施例は、上述された非明示的置換のコンセプトに基づき交換スケジュールを決定してもよい。ある実施例は、4個の変数に対応する4つのレイヤを有するBDDを検討し、当該BDDの最適なレイヤ交換スケジュールを決定する。ここで、2又は3個の変数に対応する2又は3つのレイヤを有するBDDについては、図6などに示されるように、2つのスワップがパラレルには実行できない。図12A~12Bは、4つの変数に対応する4つのレイヤを有するBDD1200の一例となる最適なレイヤ交換スケジュールを示す。13回の繰り返し中に合計で19回のレイヤスワップが実行される。同じ繰り返しに属する全てのレイヤスワップはパラレルに実行可能であることに留意されたい。従って、第1の繰り返し中すなわち、第1レベルにおいて、レイヤ1とレイヤ2及びレイヤ3とレイヤ4が同時に交換される。第2の繰り返し中、レイヤ2とレイヤ3とが交換される。第3の繰り返し中、レイヤ1とレイヤ2及びレイヤ3とレイヤ4が同時に交換される。以下同様に実行される。例えば、BDD1200の初期的な変数順序は{1,2,3,4}であると仮定する。各繰り返しの前後の変数順序は、図12BのBDD1200により示される。レイヤスワップの13回の繰り返しの経過後、BDD1200の最終的な変数順序は{2,3,4,1}である。13回の繰り返し中、4つの変数が4つのレイヤ間で移動される。4つの変数に対して、合計で24すなわち、4個の可能な変数順序がある。最適な変数順序を決定するため、24個の可能な変数順序のサイズが決定される必要があり、これにより、最小サイズを有する変数順序が選択される。しかしながら、非明示的列挙のコンセプトに基づき、24個の可能な変数順序の24個のサイズを決定するため、24個の可能な変数順序が明示的に生成される必要はない。一例としてBDD1200を用いて、BDD1200の初期的な変数順序は{1,2,3,4}であると仮定する。変数1及び2をそれぞれ有するレイヤ1及び2のサイズs1,21,2が決定され、変数3及び4をそれぞれ有するレイヤ3及び4のサイズs3,43,4が決定されてもよい。第1の繰り返し中すなわち、t=1、レイヤ1とレイヤ2及びレイヤ3とレイヤ4がパラレルに交換される。第1の繰り返し後、BDD1200の変数順序は{2,1,4,3}となる。変数2及び1をそれぞれ有するレイヤ1及び2のサイズs2,11,2が決定され、変数4及び3をそれぞれ有するレイヤ3及び4のサイズs4,33,4が決定されてもよい。第1の繰り返し後、4つの変数順序のサイズが計算される。すなわち、1変数順序{1,2,3,4}のサイズは、s1,21,2とs3,43,4の和であり{1,2,3,4}はBDD1200の初期的な変数順序であるため、当該変数順序のサイズは、実際にはレイヤスワップを要することなく知られているBDD1200の初期的なサイズであることに留意されたい、2変数順序{2,1,3,4}のサイズは、s2,11,2とs3,43,4の和であり、3変数順序{1,2,4,3}のサイズは、s1,21,2とs4,33,4の和であり、4変数順序{2,1,4,3}のサイズは、s2,11,2とs4,33,4の和である。しかしながら、実際には、第1の繰り返しに関して取得された4つの変数順序の4つのサイズ全てを明示的に計算する必要はないかもしれない。ある実施例は、レイヤ1とレイヤ2についてサイズs1,21,2とs2,11,2との小さい方を選択し、レイヤ3とレイヤ4についてサイズs3,43,4とs4,33,4との小さい方を選択し、第1の繰り返しに関して取得された4つの変数順序の最小のサイズをもたらす変数順序を決定し、以降の繰り返し中の比較のためにそれまでの最小サイズをもたらす変数順序を記録するようにしてもよい。第2の繰り返し中すなわち、t=2、レイヤ2とレイヤ3とが交換される。第2の繰り返し後、変数順序は{2,4,1,3}となる。第2の繰り返しの目的は、第1の繰り返しに関して説明された処理と同様に、レイヤ1とレイヤ2及びレイヤ3とレイヤ4が同時に交換され、より多くの変数順序のサイズが非明示的置換のコンセプトに基づき計算される他の繰り返しについて4つの変数を配置することである。第3の繰り返し前、変数2及び4をそれぞれ有するレイヤ1及び2のサイズs2,41,2が決定され、変数1及び3をそれぞれ有するレイヤ3及び4のサイズs1,33,4が決定されてもよい。第3の繰り返し中すなわち、t=3、レイヤ1とレイヤ2及びレイヤ3とレイヤ4がパラレルに交換される。第3の繰り返し後、BDD1200の変数順序は{4,2,3,1}である。変数4及び2をそれぞれ有するレイヤ1及び2のサイズs4,21,2が決定され、変数3及び1をそれぞれ有するレイヤ3及び4のサイズs3,13,4が決定されてもよい。第3の繰り返し後、他の4つの変数順序のサイズが計算される。すなわち、1変数順序{2,4,1,3}のサイズはs2,41,2とs1,33,4との和であり、2変数順序{2,4,3,1}のサイズはs2,41,2とs3,13,4との和であり、3変数順序{4,2,1,3}のサイズはs4,21,2とs1,33,4との和であり、4変数順序{4,2,3,1}のサイズはs4,21,2とs3,13,4との和である。再び実際には、第3の繰り返しに関して取得された4つの変数順序の4つのサイズの全てを明示的に計算する必要はないかもしれない。ある実施例は、レイヤ1とレイヤ2についてサイズs2,41,2とs4,21,2との小さい方を選択し、レイヤ3とレイヤ4についてサイズs1,33,4とs3,13,4との小さい方を選択し、第3の繰り返しに関して取得されたこれら4つの変数順序に対して最小のサイズをもたらす変数順序を決定する。第3の繰り返しに関して取得された4つの変数順序の最小のサイズが、第1の繰り返しに関して取得された4つの変数順序の最小のサイズと比較される。ここまでに最小のサイズをもたらす第1又は第3の繰り返しからの変数順序が、以降の繰り返し中の比較のために記録されてもよい。第4の繰り返し中すなわち、t=4、レイヤ2とレイヤ3とが交換される。第5の繰り返し中すなわち、t=5、レイヤ1とレイヤ2とが交換される。第5の繰り返し後、変数順序は{4,3,2,1}である。第4及び第5の繰り返しの目的は、第1及び第3の繰り返しに関して説明された処理と同様に、レイヤ1とレイヤ2及びレイヤ3とレイヤ4が同時に交換され、より多くの変数順序のサイズが非明示的置換のコンセプトに基づき計算される他の繰り返しのために4つの変数を配置することである。BDD1200を検討すると、レイヤ1とレイヤ2及びレイヤ3とレイヤ4が同時に交換されるさらなる4つの繰り返しがあるすなわち、第6、第9、第11及び第13の繰り返し。これらの繰り返しのそれぞれにおいて、第1及び第3の繰り返しと同様に、4つの一意的な変数順序のサイズが非明示的列挙のコンセプトに基づき計算されてもよい。BDD1200を検討すると、レイヤ1とレイヤ2及びレイヤ3とレイヤ4が同時に交換される合計で6つの繰り返しすなわち、第1、第3、第6、第9、第11及び第13の繰り返しが存在する。これら6つの繰り返しのそれぞれは、非明示的列挙のコンセプトに基づき4つの変数順序のサイズを提供する。従って、これら6つの繰り返しは、列挙又は置換繰り返しenumerationorpermutationiterationと呼ばれてもよい。これら6つの列挙繰り返しの間にあるその他の繰り返しはすなわち、第2、第4、第5、第7、第8、第10及び第12の繰り返し、以降の列挙繰り返しのため変数を再配置する。ある実施例では、各列挙繰り返しの後、列挙繰り返しに関して取得された4つの変数順序のうち最小のサイズをもたらす変数順序が選択され、それのサイズすなわち、列挙繰り返しに関して取得された4つの変数順序のサイズの最小のものが、以前の繰り返し中に取得及び記録された変数順序の最小サイズと比較され、より小さなサイズをもたらす変数順序が、これまでの最小サイズをもたらした変数順序として記録される。従って、第13の繰り返しの終了時には、第13の繰り返しに関して取得された4つの変数順序の最小のサイズと、以前の繰り返し中に決定及び記録された最小サイズとの比較結果として選択された変数順序が、24個の可能な全ての変数順序のうちで最小のサイズをもたらすため、BDD1200の最適な変数順序となる。図12A~12Bに示される最適なレイヤ交換スケジュールと、4つの変数に対応する4つのレイヤを有するBDDに適用される単純変更アルゴリズムなどとを比較する。4つの変数に対して可能な全ての変数の置換を取得するため、単純変更アルゴリズムは、パラレル化なしでは23回の繰り返しに、又はフルにパラレル化すると18回の繰り返しに含まれる23回のレイヤスワップを必要とする一方、図12A~12Bに示されるレイヤ交換スケジュールは、19回のレイヤスワップによる13回の繰り返ししか必要としない。明らかに、図12A~12Bに示されるレイヤ交換スケジュールは、より少ない繰り返し及びレイヤスワップ回数しか必要とせず、これにより完了までの時間が短縮されるため、単純変更アルゴリズムより改良されている。図12A~12Bは、4つの変数を有するBDDに対して最適な変数順序を決定するため、13回の繰り返し中に19回のレイヤスワップが実行されることを要求する最適なレイヤ交換スケジュールの一例を示す。各自が13回の繰り返し中に実行される19回のレイヤスワップを用いて、4つの変数を有するBDDに対して最適な変数順序を決定する約60個の異なる最適なレイヤ交換スケジュールがある。図12A~12Bに示されるレイヤ交換スケジュールと同様に、最適なレイヤ交換スケジュールのそれぞれは、レイヤ1とレイヤ2及びレイヤ3とレイヤ4がパラレルに交換される6つの列挙繰り返しを含む。6つの列挙繰り返しのそれぞれについて、4つの変数順序のサイズが非明示的列挙のコンセプトに基づき計算されてもよい。列挙繰り返しの間にある繰り返しは、変数を再配置する。図12Cは、最適なレイヤ交換スケジュールの他の例を示す。再び、最適なレイヤ交換スケジュールのそれぞれは、非明示的列挙のコンセプトに基づき、4つの変数を有するBDDの最適な変数順序を決定するのに利用されてもよく、当該処理は、図12A~12Bに関して説明されたものと同様である。[BDD変数のペア単位グループ化]n=2kすなわち、nは偶数であると仮定する。n個の数の集合{1,...,n}を2つの要素からなるk個の順序付けされた集合のn/2k個のグループに分ける又は分離する方法は、n/2k個存在するすなわち、各集合には2つの要素が存在し、各グループにはk個の集合が存在する。各グループは、n個の変数のセパレーションと呼ばれてもよい。例えば、n=4のケースに対してすなわち、k=2、{1,2,3,4}を2つの要素からなる2つの順序付けされた集合の6つの一意的なグループに分離する方法は6通り存在する。以下において、4つの変数を2つの要素からなる2つの順序付けされた集合の6つの一意的なグループに分離される4つの変数が示される。グループ1:{1,2}{3,4}グループ2:{1,3}{2,4}グループ3:{1,4}{2,3}グループ4:{2,3}{1,4}グループ5:{2,4}{1,3}グループ6:{3,4}{1,2}2つの要素からなるk個の集合の各グループ内において、各要素は1回しか出現しないことに留意されたい。例えば、上記6つのタイプのセパレーションの各セパレーション内では、第1の集合にある数が出現した場合、それは第2の集合には出現しない。その逆に、第2の集合にある数が出現した場合、それは第1の集合には出現しない。ある実施例では、このコンセプトをBDDの変数に適用すると、要素は変数に等価である。2つの変数の各集合はBDDの変数の2つを含み、各グループはk個の順序付けされた集合を含む。2つの変数の各集合内では、2つの変数の順序は無関係である例えば、{1,2}は{2,1}と同じとみなされる。しかしながら、2つの変数のk個の順序付けされた集合のそれぞれについては、順序は重要である。従って、[{1,2}{3,4}]は、[{3,4}{1,2}]と同じでないとみなされる。従って、セパレーション自体を順序づける方法は、n/2k通り存在する。各グループは2つの変数のk個の順序付けされた集合から構成され、2つの変数は変数のペアと呼ばれるため、BDD変数を分離する当該方法は、BDD変数のペア単位グループ化と呼ばれてもよい。6つの変数を有するBDDのケースではすなわち、n=6,k=3、6つの変数を2つの変数からなる3つの順序付けされた集合に分離する方法は90通り存在するすなわち、90個の一意的なグループ。以下において、6つの変数のペア単位セパレーションのいくつかのグループの具体例が示される。グループ1:{1,2}{3,4}{5,6}グループ2:{1,3}{2,4}{5,6}グループ3:{2,4}{1,3}{5,6}グループ4:{2,5}{1,6}{3,4}グループ5:{3,4}{1,5}{2,6}グループ6:{3,6}{1,2}{4,5}グループ7:{4,5}{2,3}{1,6}グループ8:{4,6}{1,5}{2,3}グループ9:{5,6}{1,2}{3,4}ある実施例では、2つの変数からなるk個の順序付けされた集合の各グループがBDDのある変数順序とみなされると仮定する。例えば、4つの変数のケースでは、グループ1は変数順序{1,2,3,4}を提供するすなわち、変数1,2,3,4はそれぞれレイヤ1,2,3,4にある。グループ2は変数順序{1,3,2,4}を提供するすなわち、変数1,3,2,4はそれぞれレイヤ1,2,3,4にある。グループ3は変数順序{1,4,2,3}を提供するすなわち、変数1,4,2,3はそれぞれレイヤ1,2,3,4にある。以下同様である。6つの変数のケースでは、グループ1は変数順序{1,2,3,4,5,6}を提供するすなわち、変数1,2,3,4,5,6はそれぞれレイヤ1,2,3,4,5,6にあるグループ3は変数順序{2,4,1,3,5,6}を提供するすなわち、変数2,4,1,3,5,6はそれぞれレイヤ1,2,3,4,5,6にある。グループ5は変数順序{3,4,1,5,2,6}を提供するすなわち、変数3,4,1,5,2,6はそれぞれレイヤ1,2,3,4,5,6にある。以下同様である。一例として4つの変数のケースを用いて、BDDが4つのレイヤを有する。レイヤ1とレイヤ2及びレイヤ3とレイヤ4が、連続するレイヤの2つの互いに素なペアを構成する。従って、図9に関して上述されたように、レイヤ1とレイヤ2及びレイヤ3とレイヤ4は同時に交換されてもよい。変数順序{1,2,3,4}を提供する、4つの変数のケースのグループ1[{1,2}{3,4}]を検討する。レイヤ1とレイヤ2及びレイヤ3とレイヤ4が交換された場合、レイヤスワップ後、変数順序は{2,1,4,3}になる。図10に関して上述されたように、非明示的列挙のコンセプトを利用して、レイヤ1とレイヤ2のサイズがレイヤ1とレイヤ2の交換の前後に決定され、レイヤ3とレイヤ4のサイズがレイヤ3とレイヤ4の交換の前後に決定される場合、4つの変数すなわち、{1,2,3,4},{2,1,3,4},{1,2,4,3}及び{2,1,4,3}のサイズが、レイヤ1とレイヤ2のサイズとレイヤ3とレイヤ4のサイズとを組み合わせることによって計算されてもよい。同一の処理が、その他の5つのグループのそれぞれに適用されてもよい。例えば、4つの変数のケースのグループ2[{1,3}{2,4}]について、レイヤスワップ後、グループ2により提供される変数順序は{1,3,2,4}になる。レイヤスワップ後、変数順序は{3,1,4,2}になる。再び、レイヤ1とレイヤ2のサイズがレイヤ1とレイヤ2の交換前後に決定され、レイヤ3とレイヤ4のサイズがレイヤ3とレイヤ4の交換前後に決定される場合、4つの変数順序すなわち、{1,3,2,4},{3,1,2,4},{1,3,4,2}及び{3,1,4,2}のサイズが計算されてもよい。従って、一意的な各グループは、レイヤ1とレイヤ2及びレイヤ3とレイヤ4を交換することによって、4つの異なる変数順序のサイズを提供する。6つの一意的なグループによって、4つの変数を有するBDDの24個の全ての変数順序のサイズが計算される。最小のサイズを有する変数順序が、BDDの最適な変数順序となる。BDDが6つのレイヤを有する6つの変数のケースを検討する。レイヤ1とレイヤ2、レイヤ3とレイヤ4及びレイヤ5とレイヤ6が、連続するレイヤの3つの互いに素なペアを構成する。従って、レイヤ1とレイヤ2、レイヤ3とレイヤ4及びレイヤ5とレイヤ6が同時に交換されてもよい。各グループは、異なる変数順序を提供する。例えば、6つの変数のケースのグループ7は、変数順序{4,5,2,3,1,6}を提供する。レイヤ1とレイヤ2のサイズがレイヤ1とレイヤ2の交換前後に決定され、レイヤ3とレイヤ4のサイズがレイヤ3とレイヤ4の交換前後に決定され、レイヤ5とレイヤ6のサイズがレイヤ5とレイヤ6の交換前後に決定される場合、BDDの8つの変数順序のサイズは、レイヤ1とレイヤ2のサイズ、レイヤ3とレイヤ4のサイズ及びレイヤ5とレイヤ6のサイズを非明示的列挙コンセプトに基づき合成することによって計算されてもよい。実際、90個の一意的なグループのそれぞれは、レイヤ1とレイヤ2、レイヤ3とレイヤ4及びレイヤ5とレイヤ6を交換することによって、8つの異なる変数順序のサイズを提供し、これにより、6つの変数を有するBDDの270個の全ての可能な変数順序のサイズを提供することができる。再び、最小のサイズを有する変数順序が、BDDの最適な変数順序となる。当該処理は、n個の変数に対応するn個のレイヤを有するBDDに同様に適用されてもよいただし、nは3以上の任意の奇数又は偶数である。nが奇数であるとき、2つの変数の代わりに1つのみの変数を有する各グループの集合が存在することになる。例えば、n=5すなわち、奇数である場合、5つの変数のペア単位セパレーションのいくつかのグループは、以下のようになる。グループ1:{1,2}{3,4}{5}グループ2:{1,3}{4,5}{2}グループ3:{2,4}{1,5}{3}グループ4:{1,5}{3,4}{2}各グループの変数の集合は順序付けされているためすなわち、各グループの集合の順序は、変数リオーダアルゴリズムに関連する、ある実施例では、nが奇数であり、1つのみの変数を有する1つの集合が各グループに存在するとき、各グループにおいてその他の2つの変数の集合に対するこの1つの変数の集合の相対的な位置は関連し、全てのグループにおいて同一であるべきである。例えば、1つの変数の集合は、全てのグループにおいて最後の集合となってもよいし、又は、全てのグループにおいて1番目の集合となってもよいし、全ての集合において2番目の集合などとなってもよい。すなわち、各グループにおいて、1つの変数の集合がその他の2つの変数の集合に関して実際に配置される位置1番目、2番目、3番目又は最後などは無関係であるが、1つの変数の集合は全てのグループにおいてその他の2つの変数の集合に関して同じ位置に配置される必要がある。一般化のため、ある実施例では、n個の変数が、個の一意的なグループに分離されてもよく、各グループは、個の順序付けされた集合から構成される。nが偶数であるとき、各グループの全ての集合はそれぞれ2つの変数を有している。nが奇数であるとき、各グループの1つの集合を除く全ての集合はそれぞれ2つの変数を有し、各グループの1つの集合は1つの変数を有する。各グループは、BDDの個の異なる変数順序のサイズを、非明示的列挙コンセプトに基づきすなわち、連続するレイヤの個の互いに素なペアを同時に交換し、連続するレイヤの互いに素なペアのサイズを決定し、これらのサイズを合成することによって提供してもよい。最後の全ての可能な変数順序において最小のサイズを有する変数順序が、BDDの最適な変数順序となる。ある実施例では、2つの変数又は1つの変数の個の順序付けされた集合の個の一意的なグループが構成されると、当該グループにより提供される個の異なる変数順序において最小のサイズをもたらす変数順序が決定される。この変数順序は、当該グループ内のローカルに最適な変数順序である。その後、個のグループからの個のローカルに最適な変数順序が、BDDの最小のサイズをもたらす変数順序を選択するため比較される。これが、BDDの最適な変数順序となる。図13Aは、BDD変数のペア単位のグループの一例を示す。ある実施例では、2つの変数又は1つの変数の個の順序付けされた集合の個の一意的なグループが構成されると、各グループに対して、当該グループ内のローカルに最適な変数順序を可能な限り効率的に決定することが望ましい。4つの変数を有するBDDのケースでは、4つの変数を分離することから得られる6つのグループが以下のようになると仮定する。グループ1:{1,2}{3,4}グループ2:{2,4}{1,3}グループ3:{3,4}{2,1}グループ4:{4,1}{2,3}グループ5:{1,3}{4,2}グループ6:{3,2}{1,4}2つの変数の各集合内では2つの変数の順序は関係がないため、[{4,1}{2,3}]及び[{1,4}{2,3}]は、2つの一意的なグループでなく同一のグループとみなされる。再び、2つの変数の2つの集合はそれぞれ、異なる変数順序を提供する。図12A~12Bに関して上述された最適なレイヤ交換スケジュールが、6つのグループから取得された異なる変数順序のサイズを効率的に決定するため利用されてもよい。4つの変数が上記の6つのグループに分離される場合、図12A~12Bに示される例や交換スケジュールは、非明示的列挙コンセプトに基づき24個の可能な変数順序のサイズを決定するのに利用されてもよい。図13Bにおいて、4つの変数のレイヤ交換スケジュールは、図12Bに示されたものと同じである。しかしながら、これら6つのグループに対応する変数順序のみがマークされる。図13Bが示唆するように、上述されるような2つの変数の6つの一意的なグループ又は2つの順序付けされた集合は、レイヤ1とレイヤ2及びレイヤ3とレイヤ4の双方が交換される6回の繰り返し前の6つの変数順序に対応する。2つの変数又は1つの変数の個の順序付けされた集合の個のグループすなわち、セパレーションに分離されるn個の変数のより一般的なケースでは、ある実施例において、一意的な各グループは、全てのレイヤスワップ1,2,3,4,...,n-1,nが実行されるイグザクトレイヤ交換スケジュールの繰り返しに対応する。これらの繰り返しの間において、ある実施例は、2つのグループに対応する2つの変数順序を結合するため、パラレル置換アルゴリズムを利用する。例えば、パラレル置換アルゴリズムに関して、2つのグループの1番目のグループから導出される変数順序は初期的な変数順序とみなされ、2つのグループの2番目のグループから導出される変数順序は、終了時の変数順序とみなされてもよい。ある実施例は、レイヤスワップの高々n回の繰り返しが、2つのグループ間で実行される必要がある。図13Bは、上記の分離順序について、6つの分離段階とパラレル置換段階とを示す。各分離段階は、2つの変数のn/2個の順序付けされた集合のグループに対応する。6つの分離段階はS1~S6と記される。これら分離段階の間の5つのパラレル置換段階はP1~P5と記される。各分離段階は、1回のレイヤスワップの繰り返しに対応する。しかしながら、リンクする各パラレル置換段階は、4つの変数のケースでは1~4回のレイヤスワップの繰り返しを含む。従って、最適化の目的は、パラレル置換段階により求められる繰り返しの回数を最小化する分離段階を検出することであり、これはパラレルに最適なレイヤ交換スケジュールに対応する。上述されるように、図12A~12Bに示されるレイヤ交換スケジュールは、4つの変数を有するBDDについて最適なスケジュールである。従って、ある実施例では、このスケジュールは、パラレル置換段階により求められる繰り返しの回数を最小化する分離順序を決定するため、4つの変数を有するBDDに適用されてもよい。ある実施例では、この最適化は、nの具体的な各値に対してオフラインに1回実行される。ある実施例は、網羅的アプローチを利用して、最適な分離順序を検出してもよい。にもかかわらず、網羅的アプローチが適用可能でないか実際的でないくらい大きい場合、ある実施例は、何れかの分離順序から開始し、その後にそれのローカルに最適な位置が検出されるまで、各分離を左右に独立に移すようにしてもよい。各パラレル置換段階は、高々n回の繰り返しを必要とする。従って、各分離順序は、高々回の繰り返しすなわち、回の繰り返しに及ぶレイヤ交換スケジュールに対応する。単純変更アルゴリズムはn-1回の繰り返し、又はパラレルなケースでは少なくともn-n-1回の繰り返しを必要とするため、図13Aに示される処理は、指数的により少ないレイヤスワップの繰り返ししか必要とせず、従って指数的により少ないレイヤスワップしか必要としない。実際には、最適な分離順序は、具体例から観察されるようなよりも有意に少ない繰り返ししか必要としない。[BDD変数の再帰的分離]ある実施例では、n個の変数を有する任意のBDDが与えられるとnは、3以上の任意の奇数又は偶数、n個の変数は、各グループが、個の順序付けされた集合から構成される個の一意的なグループに分離されてもよい。再び、nが偶数であるとき、各グループの全ての集合はそれぞれn個の変数のうちの2つを有する。nが奇数であるとき、各グループの1つの集合を除く全ての集合がそれぞれn個の変数のうちの2つを有し、各グループの1つの集合がn個の変数のうちの1つを有する。再び、各集合内の変数順序は無関係であり、各グループ内の集合の順序が関係する。ある実施例では、nが2の冪乗であるより具体的なケースではすなわち、nは2により繰り返し除すことができる、n個の変数は、再帰的アルゴリズムを用いて2つの変数のn/2個の順序付けされた集合の個のグループに分離されてもよい。より詳細には、n個の変数の集合が与えられると、1回目の繰り返し中に、ある実施例は、当該集合を各集合がn/2個の変数を有する2つの順序付けされた変数の集合の一意的なグループに分離してもよい。2回目の繰り返し中に、ある実施例はさらに、各グループ内の個々の集合を2以上の順序付けされた変数の集合に分離し、これにより、各集合がn/4個の変数を有する4つの順序付けされた変数の集合のさらなるグループが構成されてもよい。以下同様である。各繰り返し中、既存のグループかから個々の集合を分離することによって構成される新たなグループが、前の繰り返しから取得された既存のグループと置き換えられる。この再帰的処理は、各グループ内の各集合が2つの変数のn/2個の順序付けされた集合を有するまで続けられるようにしてもよい。4つの変数を有するBDDの最適な変数順序が、例えば、図12A~12Cに示される最適なレイヤ交換スケジュールなどを用いて効率的に決定されるため、再帰的処理は実際的には、各グループ内の各集合が4つの変数を有するまで続けられるようにしてもよい。その後に、図12A~12Cに関して上述された処理が、4つの変数の各集合についてローカルに最適な変数順序を決定するため利用されてもよい。図14Aは、n個の変数を分離するのに用いられる再帰的処理の一例を示す。図14Bは、8つの変数に適用される再帰的処理を示す。一例としてn=8を使用する。1回目の繰り返し中、8つの変数は、各グループが2つの順序付けされた集合から構成され、各集合が4つの変数から構成される複数の一意的なグループに分離されてもよい。例えば、1回目の繰り返し後、これらのグループのいくつかは以下のようになるかもしれない。グループ1:{1,2,3,4}{5,6,7,8}グループ2:{1,2,3,5}{4,6,7,8}グループ3:{1,2,3,6}{4,5,7,8}など本開示において全てをリストするための2以上のグループが存在する。2回目の繰り返し中、各グループ内には、4つの変数の各集合が再び、各グループが2つの順序付けされた集合から構成され、各集合が2つの変数から構成される複数の一意的なグループに分離される。例えば、2回目の繰り返し後、集合{1,2,3,4}は、2つの変数の2つの集合の6つのグループを構成する。同様に、集合{5,6,7,8}は、2つの変数の2つの集合の他の6つのグループを構成する。集合{1,2,3,5}は、2つの変数の2つの集合のさらなる他の6つのグループを構成する。以下同様である。2回目の繰り返し後、各グループ内の各集合は2つの変数を有する。従って、再帰は終了される。nが8より大きな数である場合、より多くの繰り返しが必要とされる。最後の繰り返し後、図14Bにおいて、各行に沿った変数の集合が、2つの変数の4つの順序付けされた集合の一意的なグループを構成し、各グループは、8つの変数のBDDの一意的な変数順序を提供する。BDDの最適な変数順序は、図13Aに関して説明されたものと同様の処理を利用して決定されてもよい。より詳細には、ある実施例は、非明示的列挙コンセプトを用いて各グループ内のローカルに最適な変数順序を決定し、その後に全てのグループに対応する全てのローカルに最適な変数のうち最小のサイズをもたらすローカルに最適な変数順序を選択することによって、BDDの最適な変数順序を決定するようにしてもよい。すなわち、ある実施例では、n個の変数の集合が与えられるとnは、2より大きな任意の奇数又は偶数、既存の集合は、一方の集合がn個の変数のうちの個を有し、他方の集合がn個の変数のうちの個を有する2つの新たな変数集合に分離される。n個の変数のそれぞれは、新たな2つの集合の双方でなく、何れか一方に属する。nが偶数であるとき、新たな2つの集合は同数の変数を有する。nが奇数であるとき、新たな2つの集合は1つの変数だけ異なる。既存の変数集合を新たな2つの変数集合に分離する上記方法は、図14Aに示される再帰的処理の各繰り返し中に、各グループの各変数集合に同様に適用される。一般に、n個の変数を各集合がを有する2つの順序付けされた集合に分離するため、各グループが個の変数の2つの順序付けされた集合から構成される個の一意的なグループが存在するすなわち、n個の変数を分離するのに、個の異なる方法が存在する。この再帰は、n個の変数が各グループが2つ又は1つの変数の個の順序付けされた集合を含む複数の一意的なグループすなわち、セパレーションに分離されるまで続けられる。すなわち、各部分集合が2つ又は1つの変数を有するまで、個の変数の各部分集合に対して、当該アルゴリズムが再帰的に実行される。各グループ内では、各変数は集合の1つにおいて1回しか出現しない。上述されるように、4つの変数を有するBDDの最適な変数順序は、例えば、図12A~12Zに示されるアルゴリズムの何れかを用いて決定されてもよい。ある実施例では、n個の変数を分離するための再帰は、各グループの各集合が4以下の変数を有するようになるまで続けられる。その後、各グループの各集合のローカルに最適な変数順序が、例えば、図12A~12Zに示されるアルゴリズムの何れかを用いて決定されてもよい。各グループについて、それのローカルに最適な変数順序は、当該グループの各集合のローカルに最適な変数順序を用いて決定される。その後、BDDに対して、それの最適な変数順序が、各グループのローカルに最適な変数順序を用いて決定される。n=5のケースについてすなわち、5つの変数、上述されたn個の変数を分離する方法に基づき、ある実施例では、5つの変数が、各グループ内において1つの集合が2つの変数を有し、1つの集合が3つの変数を有する2つの順序付けされた集合のグループに分離される。その後、5つの変数の最適な変数順序が、当該グループを用いて決定される。しかしながら、ある実施例では、5つの変数を各グループ内において1つの集合が4つの変数を有し、1つの集合が1つの変数を有する2つの順序付けされた集合のグループに分離することがより効率的であることが、実験により示唆されている。各グループの4つの変数の各集合のローカルに最適な変数順序が、例えば、図12A~12Zに示されるアルゴリズムの何れかを用いて決定されてもよい。各グループについて、それのローカルに最適な変数順序が、当該グループの4つの変数の集合のローカルに最適な変数順序を用いて決定される。5つの変数のケースの最適な変数順序が、各グループのローカルに最適な変数順序を用いて決定される。ある実施例では、n個の変数を分離するための再帰が、各グループの各集合が5以下の変数を有するようになるまで続けられる。その後、各グループの4つの変数の各集合のローカルに最適な変数順序が、例えば、図12A~12Zに示されるアルゴリズムの何れかを用いて決定されてもよい。各グループの5つの変数の各集合のローカルに最適な変数順序が、5つの変数のケースについて上述された方法を用いて決定されてもよい。各グループについて、それのローカルに最適な変数順序は、当該グループの各集合のローカルに最適な変数順序を用いて決定される。その後、BDDについて、それの最適な変数順序が、各グループのローカルに最適な変数順序を用いて決定される。ある実施例では、このコンセプトはさらに以下のように一般化されてもよい。n個の変数を分離するための再帰は、各グループの各集合がk個以下1≦k<nの変数を有するようになるまで続けられてもよい。ある実施例では、kは所定のものであってもよい例えば、kは2,3,4又は5など。各グループの各集合のローカルに最適な変数順序は、何れか適切なアルゴリズムを用いて決定されてもよい。各グループのローカルに最適な変数順序は、当該グループの各集合のローカルに最適な変数順序を用いて決定される。そして、BDDの最適な変数が、各グループのローカルに最適な変数順序を用いて決定される。ある実施例では、分離段階は、4つの変数のケースについて図13A~13Bに関して上述されたようなものと同様の方法により、順序付けされ、パラレル置換段階とリンクされる。必要とされる繰り返しは、再帰により取得され、これは既存のイグザクトアルゴリズムの要求される繰り返しより改善されていることが示される。n個の変数を分離するための当該再帰的アルゴリズムと図13A~13Bに関して上述された非再帰的アルゴリズムとを比較すると、再帰的アルゴリズムはn個の変数を有するBDDの最適な変数順序を決定するのに高々4n回のレイヤスワップの繰り返ししか必要としない一方、非再帰的アルゴリズムはn個の変数を有するBDDの最適な変数順序を決定するのに高々回のレイヤスワップの繰り返しを必要とする。4より大きなnに対して、再帰的アルゴリズムがより効率的なものとなる。[パラレルウィンドウアルゴリズム]図8に関して説明されたウィンドウアルゴリズムでは、n個の変数を有する関数を表現するBDDに対して、サイズk2≦k<nのウィンドウが選択される。当該アルゴリズムは、レイヤ[1...k],[2...k1],[3...k2]...[n-k1...n]の最適な順序を繰り返し順次検出する。既存のウィンドウアルゴリズムは、単純変更アルゴリズムを利用して、各ウィンドウ内の変数をそれのローカルな最適順序に従ってリオーダする。ある実施例では、既存のウィンドウアルゴリズムは、パラレル化により改善される。ある実施例は、kk=4などのウィンドウサイズを選択する。このとき、ウィンドウはk個の連続するレイヤから構成される。その後、各ウィンドウ内において、k個の連続するレイヤにおけるk個の変数のローカルに最適な変数順序が決定され、k個の変数が、何れか適切なBDD変数リオーダアルゴリズムを利用して、それのローカルに最適な変数順序又はローカルに実質的に最適な変数順序に従ってリオーダされる。さらに、k個の連続するレイヤの複数の互いに素なウィンドウがパラレルに処理されてもよい。2つのウィンドウは、それらが共通のレイヤを共有しない場合に互いに素である。ある実施例では、n個の変数に対応するn個のレイヤを有するBDDについて、サイズkk=4などのウィンドウによって、各繰り返し中に、n個のレイヤが高々個の互いに素なウィンドウにグループ化される例えば、k=4である場合、ウィンドウ1はレイヤ1~4を含み、ウィンドウ2はレイヤ5~8を含み、ウィンドウ3はレイヤ9~12を含むなどである。個の互いに素なウィンドウが、適切なBDD変数リオーダアルゴリズムを用いてパラレルにリオーダされてもよい例えば、単純変更アルゴリズムや変数の集合の最適な変数順序を決定する上述されたアルゴリズムの何れかなど。例えば、k=4である場合、各ウィンドウのローカルに最適な変数順序を決定するため、4つの変数を有するBDDに対する変数リオーダアルゴリズムに基づく最適レイヤ交換スケジュールが利用されてもよい。異なる繰り返しの間に、n個のレイヤが異なってグループ化されてもよい。ある実施例では、例えば、nが4により割り切れる場合、1回目の繰り返し中に、ウィンドウはレイヤ{1...4},レイヤ{5...8},...,レイヤ{n-3...n}となる。2回目の繰り返し中、ウィンドウはレイヤ{2...5},レイヤ{6...9},...,レイヤ{n-6...n-3}となる。3回目の繰り返し中、ウィンドウはレイヤ{3...6},レイヤ{7...10},...,レイヤ{n-5...n-2}となる。4回目の繰り返し中、ウィンドウはレイヤ{4...7},レイヤ{8...1},...,レイヤ{n-4...n-1}となる。5~8回目の繰り返しのウィンドウは、1~4回目の繰り返しのウィンドウと同じになり、以下同様である。当該処理は、収束するまで続けられる例えば、BDDの合計サイズが所望又は所定の閾値以下になるまで、又は変数位置のさらなる調整がBDDの合計サイズをもはや有意に減少させなくなるまで。図15Aは、パラレルウィンドウリオーダアルゴリズムの一例を示す。図15Bは、12個の変数に対応する12個のレイヤを有する一例となるBDD1500に適用されるサイズ4の一例となるウィンドウを利用したパラレルウィンドウリオーダアルゴリズムを示す。図15Aの各ステップは、一例としてBDD1500を用いて説明される。1回目の繰り返し中すなわち、t=1、図15Aのステップ1502に示されるように、12個のレイヤが4つの連続するレイヤの3つの互いに素な集合に分離される。従って、ウィンドウは、レイヤ{1...4}、レイヤ{5...8}及びレイヤ{9...12}となる。これら3つのウィンドウは、それぞれが4つの変数を有するBDDに対する最適リオーダアルゴリズム又は他の何れか適切な変数リオーダアルゴリズムを用いて、図15Aのステップ1504に示されるように、パラレルにリオーダされる。全てのウィンドウがリオーダされた後、BDD1500の現在のサイズが決定される。BDD1500の現在のサイズが所望の閾値未満である場合、当該処理は、図15Aのステップ1506に示されるように終了される。そうでない場合、もう1回繰り返しが実行される。例えば、2回目の繰り返し中すなわち、t=2、12個のレイヤが4つの連続するレイヤの2つの互いに素な集合に分離される。従って、ウィンドウは、レイヤ{2...5}及びレイヤ{6...9}となる。これら2つのウィンドウは、同様にしてパラレルにリオーダされてもよい。3回目の繰り返し中すなわち、t=3、ウィンドウは、レイヤ{3...6}及びレイヤ{7...10}となり、これら2つのウィンドウは、同様にしてパラレルにリオーダされてもよい。4回目の繰り返し中すなわち、t=4、ウィンドウは、レイヤ{4...7}及びレイヤ{8...11}となり、これら2つのウィンドウは、同様にしてパラレルにリオーダされてもよい。5回目の繰り返し中、1回目の繰り返しと同様に、グループ化が戻ってレイヤ1から再び開始される。所望の変数順序が取得されるまで例えば、BDDのサイズが十分小さくなるなど、以下同様に実行される。ある実施例では、各繰り返し中、BDDのn個のレイヤがk個の連続するレイヤの複数の互いに素な集合に分離される。しかしながら、各繰り返し中に構成されるk個の連続するレイヤの互いに素な集合は、現在の繰り返しの直前の繰り返し中に構成されたk個の連続するレイヤの互いに素な集合とは異なる。この結果、n個のレイヤは、図15Bに示されるように、各繰り返し中に異なって分離及びグループ化される。実際のアプリケーションでは、サイズ4以下のウィンドウが最も一般的に利用される。しかしながら、図15Bに示される上記処理は、任意のサイズサイズkなどのウィンドウに適用するよう拡張されてもよい。一般的なケースでは、kのウィンドウサイズによると、ある実施例は、a1×kb≦nとなるaと、となるbとに対する繰り返しで交互にレイヤ[a×k1b,a1×kb]に対して対応するイグザクトリオーダアルゴリズムを適用してもよい。[最大パラレル化を利用したウィンドウアルゴリズム]図15Bに関して上述されるように、複数のウィンドウ内の変数をパラレルにリオーダすることに加えて、各ウィンドウ内において、k個の連続するレイヤにおけるk個の変数のリオーダは、図9に関して上述されるような最大パラレル化コンセプトを利用してもよい。図16は、ウィンドウサイズ6を使用して、1つのウィンドウ内のk個の連続するレイヤにおける変数をリオーダする具体例を示す。ある実施例では、奇数の各繰り返し中、k個のレイヤが連続するレイヤの互いの素な奇数グループ化ペアにグループ化され、偶数の各繰り返し中、k個のレイヤが連続するレイヤの互いに素な偶数グループ化ペアにグループ化され、又はその反対のグループ化がされる。各繰り返し中、連続するレイヤの互いに素な全てのペアが同時に交換される。このアルゴリズムは、ウィンドウアルゴリズムの構成を維持する。所与のkに対して、当該アルゴリズムは、逆の置換によりそれのk個の入力を移すのに必要な全てのレイヤスワップを実行する。ここで、パラレル置換アルゴリズムと構造的に類似している。しかしながら、このケースでは、全てのレイヤスワップは各繰り返し中に無条件に実行される。さらに、各繰り返し中に、非明示的に検出された全ての置換のサイズが計算される。最小のサイズの置換が維持記録などされる。k個のレイヤに対する全てのレイヤスワップの終了後、パラレル置換アルゴリズムは、最小のサイズの置換にk個のレイヤを戻すのに利用されてもよい。再び、ある実施例は、BDDが所望のサイズに達するまで、レイヤが異なる繰り返し中に異なってグループ化される処理を繰り返す。[パラレルシフトアルゴリズム]図7に関して上述されたシフトアルゴリズムの主な短所は、それが本来的に順次的なものであることである。BDDの変数は、それらが配置されるレイヤのサイズに従って順序付けされる。シフトアルゴリズムのこの短所を軽減するため、ある実施例は、1回に1つの変数をシフトさせるのでなく、k個の変数を同時にシフト移動させる。しかしながら、k個の変数のそれぞれは、図7に示されるものと同様の方法によりシフトされてもよい。ある実施例では、n個の変数に対応するn個のレイヤを有するBDDが与えられると、n個の変数は、繰り返し処理を利用してそれらの最適なレイヤに移動される。各繰り返し中、現在の繰り返し中に最大のサイズを現在有しているk個のレイヤのk個の変数が、それらのローカルに最適なレイヤすなわち、位置にシフトされる。k個の変数の各集合について、シフトがk個の変数に対して同時に実行される。例えば、k個の最大となるレイヤのk個の変数がまず同時にシフトされ、その後に2番目に大きなk個のレイヤのk個の変数が同時にシフトされ、以下同様に実行される。同時のレイヤスワップの各繰り返し後、非明示的に生成された全ての置換のサイズが計算される。集合の全ての変数に対してシフトが実行されると、パラレル置換アルゴリズムは、ローカルに最小となるものに順序を戻すのに利用される。当該アルゴリズムは、全ての変数の集合について継続され、収束するまで繰り返される。図17Aは、パラレルシフトアルゴリズムの一例を示す。ある実施例では、1回目の繰り返し中、図17Aのステップ1702に示されるように、BDDのn個のレイヤにおいて最大のサイズを同時に有するk個のレイヤが選択される。選択されたk個のレイヤに現在は位置されているk個の変数は、当該繰り返し中に同時にシフトされる。k個の変数は、図17Bのステップ1704に示されるように、各自のローカルに最適なレイヤにパラレルに移動される。これを実行するため、k個の変数のそれぞれは、図7に関して上述された処理を利用して、自らのローカルに最適なレイヤにシフトされてもよい。例えば、各変数は、当該変数を有するn個のレイヤにおいて最小のサイズを現在もたらすレイヤを決定するため、n個のレイヤを移動される。当該レイヤは、現在の繰り返し中に変数のローカルに最適なレイヤである。しかしながら、ある実施例は、k個の変数をパラレルにシフトする。k個全ての変数がそれらのローカルに最適なレイヤに配置された後、BDDの現在のサイズが決定される。BDDの現在のサイズが所望の閾値未満である場合、当該処理は、図17Aのステップ1706に示されるように終了される。そうでない場合、ステップ1702と1704とを実行することから構成されるもう1回の繰り返しが繰り返される。図17Bは、3つの変数がパラレルにシフトされる一例となるBDD1700に適用されるパラレルシフトアルゴリズムを示す。9個の変数があり、変数2,5,8が最大サイズを現在有する3つのレイヤの3つの変数である。変数2,5,8は、繰り返し処理において同時のレイヤ交換を利用して、それらのローカルに最適な位置に移動される。各繰り返し中、連続するレイヤのペアの交換が互いに影響を与えない限り、変数2,5,8がパラレルにシフトされてもよい。より詳細には、変数2は、それがレイヤ1に到達するまで上方に移動し、BDD1700の最後のレイヤであるレイヤ9に到達するまで下方に移動される。変数5は、それがレイヤ1に到達するまでまず上方に移動され、その後にレイヤ9に到達するまで下方に移動される。変数8は、それがレイヤ9に到達するまで下方に移動され、その後にレイヤ1に到達するまで上方に移動される。変数のいくつかは全てのレイヤを移動するのにより多くの繰り返しを必要とし、繰り返しの一部において、1つの変数をシフトすることが他の変数をシフトすることに影響を与える可能性があるが例えば、6回目の繰り返し中、変数2は、変数8のシフトが変数2のシフトに干渉しないため、シフトすることができない、繰り返しの大部分において、これら3つの変数は、効果的にパラレル化されるすなわち、連続するレイヤの3つの互いに素なペアを同時に交換することによって同時にシフトされる。各変数が9つのレイヤ間を移動するため、当該変数が各レイヤにあるとき、当該レイヤのサイズが決定される。従って、変数2について、変数2が9つのレイヤにそれぞれあるときに決定される9つのサイズがある。9つのサイズのうちで最小のサイズを有するレイヤが、変数2のローカルに最適なレイヤである。同様に、変数5について、変数5が9つのレイヤにそれぞれあるときに決定された9つのサイズがある。第2の9つのサイズのうちで最小サイズを有するレイヤが、変数5のローカルに最適なレイヤとなる。従って、所与の変数について、変数が各レイヤにあるときに全てのレイヤ間で最小のサイズをもたらすレイヤが、現在の繰り返し中の当該レイヤのローカルに最適なレイヤとなる。BDDのサイズが十分小さくない場合、最大のサイズを現在有している3つのレイヤに配置された他の3つの変数が選択される。これら3つの変数は、変数2,5,8に関して上述されたものと同じ処理を用いて、それらのローカルに最適な位置に移動される。BDDは、多くの実用的なアプリケーションを有し、本開示に開示された各種アルゴリズムは、何れかのアプリケーションのBDDにより利用されてもよい。例えば、集積回路IC設計の分野では、ICはBDDにより表現される関数を実現するのに利用されてもよい。IC設計が従属する必要がある性質は、BDDにより表現されてもよく、当該回路の設計をフォーマルベリフィケーションすることに関連して利用される。ヘルスケアの分野では、BDDは、医療センサにより収集されるデータを表すのに利用される。フォーマルベリフィケーションの分野では、BDDは、遷移関係又は到達可能な状態空間をそれら各自の性質と共にモデル化するのに利用されてもよい。ハードウェア及びソフトウェアシステムに関して、フォーマルベリフィケーションformalverificationは、形式的な数学方法を利用して、ある形式的仕様や性質に関してシステムの基礎となる意図されたアルゴリズムの正しさを証明又は反証するための処理である。これらのハードウェア及びソフトウェアシステムのベリフィケーションは、システムの抽象的な数学モデルに対するフォーマルプルーフを提供することによって実行され、数学モデルとシステムの性質との間の対応関係が構成により知られる。システムをモデル化するためしばしば利用される数学オブジェクトの具体例は、有限状態マシーン、ラベル付けされた遷移システム、Petriネット、時間付きオートマトン、バイブリッドオートマトン、プロセス代数、操作的セマティック、表示的セマティック、公理的セマティック、Hoareロジックなどのプログラミング言語のフォーマルセマティックである。BDD、又はより詳細にはBDDを構成するデータは、コンピュータ可読な非一時的記憶媒体に格納されてもよい。BDDの変数が本開示において開示されたアルゴリズムの何れかを用いてリオーダされるとき、当該データは、コンピュータ可読な非一時的記憶媒体により実現されるように変換される。ある実施例では、任意の整数の集合はブール関数として表現され、ブール関数はBDDにより表現されてもよい。整数の集合が与えられると、ある実施例は、集合の最大の整数を表現するのに必要とされる最小数のビットを決定する。このビット数は、ブール関数の変数の個数である。その後、集合の各整数について、ブール関数はTRUEと評価され、集合にない任意の整数については、ブール関数はFALSEと評価される。例えば、整数の集合{1,3,5,6}を検討する。集合の最大の整数は6であり、3ビットを要する。従って、この整数の集合を表現するのに使用されるブール関数は、3つの変数x1,x2及びx3を必要する。以下のテーブルは、{1,3,5,6}を表現するのに利用されるときの3つの変数の値とブール関数の値とを示す。ある実施例は、1以上のコンピュータシステム上で実現されてもよい。図18は、一例となるコンピュータシステム1800を示す。ある実施例では、1以上のコンピュータシステム1800が、ここに開示又は図示される1以上の方法の1以上のステップを実行する。ある実施例では、1以上のコンピュータシステム1800は、ここに開示又は図示される機能を提供する。ある実施例では、1以上のコンピュータシステム1800上で実行されるソフトウェアは、ここに開示又は図示される1以上の方法の1以上のステップを実行し、又はここに開示又は図示される機能を提供する。ある実施例は、1以上のコンピュータシステム1800の1以上の部分を含む。本開示は、何れか適切な個数のコンピュータシステム1800を想定する。本開示は、何れか適切な物理形態をとるコンピュータシステム1800を想定する。例えば、限定することなく、コンピュータシステム1800は、埋め込みコンピュータシステム、システムオンチップSOC、シングルボードコンピュータシステムSBC例えば、コンピュータオンモジュールCOMやシステムオンモジュールSOMなど、デスクトップコンピュータシステム、ラップトップ若しくはノートブックコンピュータシステム、インタラクティブキオスク、メインフレーム、コンピュータシステムのメッシュ、携帯電話、PDAPersonalDigitalAssistant、サーバ、又はこれらの2以上の組み合わせであってもよい。必要に応じて、コンピュータシステム1800は、1以上のネットワークに1以上のクラウドコンポーネントを有する1以上のコンピュータシステム1800を有し、単一の又は分散化され、複数の場所に及び、複数のマシーンに及び、クラウドに常駐するものであってもよい。必要に応じて、1以上のコンピュータシステム1800は、実質的に空間的又は時間的制約なく、ここに開示又は図示される1以上の方法の1以上のステップを実行してもよい。例えば、限定することなく、1以上のコンピュータシステム1800は、ここに開示又は図示される1以上の方法の1以上のステップをリアルタイムに又はバッチモードにより実行してもよい。1以上のコンピュータシステム1800は、必要に応じて、ここに開示又は図示される1以上の方法の1以上のステップを異なる時点で又は異なる位置において実行するようにしてもよい。ある実施例では、コンピュータシステム1800は、プロセッサ1802、メモリ1804、ストレージ1806、入出力I/Oインタフェース1808、通信インタフェース1810及びバス1812を有する。本開示は、ある配置においてある個数のコンポーネントを有するコンピュータシステムを開示及び図示するが、本開示は、何れか適切な配置において何れか適切な個数の適切なコンポーネントを有する何れか適切なコンピュータシステムを想定する。ある実施例では、プロセッサ1802は、コンピュータプログラムを構成するものなど、命令を実行するためのハードウェアを有する。例えば、限定することなく、命令を実行するため、プロセッサ1802は、整数レジスタ、内部キャッシュ、メモリ1804又はストレージ1806から命令を抽出又はフェッチし、それらを復号化及び実行し、1以上の結果を内部レジスタ、内部キャッシュ、メモリ1804又はストレージ1806に書き込む。ある実施例では、プロセッサ1802は、データ、命令又はアドレスのための1以上の内部キャッシュを有する。本開示は、必要に応じて、何れか適切な個数の何れか適切な内部キャッシュを有するプロセッサ1802を想定する。例えば、限定することなく、プロセッサ1802は、1以上の命令キャッシュ、1以上のデータキャッシュ及び1以上のTLBTranslationLookasideBufferを有してもよい。命令キャッシュの命令は、メモリ1804又はストレージ1806における命令のコピーであってもよく、命令キャッシュは、プロセッサ1802によるこれらの命令の抽出を迅速化する。データキャッシュのデータは、プロセッサ1802において実行される移行の命令によるアクセスのため、又はメモリ1804又はストレージ1806への書き込みのため、プロセッサ1802において実行される以前の命令の結果や他の適切なデータに対して実行するため、プロセッサ1802において実行される命令のためのデータのメモリ1804又は1806へのコピーであってもよい。データキャッシュは、プロセッサ1802によるリード又はライト処理を迅速化する。TLBは、プロセッサ1802のための仮想アドレスの変換を迅速化する。ある実施例では、プロセッサ1802は、データ、命令又はアドレスのための1以上の内部レジスタを有する。本開示は、必要に応じて、何れか適切な個数の何れか適切な内部レジスタを含むプロセッサ1802を想定する。必要に応じて、プロセッサ1802は、1以上のALUArithmeticLogicUnitを有してもよいし、マルチコアプロセッサであってもよいし、又は1以上のプロセッサ1802を有してもよい。本開示はあるプロセッサを開示及び図示しているが、本開示は、何れか適切なプロセッサを想定する。ある実施例では、メモリ1804は、プロセッサ1802が実行する命令やプロセッサ1802が処理するデータを格納するためのメインメモリを有する。例えば、限定することなく、コンピュータシステム1800は、ストレージ1806や他のソース例えば、他のコンピュータシステム1800などからメモリ1804に命令をロードする。その後、プロセッサ1802は、メモリ1804から整数レジスタ又は内部キャッシュに命令をロードする。これらの命令を実行するため、プロセッサ1802は、内部レジスタ又は内部キャッシュから命令を抽出及び復号化する。命令の実行中又は実行後、プロセッサ1802は、1以上の結果中間結果又は最終結果であってもよいを内部レジスタ又は内部キャッシュに書き込む。プロセッサ1802は、その後にこれらの結果の1以上のメモリ1804に書き込む。ある実施例では、プロセッサ1802は、1以上の内部レジスタ若しくは内部キャッシュに又はメモリ1804にある命令しか実行せずストレージ1806などとは対照的に、また1以上の内部レジスタ若しくは内部キャッシュに又はメモリ1804におけるデータに対してしか処理しないストレージ1806などとは対照的に。1以上のメモリバスそれぞれがアドレスバスとデータバスとを含むは、プロセッサ1802とメモリ1804とを結合する。バス1812は、後述されるように、1以上のメモリバスを有する。ある実施例では、1以上のメモリ管理ユニットMMUは、プロセッサ1802とメモリ1804との間にあり、プロセッサ1802により要求されるメモリ1804へのアクセスを実行する。ある実施例では、メモリ1804は、RAMRandomAccessMemoryを有する。このRAMは、必要に応じて揮発性メモリであってもよい。必要に応じて、このRAMは、ダイナミックRAMDRAM又はスタティックRAMSRAMであってもよい。本開示は、何れか適切なRAMを想定する。メモリ1804は、必要に応じて1以上のメモリ1804を有してもよい。本開示はあるメモリを開示及び図示するが、本開示は、何れか適切なメモリを想定する。ある実施例では、ストレージ1806は、データや命令のためのマスストレージを有する。例えば、限定することなく、ストレージ1806は、HDD、フロッピー登録商標ディスクドライブ、フラッシュメモリ、光ディスク、光磁気ディスク、磁気テープ、USBUniversalSerialBusドライブ又はこれらの2以上の組み合わせを有してもよい。ストレージ1806は、必要に応じて、着脱可能な又は着脱不可な又は固定されたメディアを有してもよい。ストレージ1806は、必要に応じて、コンピュータシステム1800の内部又は外部にあってもよい。ある実施例では、ストレージ1806は不揮発性のソリッドステートメモリである。ある実施例では、ストレージ1806は、ROMReadOnlyMemoryを含む。必要に応じて、このROMは、マスクプログラムされたROM、プログラマブルROMPROM、EPROMErasablePROM、EEPROMElectricallyEPROM、EAROMElectricallyAlterableROM、フラッシュメモリ又はこれらの2以上の組み合わせであってもよい。本開示は、何れか適切な物理的形態をとるマスストレージ1806を想定する。ストレージ1806は、必要に応じて、プロセッサ1802とストレージ1806との間の通信を実現する1以上のストレージ制御ユニットを有してもよい。必要に応じて、ストレージ1806は1以上のストレージ1806を有する。本開示はあるストレージを開示及び図示するが、本開示は何れか適切なストレージを想定する。ある実施例では、I/Oインタフェース1808は、コンピュータシステム1800と1以上のI/Oデバイスとの間の通信のための1以上のインタフェースを提供するハードウェア、ソフトウェア又はその方法を含む。コンピュータシステム1800は、必要に応じて、これらのI/Oデバイスの1以上を有してもよい。これらのI/Oデバイスの1以上は、ユーザとコンピュータシステム1800との間の通信を可能にする。例えば、限定することなく、I/Oデバイスは、キーボード、キーパッド、マイクロフォン、モニタ、マウス、プリンタ、スキャナ、スピーカー、スチルカメラ、スタイラス、タブレット、タッチスクリーン、トラックボール、ビデオカメラ、他の適切なI/Oデバイス又はこれらの2以上の組み合わせを有してもよい。I/Oデバイスは、1以上のセンサを有してもよい。本開示は、何れか適切なI/Oデバイスと何れか適切なI/Oインタフェース1808とを想定する。必要に応じて、I/Oインタフェース1808は、これらのI/Oデバイスの1以上を駆動するための1以上のデバイス又はプロセッサ1802を有効にするソフトウェアドライバを有してもよい。I/Oインタフェース1808は、必要に応じて、1以上のI/Oインタフェース1808を有してもよい。本開示はあるI/Oインタフェースを開示及び図示するが、本開示は、何れか適切なI/Oインタフェースを想定する。ある実施例では、通信インタフェース1810は、コンピュータシステム1800と1以上の他のコンピュータシステム1800又は1以上のネットワークとの間の通信例えば、パケットベース通信などのための1以上のインタフェースを提供するハードウェア、ソフトウェア又はその双方を含む。例えば、限定することなく、通信インタフェース1810は、イーサネット登録商標や他の有線ベースネットワーク、Wi-Fiネットワークなどの無線ネットワークと通信するための無線NICWNICや無線アダプタと通信するためのネットワークインタフェースコントローラNICやネットワークアダプタを有してもよい。本開示は、何れか適切なネットワークや何れか適切な通信インタフェース1810とを想定する。例えば、限定することなく、コンピュータシステム1800は、アドホックネットワーク、PANPersonalAreaNetwork、LANLocalAreaNetwork、WANWideAreaNetwork、MANMetropolitanAreaNetwork、インターネットの1以上の部分又はこれらの2以上の組み合わせと通信してもよい。これらのネットワークの1以上の1以上の部分は、有線又は無線であってもよい。例えば、コンピュータシステム1800は、無線PANWPAN例えば、BLUETOOTHWPANなど、Wi-Fiネットワーク、Wi-MAXネットワーク、携帯電話ネットワークGSMGlobalSystemforMobileCommunicationsネットワークなど、他の適切な無線ネットワーク又はこれらの2以上の組み合わせと通信してもよい。コンピュータシステム1800は、必要に応じて、これらのネットワークの何れかのための何れか適切な通信インタフェース1810を有してもよい。通信インタフェース1810は、必要に応じて、1以上の通信インタフェース1810を有してもよい。本開示はある通信インタフェースを開示及び図示するが、本開示は、何れか適切な通信インタフェースを想定する。ある実施例では、バス1812は、コンピュータシステム1800のコンポーネントを互いに接続するハードウェア、ソフトウェア又はその双方を有する。例えば、限定することなく、バス1812は、AGPAcceleratedGraphicsPortや他のグラフィックスバス、EISAEnhancedIndustryStandardArchitectureバス、FSBFront-SideBus、HYPERTRANSPORTHTインターコネクト、ISAIndustryStandardArchitectureISAバス、Infinibandインターコネクト、LPCLow-Pin-Countバス、メモリバス、MCAMicroChannelArchitectureバス、PCIPeripheralComponentInterconnectバス、PCI-XPCI-Expressバス、SATASerialAdvancedTechnologyAttachmentバス、VLBVideoElectronicsStandardAssociationlocalバス、他の適切なバス、又はこれらの2以上の組み合わせを含むものであってもよい。バス1812は、必要に応じて、1以上のバス1812を有してもよい。本開示はあるバスを開示及び図示するが、本開示は、何れか適切なバス又はインターコネクトを想定する。ここでは、コンピュータ可読記憶媒体という表現は、1以上の非一時的な有形のコンピュータ可読記憶媒体が有する構成を含む。例えば、限定することなく、コンピュータ可読記憶媒体は、半導体ベース又は他の集積回路IC例えば、FPGAField-ProgrammableGateArray又はASICApplication-SpecificICなど、ハードディスク、HDD、ハイブリッドハードドライブHHD、光ディスク、光ディスクドライブODD、光磁気ディスク、光磁気ドライブ、フロッピー登録商標ディスク、フロッピー登録商標ディスクドライブFDD、磁気テープ、ホログラフィック記憶媒体、ソリッドステートドライブSSD、RAMドライブ、SECUREDIGITALカード、SECUREDIGITALドライブ、他の適切なコンピュータ可読記憶媒体又はこれらの2以上の組み合わせを含むものであってもよい。ここでは、コンピュータ可読記憶媒体という表現は、保護対象でない媒体を排除する。ここでは、コンピュータ可読記憶媒体という表現保護対象でない信号伝送伝搬電気又は電磁気信号などの一時的形態を排除する。非一時的コンピュータ可読記憶媒体は、揮発性、不揮発性又はこれらの組み合わせであってもよい。本開示は、何れか適切なストレージを実現する1以上のコンピュータ可読記憶媒体を想定する。ある実施例では、コンピュータ可読記憶媒体は、プロセッサ1802の1以上の部分例えば、1以上の内部レジスタ又はキャッシュなど、メモリ1804の1以上の部分、ストレージ1806の1以上の部分又はこれらの組み合わせを実現する。ある実施例では、コンピュータ可読記憶媒体は、RAM又はROMを実現する。ある実施例では、コンピュータ可読記憶媒体は、揮発性又は永続的メモリを実現する。ある実施例では、1以上のコンピュータ可読記憶媒体はソフトウェアを具現化する。ここでは、ソフトウェアという表現は、1以上のアプリケーション、バイトコード、1以上のコンピュータプログラム、1以上の実行可能コード、1以上の命令、ロジック、マシーンコード、1以上のスクリプト、ソースコードなどを含むものであってもよい。ある実施例では、ソフトウェアは、1以上のAPIApplicationProgrammingInterfaceを有する。本開示は、何れか適切なプログラミング言語又はプログラミング言語の組み合わせにより表現若しくは記述される何れか適切なソフトウェアを想定する。ある実施例では、ソフトウェアは、ソースコード又はオブジェクトコードとして表現される。ある実施例では、ソフトウェアは、C、Perl、これらの適切な拡張などのより高いレベルのプログラミング言語により表現される。ある実施例では、ソフトウェアは、アセンブリ言語又はマシーンコードなどのより低いレベルのプログラミング言語により表現される。ある実施例では、ソフトウェアはJavaにより表現される。ある実施例では、ソフトウェアは、HTMLHyperTextMarkupLanguage、XMLExtensibleMarkupLanguage又は他の適切なマークアップ言語により表現される。本開示は、当業者が理解するここでの実施例に対する全ての変更、置換、変形及び改良を含む。同様に、必要に応じて、添付した請求項は、当業者が理解するここでの実施例に対する全ての変更、置換、変形及び改良を含む。以上、本発明の実施例について詳述したが、本発明は上述した特定の実施形態に限定されるものではなく、特許請求の範囲に記載された本発明の要旨の範囲内において、種々の変形変更が可能である。以下の説明に関し、さらに以下の付記を開示する。付記1n個n≧2の変数を有する関数を表現する二分決定図BDDであって、前記n個の変数にそれぞれ対応するn個のレイヤを有するBDDにアクセスするステップと、前記n個の変数の1つの順序付けされた集合の1つのグループを構成するステップと、既存の各グループがk個以下1≦k<nの変数の1以上の順序付けされた集合を有するまで、1以上の変数の1以上の順序付けされた集合の1以上の新たなグループを再帰的に構成し、1以上の変数の1以上の順序付けされた集合の1以上の既存のグループを置換するステップと、前記1以上の既存のグループのそれぞれについて、前記グループ内で取得される前記BDDの複数の異なる変数順序において最小のサイズをもたらすローカルに最適な変数順序を決定するステップと、前記1以上の既存のグループに対応する1以上のローカルに最適な変数順序から、前記1以上の既存のローカルに最適な変数順序において最小のサイズをもたらす前記BDDの最適な変数順序を選択するステップと、を有する1以上の計算装置により実行される方法であって、各繰り返しは、既存の各グループについて、n’個の変数を現在有する前記既存のグループの順序付けされた各集合に対して、n’>kである場合、部分集合の各ペアについて、第1部分集合が前記集合のn’個の変数の個を有し、第2部分集合が前記集合のn’個の変数の個を有する、部分集合の1以上のペアに前記集合を分離するステップと、前記既存のグループの順序付けされた各集合を対応する前記順序付けされた集合を分離することによって構成される部分集合の1以上のペアとそれぞれ置換することによって、前記既存のグループを置換するための1以上の新たなグループを構成するステップと、を有する方法。付記2k=4である、付記1記載の方法。付記3各繰り返しはさらに、既存の各グループについて、n’個の変数を現在有する前記既存のグループの順序付けされた各集合に対して、n’=5である場合、部分集合の各ペアについて、第1部分集合が前記集合の5個の変数の4個を有し、第2部分集合が前記集合の5個の変数の1個を有する、前記部分集合の1以上のペアに前記集合を分離するステップを有する、付記2記載の方法。付記4前記BDDの最適な変数順序に従って前記BDDのn個の変数をリオーダするステップをさらに有する、付記1記載の方法。付記5前記BDDは、非一時的なコンピュータ可読記憶媒体により実現されるデータであり、前記BDDのn個の変数をリオーダするステップは、前記非一時的なコンピュータ可読記憶媒体により実現される前記BDDの1以上のデータを変換する、付記4記載の方法。付記6前記BDDにより表現される関数は、医療センサにより収集されるデータを表現する、付記1記載の方法。付記7電子回路の設計は、前記BDDにより表現される関数を実現する、付記1記載の方法。付記8前記BDDにより表現される関数は、電子回路が充足すべき前記電子回路の性質を規定する、付記1記載の方法。付記9前記BDDにより表現される関数は、システムのフォーマルベリフィケーションに使用される1以上の遷移関係又は1以上の到達可能な状態空間を規定する、付記1記載の方法。付記101以上のプロセッサにより実行可能な命令を有するメモリと、前記メモリに接続され、前記命令を実行するよう動作可能な前記1以上のプロセッサと、を有するシステムであって、前記1以上のプロセッサは、前記命令が実行されると、n個n≧2の変数を有する関数を表現する二分決定図BDDであって、前記n個の変数にそれぞれ対応するn個のレイヤを有するBDDにアクセスするステップと、前記n個の変数の1つの順序付けされた集合の1つのグループを構成するステップと、既存の各グループがk個以下1≦k<nの変数の1以上の順序付けされた集合を有するまで、1以上の変数の1以上の順序付けされた集合の1以上の新たなグループを再帰的に構成し、1以上の変数の1以上の順序付けされた集合の1以上の既存のグループを置換するステップと、前記1以上の既存のグループのそれぞれについて、前記グループ内で取得される前記BDDの複数の異なる変数順序において最小のサイズをもたらすローカルに最適な変数順序を決定するステップと、前記1以上の既存のグループに対応する1以上のローカルに最適な変数順序から、前記1以上の既存のローカルに最適な変数順序において最小のサイズをもたらす前記BDDの最適な変数順序を選択するステップと、を実行するよう動作可能であり、各繰り返しは、既存の各グループについて、n’個の変数を現在有する前記既存のグループの順序付けされた各集合に対して、n’>kである場合、部分集合の各ペアについて、第1部分集合が前記集合のn’個の変数の個を有し、第2部分集合が前記集合のn’個の変数の個を有する、部分集合の1以上のペアに前記集合を分離するステップと、前記既存のグループの順序付けされた各集合を対応する前記順序付けされた集合を分離することによって構成される部分集合の1以上のペアとそれぞれ置換することによって、前記既存のグループを置換するための1以上の新たなグループを構成するステップと、を有するシステム。付記11k=4である、付記10記載のシステム。付記12各繰り返しはさらに、既存の各グループについて、n’個の変数を現在有する前記既存のグループの順序付けされた各集合に対して、n’=5である場合、部分集合の各ペアについて、第1部分集合が前記集合の5個の変数の4個を有し、第2部分集合が前記集合の5個の変数の1個を有する、前記部分集合の1以上のペアに前記集合を分離するステップを有する、付記11記載のシステム。付記13前記1以上のプロセッサはさらに、前記命令が実行されると、前記BDDの最適な変数順序に従って前記BDDのn個の変数をリオーダするステップを実行するよう動作可能である、付記10記載のシステム。付記14前記BDDは、非一時的なコンピュータ可読記憶媒体により実現されるデータであり、前記BDDのn個の変数をリオーダするステップは、前記非一時的なコンピュータ可読記憶媒体により実現される前記BDDの1以上のデータを変換する、付記13記載のシステム。付記15前記BDDにより表現される関数は、医療センサにより収集されるデータを表現する、付記10記載のシステム。付記16電子回路の設計は、前記BDDにより表現される関数を実現する、付記10記載のシステム。付記17前記BDDにより表現される関数は、電子回路が充足すべき前記電子回路の性質を規定する、付記10記載のシステム。付記18前記BDDにより表現される関数は、システムのフォーマルベリフィケーションに使用される1以上の遷移関係又は1以上の到達可能な状態空間を規定する、付記10記載のシステム。付記19n個n≧2の変数を有する関数を表現する二分決定図BDDであって、前記n個の変数にそれぞれ対応するn個のレイヤを有するBDDにアクセスするステップと、前記n個の変数の1つの順序付けされた集合の1つのグループを構成するステップと、既存の各グループがk個以下1≦k<nの変数の1以上の順序付けされた集合を有するまで、1以上の変数の1以上の順序付けされた集合の1以上の新たなグループを再帰的に構成し、1以上の変数の1以上の順序付けされた集合の1以上の既存のグループを置換するステップと、前記1以上の既存のグループのそれぞれについて、前記グループ内で取得される前記BDDの複数の異なる変数順序において最小のサイズをもたらすローカルに最適な変数順序を決定するステップと、前記1以上の既存のグループに対応する1以上のローカルに最適な変数順序から、前記1以上の既存のローカルに最適な変数順序において最小のサイズをもたらす前記BDDの最適な変数順序を選択するステップと、を1以上のコンピュータシステムに実行させるソフトウェアを格納する非一時的なコンピュータ可読記憶媒体であって、各繰り返しは、既存の各グループについて、n’個の変数を現在有する前記既存のグループの順序付けされた各集合に対して、n’>kである場合、部分集合の各ペアについて、第1部分集合が前記集合のn’個の変数の個を有し、第2部分集合が前記集合のn’個の変数の個を有する、部分集合の1以上のペアに前記集合を分離するステップと、前記既存のグループの順序付けされた各集合を対応する前記順序付けされた集合を分離することによって構成される部分集合の1以上のペアとそれぞれ置換することによって、前記既存のグループを置換するための1以上の新たなグループを構成するステップと、を有する記憶媒体。付記20k=4である、付記19記載の記憶媒体。付記21各繰り返しはさらに、既存の各グループについて、n’個の変数を現在有する前記既存のグループの順序付けされた各集合に対して、n’=5である場合、部分集合の各ペアについて、第1部分集合が前記集合の5個の変数の4個を有し、第2部分集合が前記集合の5個の変数の1個を有する、前記部分集合の1以上のペアに前記集合を分離するステップを有する、付記20記載の記憶媒体。付記22前記ソフトウェアはさらに、前記命令が実行されると、前記BDDの最適な変数順序に従って前記BDDのn個の変数をリオーダするステップを実行可能である、付記19記載の記憶媒体。付記23前記BDDは、非一時的なコンピュータ可読記憶媒体により実現されるデータであり、前記BDDのn個の変数をリオーダするステップは、前記非一時的なコンピュータ可読記憶媒体により実現される前記BDDの1以上のデータを変換する、付記22記載の記憶媒体。付記24前記BDDにより表現される関数は、医療センサにより収集されるデータを表現する、付記19記載の記憶媒体。付記25電子回路の設計は、前記BDDにより表現される関数を実現する、付記19記載の記憶媒体。付記26前記BDDにより表現される関数は、電子回路が充足すべき前記電子回路の性質を規定する、付記19記載の記憶媒体。付記27前記BDDにより表現される関数は、記憶媒体のフォーマルベリフィケーションに使用される1以上の遷移関係又は1以上の到達可能な状態空間を規定する、付記19記載の記憶媒体。付記28n個n≧2の変数を有する関数を表現する二分決定図BDDであって、前記n個の変数にそれぞれ対応するn個のレイヤを有するBDDにアクセスする手段と、前記n個の変数の1つの順序付けされた集合の1つのグループを構成する手段と、既存の各グループがk個以下1≦k<nの変数の1以上の順序付けされた集合を有するまで、1以上の変数の1以上の順序付けされた集合の1以上の新たなグループを再帰的に構成し、1以上の変数の1以上の順序付けされた集合の1以上の既存のグループを置換する手段と、前記1以上の既存のグループのそれぞれについて、前記グループ内で取得される前記BDDの複数の異なる変数順序において最小のサイズをもたらすローカルに最適な変数順序を決定する手段と、前記1以上の既存のグループに対応する1以上のローカルに最適な変数順序から、前記1以上の既存のローカルに最適な変数順序において最小のサイズをもたらす前記BDDの最適な変数順序を選択する手段と、を有するシステムであって、各繰り返しは、既存の各グループについて、n’個の変数を現在有する前記既存のグループの順序付けされた各集合に対して、n’>kである場合、部分集合の各ペアについて、第1部分集合が前記集合のn’個の変数の個を有し、第2部分集合が前記集合のn’個の変数の個を有する、部分集合の1以上のペアに前記集合を分離する手段と、前記既存のグループの順序付けされた各集合を対応する前記順序付けされた集合を分離することによって構成される部分集合の1以上のペアとそれぞれ置換することによって、前記既存のグループを置換するための1以上の新たなグループを構成する手段と、を有するシステム。"