(57)【特許請求の範囲】
【請求項１】
複数個の再構成可能なハードウェア・モジュールから成るブールＳＡＴソルバー装置における、複数個のブール変数を含むブールＳＡＴ公式を解くための方法であって、前記ブールＳＡＴソルバー装置は、ブールＳＡＴソルバー・アルゴリズムを実装する少なくとも１つの文節モジュールを有する複数個の要素プロセッサー、制御装置、複数個の要素プロセッサーと制御装置を環状に相互接続するパイプライン・バスを備え、前記ブールＳＡＴソルバー装置の前記制御装置でブールＳＡＴ公式を解くためのコンピューター・プログラムを実行することにより、下記の各ステップを実行する。
前記ブールＳＡＴ公式の複数個のブール変数を既知の値に初期化するステップと、
１個の自由変数を前記複数個のブール変数から選択できるかどうかを判定するステップと、
前記自由変数を選択できない場合に、すべての変数が割り当てられてブールＳＡＴ公式が解決されたことを示すステップと、
前記自由変数を選択できた場合に、事前に決定された値を前記自由変数に割り当てるステップと、
前記自由変数への割り当ての論理含意を計算するステップと、
割り当ての論理含意が変数の中に競合が存在することを示す場合に、当該自由変数の論理含意から発生した競合に対して競合分析を実行するステップと、
割り当てられた自由変数から値を得た変数のバックトラックが可能かどうかを判定するステップと、
バックトラックが可能である場合、前記変数をバックトラックして前記変数を決定し、論理含意の計算ステップへ移行するステップと、
バックトラックが不可能である場合、ブールＳＡＴ公式が解決不能であることを示すステップ。
【請求項２】
複数個のブール変数を有するブールＳＡＴ公式を解くために適応されたコンピューター・システムであって、下記要件を備える。
プロセッサーと、
前記プロセッサーで実行されるブールＳＡＴ公式を解くためのコンピューター・プログラムを格納するメモリーとを備え、
前記プロセッサーが、前記メモリーに格納される前記コンピューター・プログラムを実行することにより、下記の各処理を実行する。
前記ブールＳＡＴ公式の複数個のブール変数を既知の値に初期化する処理と、
１個の自由変数を前記複数個のブール変数から選択できるかどうかを判定する処理と、
前記自由変数を選択できない場合に、すべての変数が割り当てられてブールＳＡＴ公式が解決されたことを示す処理と、
前記自由変数を選択できた場合に、事前に決定された値を前記自由変数に割り当てる処理と、
前記自由変数への割り当ての論理含意を計算する処理と、
割り当ての論理含意が変数の中に競合が存在することを示す場合に、当該自由変数の論理含意から発生した競合に対して競合分析を実行する処理と、
割り当てられた自由変数から値を得た変数のバックトラックが可能かどうかを判定する処理と、
バックトラックが可能である場合、前記変数をバックトラックして前記変数を決定し、論理含意の計算処理へ移行する処理と、
バックトラックが不可能である場合、ブールＳＡＴ公式が解決不能であることを示す処理。
【請求項３】
コンピューター上で動作し、複数個のブール変数を有するブールＳＡＴ公式を解決することを可能にするためのコンピューター・プログラムであって、下記要件を備える。
前記コンピューターが、ブールＳＡＴソルバー・アルゴリズムを実装する少なくとも１つの文節モジュールを有する複数個の要素プロセッサー、制御装置、複数個の要素プロセッサーと制御装置を環状に相互接続するパイプライン・バスを備え、
前記コンピューター・プログラムが、前記コンピューターの前記制御装置に下記の各処理を実行させる。
前記ブールＳＡＴ公式の複数個のブール変数を既知の値に初期化する処理と、
１個の自由変数を前記複数個のブール変数から選択できるかどうかを判定する処理と、
前記自由変数を選択できない場合に、すべての変数が割り当てられてブールＳＡＴ公式が解決されたことを示す処理と、
前記自由変数を選択できた場合に、事前に決定された値を前記自由変数に割り当てる処理と、
前記自由変数への割り当ての論理含意を計算する処理と、
割り当ての論理含意が変数の中に競合が存在することを示す場合に、当該自由変数の論理含意から発生した競合に対して競合分析を実行する処理と、
割り当てられた自由変数から値を得た変数のバックトラックが可能かどうかを判定する処理と、
バックトラックが可能である場合、前記変数をバックトラックして前記変数を決定し、論理含意の計算ステップへ移行する処理と、
バックトラックが不可能である場合、ブールＳＡＴ公式が解決不能であることを示す処理。
【請求項４】
ソルバー装置を使用して複数個のブール変数を有するブールＳＡＴ公式を解決する方法であって、前記ソルバー装置は、ブールＳＡＴソルバー・アルゴリズムを実装する少なくとも１つの文節モジュールを有する複数個の要素プロセッサー、制御装置、複数個の要素プロセッサーと制御装置を環状に相互接続するパイプライン・バス、及び制御装置に相互接続されたホスト・コンピューターを備え、
前記ホスト・コンピュータで、ブールＳＡＴソルバー・アルゴリズム及びブールＳＡＴ公式を前記制御装置にダウンロードするステップを実行し、
前記制御装置で、ブールＳＡＴ公式を解くためのコンピューター・プログラムを実行することにより、
ブールＳＡＴ公式を区分し、この区分を前記複数個の要素プロセッサーにロードするステップと、
ブールＳＡＴ公式の複数個の変数を既知の値に初期化するステップと、
１個の自由変数を前記複数個のブール変数から選択できるかどうかを判定するステップと、
前記自由変数を選択できない場合に、すべての変数が割り当てられてブールＳＡＴ公式が解決されたことを示すステップと、
前記自由変数を選択できた場合に、事前に決定された値を前記自由変数に割り当てるステップと、
前記自由変数への割り当ての論理含意を計算するステップと、
割り当ての論理含意が変数の中に競合が存在することを示す場合に、当該自由変数の論理含意から発生した競合に対して競合分析を実行するステップと、
割り当てられた自由変数から値を得た変数のバックトラックが可能かどうかを判定するステップと、
バックトラックが可能である場合、前記変数をバックトラックして前記変数を決定し、論理含意の計算ステップへ移行するステップと、
バックトラックが不可能である場合、ブールＳＡＴ公式が解決不能であることを示すステップの各ステップを実行する。
【発明の詳細な説明】
【０００１】
【発明の属する技術分野】
本発明は、一連の信号を表すブール・アルゴリズムの中に競合する信号が存在するかどうかを判断することに関する。さらに具体的には、本発明は、再構成可能なハードウェアをパイプライン化されたアーキテクチャーに組み込む装置を使用して、ブール・アルゴリズムに対してブール満足化可能性試験を実施するための方法及び装置である。再構成可能なハードウェアにブール・アルゴリズムの文節が入力され、ブール・アルゴリズムを構成する変数に対して含意及び競合分析が実行される。さらに、本発明は、競合が発見された場合に、その変数に対して非発生順のバックトラックを実施する。本発明は、さまざまな方法、装置、ハードウェア・アーキテクチャー、コンピューター・システム、及びブール・アルゴリズムの満足化可能性試験を行うコンピューター・プログラム製品において実施される。
【０００２】
【従来の技術】
下記の文献には、本発明に関連する標記主題について有益な背景情報が提供されている。
【０００３】
チャレンジ・ベンチマーク：
ＤＩＭＡＣＳ、「ＤＩＭＡＣＳ  Ｃｈａｌｌｅｎｇｅ  Ｂｅｎｃｈｍａｒｋｓａｎｄ  ＵＣＳＣ  Ｂｅｎｃｈｍａｒｋｓ（ＤＩＭＡＣＳのチャレンジ・ベンチマーク及びＵＣＳＣベンチマーク）」、  ｆｔｐ：／／ｄｉｍａｃｓ．ｒｕｔｇｅｒｓ．ｅｄｕ／ｐｕｂ／ｃｈａｌｌｅｎｇｅ／ｓａｔ／ｂｅｎｃｈｍａｒｋｓ／ｃｎｆに掲載。
【０００４】
満足化可能性試験のための再構成可能なハードウェアの使用：
Ｍ．  Ａｂｒａｍｏｖｉｃｉ及びＤ．  Ｓａａｂ、「Ｓａｔｉｓｆｉａｂｉｌｉｔｙ  ｏｎ  Ｒｅｃｏｎｆｉｇｕｒａｂｌｅ  Ｈａｒｄｗａｒｅ（再構成可能なハードウェアの満足化可能性）」、Ｓｅｖｅｎｔｈ  Ｉｎｔｅｒｎａｔｉｏｎａｌ  Ｗｏｒｋｓｈｏｐ  ｏｎ  Ｆｉｅｌｄ  Ｐｒｏｇｒａｍｍａｂｌｅ  Ｌｏｇｉｃ  ａｎｄ  Ａｐｐｌｉｃａｔｉｏｎｓ（フィールド・プログラマブル論理及びアプリケーションに関する第７回国際ワークショップ）（１９９７年）。
【０００５】
シストリック処理システム：
Ｊ．  Ａｒｎｏｌｄ、Ｄ．  Ｂｕｅｌｌ、及びＥ．  Ｄａｖｉｓ、「Ｓｐｌａｓｈ  ２  （Ａｔｔａｃｈｅｄ  Ｐｒｏｃｅｓｓｏｒ  Ｂｏａｒｄ）（Ｓｐｌａｓｈ  ２（付加プロセッサー・ボード））」、Ｆｏｕｒｔｈ  Ａｎｎｕａｌ  ＡＣＭ  Ｓｙｍｐｏｓｉｕｍ  ｏｎ  Ｐａｒａｌｌｅｌ  Ａｌｇｏｒｉｔｈｍｓ  ａｎｄ  Ａｒｃｈｉｔｅｃｔｕｒｅｓ（並列アルゴリズム及びアーキテクチャーに関する第４会年次ＡＣＭシンポジウム）、ｐｐ．  ３１６−３２２（１９９２年）。
【０００６】
ＦＰＧＡ間の仮想配線：
Ｊ．  Ｂａａｂ、Ｒ．  Ｔｅｓｓｉｅｒ、及びＡ．  Ａｇａｒｗａｌ、「Ｏｖｅｒｃｏｍｉｎｇ  Ｐｉｎ  Ｌｉｍｉｔａｔｉｏｎｓ  Ｉｎ  ＦＰＧＡ−Ｂａｓｅｄ  Ｌｏｇｉｃ  Ｅｍｕｌａｔｏｒｓ  （ＦＰＧＡベース論理エミュレーターにおけるピン制限の克服）」、ＩＥＥＥ  Ｗｏｒｋｓｈｏｐ  ｏｎ  ＦＰＧＡ−ｂａｓｅｄ  Ｃｕｓｔｏｍ  Ｃｏｍｐｕｔｉｎｇ  Ｍａｃｈｉｎｅｓ（ＦＰＧＡベース・カスタム計算機に関するＩＥＥＥワークショップ）、ｐｐ．  １４２−１５１（１９９３年）。
【０００７】
等価検査のための組み合わせ検証：
Ｊ．  Ｂｕｒｃｈ及びＶ．  Ｓｉｎｇｈａｌ、「Ｔｉｇｈｔ  Ｉｎｔｅｇｒａｔｉｏｎ  Ｏｆ  Ｃｏｍｂｉｎａｔｉｏｎａｌ  Ｖｅｒｉｆｉｃａｔｉｏｎ  Ｍｅｔｈｏｄｓ（組み合わせ検証方法の緊密な統合）」、Ｐｒｏｃｅｅｄｉｎｇｓｏｆ  ＩＣＣＡＤ（ＩＣＣＡＤの処理）、ｐｐ．  ５７０−５７６（１９９８年）。
【０００８】
推移閉包計算及び意思決定の使用による試験生成アルゴリズム：
Ｓ．  Ｃｈａｋｒａｄｈａｒ、Ｖ．  Ａｇｒａｗａｌ、及びＳ．  Ｒｏｔｈｗｅｉｌｅｒ、「Ａ  Ｔｒａｎｓｉｔｉｖｅ  Ｃｌｏｓｕｒｅ  Ａｌｇｏｒｉｔｈｍ  Ｆｏｒ  Ｔｅｓｔ  Ｇｅｎｅｒａｔｉｏｎ（試験生成用推移閉包アルゴリズム）」ＩＥＥＥ  Ｔｒａｎｓａｃｔｉｏｎｓ  ｏｎ  Ｃｏｍｐｕｔｅｒ−Ａｉｄｅｄ  Ｄｅｓｉｇｎ  ｏｆ  Ｉｎｔｅｇｒａｔｅｄ  Ｃｉｒｃｕｉｔｓ  ａｎｄＳｙｓｔｅｍｓ  （集積回路及びシステムのコンピュータ支援設計に関するＩＥＥＥ報告書）、Ｖｏｌ．１２、Ｎｏ．７、ｐｐ．１０１５−２８（１９９３年７月）。
【０００９】
数量化理論のための統一プルーフ手順：
Ｍ．  Ｄａｖｉｓ及びＨ．  Ｐｕｔｎａｍ、「Ａ  Ｃｏｍｐｕｔｉｎｇ  Ｐｒｏｃｅｄｕｒｅ  ｆｏｒ  Ｑｕａｎｔｉｆｉｃａｔｉｏｎ  Ｔｈｅｏｒｙ  （数量化理論の計算手順）」、Ｊｏｕｒｎａｌ  ｏｆ  ｔｈｅ  ＡＣＭ（米国計算機学会機関誌）、Ｖｏｌ．７、ｐｐ．２０１−２１５（１９６０年）。
【００１０】
組み合わせ論理回路用の経路指向意思決定（ＰＯＤＥＭ：  Ｐａｔｈ−Ｏｒｉｅｎｔｅｄ  Ｄｅｃｉｓｉｏｎ  Ｍａｋｉｎｇ）：
Ｐ．  Ｇｏｅｌ、「Ａｎ  Ｉｍｐｌｉｃｉｔ  Ｅｎｕｍｅｒａｔｉｏｎ  Ａｌｇｏｒｉｔｈｍ  Ｔｏ  Ｇｅｎｅｒａｔｅ  Ｔｅｓｔｓ  Ｆｏｒ  Ｃｏｍｂｉｎａｔｉｏｎａｌ  Ｌｏｇｉｃ  Ｃｉｒｃｕｉｔｓ（組み合わせ論理回路用試験生成のための間接的列挙アルゴリズム）」、ＩＥＥＥ  Ｔｒａｎｓａｃｔｉｏｎｓｏｎ  Ｃｏｍｐｕｔｅｒｓ（コンピューターに関するＩＥＥＥ報告書）、Ｖｏｌ．Ｃ３０、Ｎｏ．３、ｐｐ．３３７−３４３（１９８１年３月）。
【００１１】
ブール満足化可能性チェッカーと連結された２進法決定ダイアグラムの使用による、問題規模の縮小及びバックトラック要件の削減：
Ａ．  Ｇｕｐｔａ及びＰ．  Ａｓｈａｒ、「Ｉｎｔｅｇｒａｔｉｎｇ  Ａ  Ｂｏｏｌｅａｎ  Ｓａｔｉｓｆｉａｂｉｌｉｔｙ  Ｃｈｅｃｋｅｒ  Ａｎｄ  ＢＤＤｓ  Ｆｏｒ  Ｃｏｍｂｉｎａｔｉｏｎａｌ  Ｖｅｒｉｆｉｃａｔｉｏｎ（組み合わせ検証のためのブール満足化可能性チェッカーとＢＤＤの統合）」、Ｐｒｏｃｅｅｄｉｎｇｓ  ｏｆ  ＶＬＳＩ  Ｄｅｓｉｇｎ  ９８（ＶＬＳＩ設計９８の議事録）、ｐｐ．２２２−２２５（１９９８年）。
【００１２】
組み合わせ回路における単一スタックアット障害に関する試験パターンの生成におけるブール満足化可能性手法の使用：
Ｔ．  Ｌａｒｒａｂｅｅ、「Ｔｅｓｔ  Ｐａｔｔｅｒｎ  Ｇｅｎｅｒａｔｉｏｎ  Ｕｓｉｎｇ  Ｂｏｏｌｅａｎ  Ｓａｔｉｓｆｉａｂｉｌｉｔｙ（ブール満足化可能性の使用による試験パターンの生成）」、ＩＥＥＥ  Ｔｒａｎｓａｃｔｉｏｎｓ  ｏｎ  Ｃｏｍｐｕｔｅｒ−Ａｉｄｅｄ  Ｄｅｓｉｇｎ（コンピューター支援設計に関するＩＥＥＥ報告書）、Ｖｏｌ．１１、Ｎｏ．１、ｐｐ．４−１５（１９９２年１月）。
【００１３】
競合分析による基本的バックトラックの増補：
Ｊ．  Ｓｉｌｖａ及びＫ．  Ｓａｋａｌｌａｈ、「ＧＲＡＳＰ−Ａ  Ｎｅｗ  Ｓｅａｒｃｈ  Ａｌｇｏｒｉｔｈｍ  Ｆｏｒ  Ｓａｔｉｓｆｉａｂｉｌｉｔｙ（満足化可能性ための新探索アルゴリズムＧＲＡＳＰ−Ａ）」Ｐｒｏｃｅｅｄｉｎｇｓ  ｏｆ  ＩＣＣＡＤ（ＩＣＣＡＤの議事録）、ｐｐ．２２０−２２７（１９９６年）。
【００１４】
組み合わせ論理試験生成に関する満足化可能性への縮約の使用：
Ｐ．  Ｓｔｅｐｈａｎ、Ｒ．  Ｂｒａｙｔｏｎ及びＡ．  Ｓａｎｇｉｏｖａｎｎｉ−Ｖｉｎｃｅｎｔｅｌｌｉ、「Ｃｏｍｂｉｎａｔｉｏｎａｌ  Ｔｅｓｔ  Ｇｅｎｅｒａｔｉｏｎ  Ｕｓｉｎｇ  Ｓａｔｉｓｆｉａｂｉｌｉｔｙ（満足化可能性を使用した組み合わせ試験生成）」、ＩＥＥＥ  Ｔｒａｎｓａｃｔｉｏｎｓ  ｏｎ  Ｉｎｔｅｇｒａｔｅｄ  Ｃｉｒｃｕｉｔｓ  ａｎｄ  Ｓｙｓｔｅｍｓ（集積回路及びシステムに関するＩＥＥＥ報告書）、Ｖｏｌ．１５、Ｎｏ．９、ｐｐ．１１６７−７６（１９９６年９月）。
【００１５】
ＦＰＧＡ上の各問題インスタンスを解決する専用回路の使用による満足化可能性問題の解決：
Ｔ．  Ｓｕｙａｍａ、Ｍ．  Ｙｏｋｏｏ、及びＨ．  Ｓａｗａｄａ、「Ｓｏｌｖｉｎｇ  Ｓａｔｉｓｆｉａｂｉｌｉｔｙ  Ｐｒｏｂｌｅｍｓ  ｏｎ  ＦＰＧＡｓ（ＦＰＧＡ上の満足化可能性問題の解決）」、Ｓｉｘｔｈ  Ｉｎｔｅｒｎａｔｉｏｎａｌ  Ｗｏｒｋｓｈｏｐ  ｏｎ  Ｆｉｅｌｄ  ＰｒｏｇｒａｍｍａｂｌｅＬｏｇｉｃ  ａｎｄ  Ａｐｐｌｉｃａｔｉｏｎｓ（フィールド・プログラマブル論理及びアプリケーションに関する第６回国際ワークショップ）（１９９６年）。
【００１６】
次に、本発明を理解するための適切な基礎を提供するため上記の技術について論じる。
【００１７】
文献に示されるように、ブール満足化可能性検査（ＳＡＴ：  ＢｏｏｌｅａｎＳａｔｉｓｆｉａｂｉｌｉｔｙ  Ｃｈｅｃｋｉｎｇ）は、超大規模集積（ＶＬＳＩ：  ｖｅｒｙ  ｌａｒｇｅ  ｓｃａｌｅ  ｉｎｔｅｇｒａｔｅｄ）回路のコンピュータ支援設計（ＣＡＤ）における多数のアプリケーションの中核をなすものである。文献では、ＦＰＧＡ（Ｆｉｅｌｄ  Ｐｒｏｇｒａｍｍａｂｌｅ  Ｇａｔｅ  Ａｒｒａｙ：  フィールド・プログラマブル・ゲート・アレイ）をベースとする、インスタンスごとの再構成が可能なハードウェアを使用してＳＡＴを迅速化する技術が多数提案されている。ＳＡＴのソフトウェア実装における大幅な迅速化に成功した例は多数報告されているが、この技術が広く普及するためには、いつくかの根本的な課題の解決が待たれる。
【００１８】
【発明が解決しようとする課題】
第１の根本的な課題は、アルゴリズムのハードウェア実装をＦＰＧＡ上にコンパイルするための時間的なオーバーヘッドである。これには、論理ネット・リストをＦＰＧＡの組み合わせ論理ブロック（ＣＬＢ：  Ｃｏｍｂｉｎａｔｉｏｎ  Ｌｏｇｉｃ  Ｂｌｏｃｋｓ）にマッピングする時間と、場所及び経路を指定するための時間が含まれる。現実には、この２つを合わせた時間は、実際に公式を解く時間に匹敵するかそれ以上の長さとなるのがほとんどである。これは、ソフトウェアにおいても同様である。
【００１９】
第２の根本的な課題は、ハードウェア・アルゴリズムにおいて達成されている高度化のレベルが最良のソフトウェア・アルゴリズムのレベルに匹敵しないことである。基本的には、ハードウェア・アルゴリズムの高速化は、生並行処理に依存して実現される。その結果、ソフトウェアのヒューリスティック手法が非常に効率的に機能するために、ソフトウェア実装の方がハードウェア・アルゴリズムより高速かそれと同程度となる例は多数ある。ＳＡＴをハードウェアの面から高速化するための従来の取り組みでは、ハードウェアＳＡＴアルゴリズムに非発生順のバックトラックが組み込まれていた。また、ＳＡＴソルバーを大幅に高速化する上でしばしば効果を発揮するもう１つの重要な方法としては、探索の必要のない解の部分空間に対応する文節を付加することが挙げられる。ただし、従来のアーキテクチャーでこの方法を実施することは実際には不可能である。
【００２０】
もう１つの根本的な欠点は、従来のアーキテクチャーではクロック速度がＦＰＧＡで達成可能な速度よりはるかに低速となってしまうことである。このクロック速度の低速化は、リテラル間の接続がワイヤーにより実装されるためレイアウトが不規則となること、長いワイヤーを使用しなければならないこと、ワイヤーがＦＰＧＡの境界を横断すること、という３つの原因による。
【００２１】
ブール満足化可能性の問題はよく知られた制約満足化問題であり、試験生成、論理検証、及びタイミング分析などのコンピューター支援設計において幅広く使用されている。ブール公式を与えられた場合、その目的は、公式の評価が真となる０−１値の変数割り当てを発見するか、あるいはそのような割り当てが存在しないことを立証するかのいずれかである。
【００２２】
ブール公式は、典型的には論理積正規形（ＣＮＦ：  ｃｏｎｊｕｎｃｔｉｖｅｎｏｒｍａｌ  ｆｏｒｍ）で表現され、「積和形式」とも呼ばれる。ＣＮＦに含まれる各々の和の項（文節）は、いくつかの単一リテラルの和であり、ここでの各リテラルは１つの変数またはその否定である。ｎ文節とは、ｎ個のリテラルを有する文節である。例えば、Ｖｉ＋Ｖ’ｊ＋Ｖｋは３文節と呼ばれる。公式全体の評価結果が１になるためには、各文節が満たされる（すなわち、評価結果が１になる）ことが必要である。
【００２３】
現在のほとんどのＳＡＴソルバーは、Ｄａｖｉｓ−Ｐｕｔｎａｍアルゴリズムをベースとしている。図１２を参照すると、この図には基本Ｄａｖｉｓ−Ｐｕｔｎａｍアルゴリズムの擬似コードが示されている。また、図１３には、基本Ｄａｖｉｓ−Ｐｕｔｎａｍアルゴリズムの処理フローが図示されている。
【００２４】
この基本アルゴリズムは、ステップＳ１００に示されるように、空の部分割り当てから始まる。ステップＳ１１０では、アルゴリズムは、使用可能な自由変数があるかどうかを判断する。アルゴリズムは、自由変数に０または１の値を１つずつ割り当てながら処理を進める。各割り当ての後、アルゴリズムはステップＳ１２０で、その割り当てが他の変数に対して有する直接含意と推移含意を決定する。ステップＳ１３０では、アルゴリズムは矛盾をチェックする。ステップＳ１４０で含意プロシージャー中に矛盾が検出されなかった場合、アルゴリズムはステップＳ１５０で次の自由変数を選択し、含意プロシージャーを繰り返す。矛盾が検出されなかった場合、アルゴリズムは、ステップＳ１６０−Ｓ１８０に示されるように、これまで１つの値についてのみ試みられた直近の割り当て変数を相補することにより、新たな部分割り当てを試みる。このステップはバックトラックと呼ばれる。使用可能な自由変数が尽き、かつ矛盾に遭遇しなかったとき（すなわち、すべての文節が満足され、解が発見された）か、あるいは、可能性のある割り当てが尽きたときに、アルゴリズムは終了する。このアルゴリズムは、解が存在していればそれを検出するという点で、完全であると言うことができる。
【００２５】
含意の決定は、探索空間のプルーニングを行う上で極めて重要である。それは、（１）含意の決定により、アルゴリズムは矛盾する部分割り当てに対応する探索空間の全領域をスキップできる、及び（２）１つの暗黙変数により、探索の実行対象となる自由変数が１つ減る、という２つの理由による。残念ながら、新規の割り当て変数または暗黙変数を含む文節が１つずつスキャンされて順に更新され、新たな含意が検出されなくなるまでこのプロセスが繰り返されるので、ソフトウェアでの含意の検出は非常に低速である。
【００２６】
ハードウェアによるＳＡＴアルゴリズムの高速化が期待されるのは、アルゴリズムの中核を成す含意プロシージャーは高度な並列化が可能であり、基本論理ゲートに容易にマッピングできる、という２つの理由による。
【００２７】
この分野の最近の文献では、同一の基本フローを維持しながらアルゴリズムの機能を拡張したＤａｖｉｓ−Ｐｕｔｎａｍアルゴリズムのさまざまなソフトウェア実装が報告されている。特に、ＧＲＡＳＰの研究は、非発生順のバックトラック（競合分析）と動的文節付加を適用することによって探索空間のさらなるプルーニングに貢献したという点で注目に値する。
【００２８】
競合分析及び文節付加は、比較的容易にソフトウェア実装できる。新規の値が暗黙に定義されると、その値は含意グラフを記録するデータ構造に追加される。競合が発生した場合は、グラフを後方にトラバースすることによってその競合の先行点が識別される。新規の文節を文節データベースに追加することも容易である。こうした手法によって、多数の問題におけるパフォーマンスを大幅に向上させることができる。
【００２９】
ＧＲＡＳＰにより報告されたパフォーマンス向上の多くの部分は、その競合分析の実装によって実現された。基本Ｄａｖｉｓ−Ｐｕｔｎａｍアルゴリズムは、競合を確認すると、バックトラックして部分割り当てを変更する。ただし、このアルゴリズムは、確認された競合の真の原因はどの変数かを分析することはしない。つまり、このバックトラック・プロセスは、競合に関連のない変数を相補し、その先にある袋小路を繰り返し探索する恐れがある。これより高度な競合分析は、競合に至る変数割り当てを識別する機能をもつ。このタイプの競合分析は、逆含意プロシージャーとして動作しながら、競合に至る暗黙リテラルの推移先行点を識別する。
【００３０】
ここで、方程式（１）に示される以下の３文節から成るブール公式を例にとって考察する。
【数１】
0004404438.tif 000002
ｖ１、ｖ２  ．．．  ｖ７がすでに１に割り当てられており、続いてｖ８が１に割り当てられるとすると、その結果は図１に示されるような含意グラフとなる。競合はｖ１０で検出される。この競合の先行点は、ｖ１、ｖ３、及びｖ８である。同様に、ｖ８が０に変更されると（図２参照）、ｖ８はｖ９に競合を発生させる。この競合の原因は、ｖ１、ｖ２、及びｖ’８である。この時点で、ｖ８がどちらの値であっても競合に至ることがわかる。基本アルゴリズムであれば、ここでｖ７の値が０に変更され、再度試行される。しかし、実際にはｖ１、ｖ２、及びｖ３が競合の原因であるので、二重の競合を引き起こす直近の割り当て変数、すなわちｖ３まで直接バックトラックすることができる。これは、非発生順バックトラックと呼ばれる。
【００３１】
一般に、分岐変数ｖｋで競合に初めて遭遇した場合、この先行点セットはＰ（ｖｋ）として識別することができる。その後ｖ’ｋの競合がある場合は、別の先行点セットのＰ（ｖ’ｋ）を得ることができる。ｖｋ及びｖ’ｋを除くこれら２セットの合併は、ｖｋにおける二重の競合に至る先行点である。このセット内の変数までバックトラックすることは可能である。
【００３２】
先に挙げた実施例では、競合分析により、ｖ１、ｖ２、及びｖ３がすべて１の場合は公式が満足されないことが明らかとなる。これは隠れた制約であり、文節として直接明示されることはない。解決しようとするブール公式には、新規の文節（ｖ’１＋ｖ’２＋ｖ’３）を付加できる。この文節を公式に付加することにより、ソルバーはこの競合を早期に検出し、今後の探索において同じ空間を探索する無駄を省くことができる。
【００３３】
競合分析及び文節付加は、比較的容易にソフトウェア実装できる。新規の値が暗黙に示されると、その値は含意グラフを記録するデータ構造に追加される。競合が発生した場合は、グラフを後方にトラバースすることによってその競合の先行点が識別される。新規の文節を文節データベースに追加することも容易である。こうした手法によって、多数の問題におけるパフォーマンスを大幅に向上させることができる。  文献には、再構成可能なハードウェアを使用してＳＡＴを解くためのいくつかの提案が記載されている。Ｓｕｙａｍａその他は、Ｄａｖｉｓ−Ｐｕｔｎａｍのアプローチとは明確に異なった独自のＳＡＴアルゴリズムを提案している。彼らのアプローチの特徴は、どの時点においても（部分的ではなく）完全な変数割り当てが評価されるということである。Ｓｕｙａｍａその他は探索空間のプルーニングを行うための探索ヒューリスティック手法を提案しているが、そのアプローチでビジットされた状態の数は、基本Ｄａｖｉｓ−Ｐｕｔｎａｍアプローチでビジットされた数の最大８倍に上ることもありうることを認めている。
【００３４】
Ａｂｒａｍｏｖｉｃｉ及びＳａａｂの研究でも、構成可能なハードウェアＳＡＴソルバーが提案されている。そのアプローチは、基本的には、再構成可能なハードウェア内にＰＯＤＥＭ（Ｐａｔｈ−Ｏｒｉｅｎｔｅｄ  ＤＥｃｉｓｉｏｎ  Ｍａｋｉｎｇ：  経路指向意思決定）ベースのアルゴリズムを実装するものと言うことができる。ＰＯＤＥＭは、試験生成問題を解決するために使用されるのが典型的である。回路の一次入力と一次出力の制御と観察に依存するＰＯＤＥＭとは異なり、このＤａｖｉｓ−Ｐｕｔｎａｍアルゴリズムは回路内の内部変数間の関係も捕捉する。これにより、ビジットされる状態空間とランタイムが大幅に減少される。
【００３５】
さらに、文献に記述される従来のハードウェアＳＡＴソルバーは、動的文節付加を採用していない。重要なのは、従来のアプローチはいずれも、公式ごとに著しく異なる公式特化ソルバー回路を生成する点である。そのため、各公式の回路全体を完全に合成し、配置及び経路指定し、複数のＦＰＧＡにゼロからダウンロードしなければならない。これは、かなりのランタイム・オーバーヘッドとなる。  本発明は上記の事情を背景としてなされたものであり、従来技術の上記の問題及び限界を克服することを目的とし、さらに、ブールＳＡＴ公式を解く機能を提供することを目的とする。
【００３６】
本発明の追加の目的及び利点については、その一部を以下の記述の中で述べるが、その他の部分については本記述から明らとなるか、もしくは本発明を実践することにより知ることができるであろう。本発明の目的及び利点は、付属の請求項の中で特に指摘する器具及び組み合わせにより実現及び達成することができる。
【００３７】
本発明のさらなる目的は、ブールＳＡＴ公式を解くための方法、コンピューター・システム、及びコンピューター・プログラム製品を提供することにある。
【００３８】
本発明のまたさらなる目的は、ブールＳＡＴ公式を解くためのブールＳＡＴソルバーを作成するための方法、コンピューター・システム、及びコンピューター・プログラム製品を提供することにある。
【００３９】
本発明のまたさらなる目的は、ブールＳＡＴ公式をダウンロードして区分化し、ブールＳＡＴ公式を解くための要素プロセッサーにその区分をロードするための方法及び装置を提供することにある。
【００４０】
【課題を解決するための手段】
本発明の上記及びその他の目的は、ブールＳＡＴ公式から得た変数を処理対象として引き渡すための手段として、要素プロセッサーと制御装置との間に設けた環状トポロジー・パイプライン・バスを使用する装置を提供することにより達成される。
【００４１】
本発明の上記及びさらなる目的は、さらに、隠れた制約を発見するためにブールＳＡＴ公式に冗長文節を動的に付加する方法及び装置を提供することによりさらに達成される。
【００４２】
上記の目的は、さらに、ブールＳＡＴ公式の変数間の含意及び競合を計算し、検出された競合を解決するために非発生順のバックトラックを実行するための方法を提供することによって達成される。
【００４３】
上記の目的は、ブールＳＡＴ公式を解くためのブールＳＡＴソルバー装置を生成する方法を提供することにより達成されるのが望ましく、ここでのブールＳＡＴソルバーは複数個の再構成可能なハードウェア・モジュールを備え、当該方法には、ブールＳＡＴ公式を読み取ること、ブールＳＡＴ公式を区分化し、この各区分を事前に決定された変数数に制限すること、複数個の再構成可能なモジュールを回路アレイを形成するように構成すること、ブールＳＡＴ公式の区分を複数個の再構成可能なハードウェア・モジュールの各々における回路アレイに割り当てること、及び、複数の再構成可能なハードウェア・モジュールの各々の中でブールＳＡＴ公式の各区分に固有な機能及び接続をプログラムすることが含まれる。
【００４４】
上記の目的は、さらに、複数個の再構成可能なハードウェア・モジュールから成るブールＳＡＴソルバーを使用して、複数個のブール変数を含むブールＳＡＴ公式を解くための方法を提供することにより達成されるのが望ましく、当該方法は、複数個のブール変数を既知の状態に設定するステップ、１個の自由変数を複数個のブール変数から選択し、自由変数の選択の結果に応じて、既知の値を選択された自由変数に割り当てるか、すべての変数が割り当てられてブールＳＡＴ公式が解決されたことを示すステップ、事前に決定された値を当該自由変数に割り当てるステップ、当該自由変数への割り当ての論理含意を計算し、論理含意の結果に応じて、当該自由変数に対して競合分析を実行するか、複数個のブール変数から別の自由変数を選択するかのいずれかを行うステップ、当該自由変数の論理含意から発生した競合に対して競合分析を実行するステップ、及び、割り当てられた自由変数から値を得た先行の変数をバックトラックするかどうかを決定し、バックトラックの決定の結果に応じて、当該先行変数をバックトラックして論理含意を再び開始するか、ブールＳＡＴ公式が解決不能であることを示すかのいずれかを行うステップを備える。
【００４５】
上記の目的は、さらに、複数個のブール変数を有するブールＳＡＴ公式を解決するように適応されたコンピューター・システムを提供することにより達成されるのが望ましく、当該コンピューター・システムは、複数個のブール変数を既知の状態に設定するステップ、１個の自由変数を複数個のブール変数から選択し、自由変数の選択の結果に応じて、既知の値を選択された自由変数に割り当てるか、すべての変数が割り当てられブールＳＡＴ公式が解決されたことを示すかのいずれかを行うステップ、事前に決定された値を当該自由変数に割り当てるステップ、当該自由変数への割り当ての論理含意を計算し、論理含意の結果に応じて、当該自由変数に対して競合分析を実行するか、複数個のブール変数から別の自由変数を選択するかのいずれかを行うステップ、当該自由変数の論理含意から発生した競合に対し競合分析を実行するステップ、及び、割当てられた自由変数から値を得た先行の変数をバックトラックするかどうかを決定し、バックトラックの決定の結果に応じて、当該先行変数をバックトラックして論理含意を再び開始するか、ブールＳＡＴ公式が解決不能であることを示すことを示すかのいずれかを行うステップをコンピューター・システムが実行できるようにするために適応されたソフトウェア命令を備えるプロセッサー及びメモリーを備える。
【００４６】
上記の目的は、さらに、コンピューターが複数個のブール変数を有するブールＳＡＴ公式を解決することを可能にするためのコンピューター・プログラム製品を提供することによって達成されるのが望ましく、当該コンピューター・プログラム製品は、コンピューターが事前に決定された演算を実行することを可能にするためのソフトウェア命令、及び当該ソフトウェア命令を保持するコンピューター読み取り可能媒体を備え、当該の事前に決定された演算には、複数個のブール変数を既知の状態に設定するステップ、１個の自由変数を複数個のブール変数から選択し、自由変数の選択の結果に応じて、当該の選択された自由変数に既知の値を割り当てるか、すべての変数が割り当てられてブールＳＡＴ公式が解決されたことを示すかのいずれかを行うステップ、事前に決定された値を当該自由変数に割り当てるステップ、当該自由変数への割り当ての論理含意を計算し、論理含意の結果に応じて、当該自由変数に競合分析を実行するか、複数個のブール変数から別の自由変数を選択するかのいずれかを行うステップ、当該自由変数の論理含意から発生した競合に対して競合分析を実行するステップ、割り当てられた自由変数から値を得た先行の変数をバックトラックするかどうかを決定し、バックトラックの決定の結果に応じて、先行変数をバックトラックして論理含意を再び開始するか、ブールＳＡＴ公式が解決不能であることを示すかのいずれかを行うステップが含まれる。
【００４７】
上記の目的は、さらに、ソルバー装置を使用して複数個のブール変数を有するブールＳＡＴ公式を解決する方法を提供することにより達成されるのが望ましく、ここでのソルバー装置は複数個の要素プロセッサー、制御装置、複数個の要素プロセッサーと制御装置を環状に相互接続するパイプライン・バス、及び制御装置に相互接続されたホスト・コンピューターを備え、当該方法には、ブールＳＡＴ公式を制御装置にダウンロードすること、ブールＳＡＴ公式を区分し、この区分を複数個の要素プロセッサーにロードすること、ブールＳＡＴ公式の複数個の変数を既知の値に初期化すること、複数個のブール変数から１個の自由変数の選択を試み、既知の値を自由変数に割り当てる試みの結果に応じて、当該自由変数を既知の値に割り当てるか、ブールＳＡＴ公式が解決されたことを示すかのいずれかを実行すること、当該自由変数への割り当ての論理含意を計算し、論理含意の結果に応じて、当該自由変数に対して競合分析を実行するか、割り当て用として複数個のブール変数から別の自由変数を選択するかのいずれかを行うこと、当該自由変数の論理含意から発生した競合に対して競合分析を実行すること、割り当てられた自由変数から値を得た先行の変数をバックトラックするかどうかを決定し、バックトラックの決定の結果に応じて、先行変数をバックトラックして論理含意を再び開始するか、ブールＳＡＴ公式が解決不能であることを示すかのいずれかを行うことが含まれる。
【００４８】
上記の目的は、さらに、ブールＳＡＴソルバー・アルゴリズム及び公式をダウンロードし、対応するブールＳＡＴ問題を解決するための装置を提供することにより達成されるのが望ましく、そのアーキテクチャーは、ブールＳＡＴソルバー・アルゴリズムを実装するための少なくとも１つの文節モジュール、ブールＳＡＴソルバー・アルゴリズム及び公式を受け取ってブールＳＡＴソルバー・アルゴリズム及び公式を当該の少なくとも１つの文節モジュールに分配するための制御装置、制御装置と当該の少なくとも１つの文節モジュールを環状トポロジーに相互接続し、それにより、ブールＳＡＴソルバー・アルゴリズム、公式、及び変数値を制御装置と当該の少なくとも１つの文節モジュールとの間、及び文節モジュール同士の間で引き渡すことを可能にするパイプライン・バス、及び、ブールＳＡＴソルバー・アルゴリズム及び公式を制御装置にダウンロードし、そこから結果を受け取るためのホスト・コンピューターを備える。
【００４９】
【発明の実施の形態】
次に、本発明の好適な実施の形態について図面を参照しつつ詳細に説明する。
【００５０】
従来のアーキテクチャーの設計フローでは、各ＳＡＴ公式を再構成可能なハードウェア、すなわちＦＰＧＡにおいて実装するためには、合成、マッピング、場所と経路の指定、及びビット・ストリーム生成という４つのステップのすべてが必要とされる。本発明により、規則性の量と反復構成の数が最大限に拡大された。この規則性は、従来のアーキテクチャーよりもはるかに高速な命令のアーキテクチャーをもたらすコンパイル・フローとともに利用される。
【００５１】
本発明のモジュール性は、ＳＡＴソルバー回路が文節ベースであることから生じる。各文節の分岐回路は、その文節から生じた変数含意をカプセル化する。ｎリテラル文節の分岐回路は、どの組み合わせにおいても入出力接続を除いて同一である。特に、一般的な３リテラル文節ｖｉ＋ｖｊ＋ｖｋの含意分岐回路は下記のようなものとなる。
【数２】
0004404438.tif 000003
ここで、ｖ’ｉ、ｖ’ｊ、ｖ’ｋは入力であり、ｖｉ、ｖｊ、ｖｋは暗黙出力である。同数のリテラルを有する文節については、１つのモジュールを設計するだけでよい。これらのモジュールは、１度コンパイルすれば、ＦＰＧＡ内の異なる場所に配置することができる。その後、各文節の最後の分岐回路が、入出力ワイヤーの識別により決定される。
【００５２】
コンパイルを高速で行うためには、文節分岐回路自身のモジュラー・マッピングだけでは不十分であり、信号の経路指定もまた重要である。例えば、直接ワイヤー接続部を有する固定文節モジュールを使用する場合でも、その結果得られる回路の場所と経路の指定はまだなお困難である。データ通信のためには、さらに規則正しい構成が必要とされる。その構成は、バスなどの固定された構成であるのが理想的である。同時に、その構成は、暗黙値を伝搬するための帯域幅をサポートする必要がある。
【００５３】
バスまたはクロスバーは規則性のある通信を提供できるが、典型的なバスは一度に１回のトランザクションしか行うことができない。これは、通信帯域幅の制限要因となる。また、複数のＦＰＧＡを単一のバスに効率的に接続することは困難である。一方、クロスバーは、高い帯域幅で２点間通信を提供できる。しかしながら、文節と変数が多数であるため、固定クロスバーのワイヤー数が非常に多くなるので、所要数の接続を行うことは現実には実行可能でない。
【００５４】
ＳＡＴ問題の通信要件を研究した結果、本発明では、各タイム・スロットが固定の変数セットに対応付けられる環状トポロジー・パイプライン・バス構成を使用することとした。興味深いことに、ＳＡＴ問題のデータ通信要件は、そのメッセージが本質的には変数を新規の値に更新するために使用される点で、一般の並行処理とは異なる。変数の個数は比較的少なく、数百程度である。回路周辺の全変数の値を送出する固定タイミング・シーケンスの使用により、通信制御が簡素化される。
【００５５】
次に、本発明の実施の形態の利点を大まかに説明する。本発明の装置の実施例では、パイプライン・バスは複数のＦＰＧＡにまたがってリングを形成する。データのパイプライン化を実施するために、Ｄ型のフリップ・フロップがバス上に配置される。各ＦＰＧＡは、パイプライン・バス上の１段に相当する。各ＦＰＧＡでは、パイプライン・バス上の値は各段の文節分岐回路により監視または変更できる。典型的なバス・トランザクション・プロトコルは使用しない。データ・ビットは固定シーケンスでパイプライン・バス上に伝搬され、変数の識別は単純なカウンター／コンパレーターにより決定される。
【００５６】
例えば、ＳＡＴ公式に１６０個の変数があり、バスの幅は３２ビットであるとする。変数のリテラルは、ｖ０、ｖ’０、．．．ｖ１５９、ｖ’１５９として索引付けされる。１６個の変数のリテラルは１段で３２本のワイヤーを占有する。ワイヤーはｗ０．．．ｗ３１である。クロックｔ０で、ｖ０、ｖ’０．．．ｖ１５、ｖ’１５が同じ段にある場合、クロックｔ０＋１では、ｖ１６、ｖ’１６．．．ｖ３１、ｖ’３１がこの段にパイプライン化され、ｖ０、ｖ’０．．．ｖ１５、ｖ’１５は次の段に伝搬される。パイプラインの各段では、変数は事前に決定された順序で引き渡される。この方式の利点は、変数がシーケンスの位置により識別されるので、その識別を送出する必要がないことである。これにより、値の伝搬のスループットが高レベルに維持され、実装は単純となる。識別はシーケンスのカウンターと格納された値とを比較することによって実行することができる。
【００５７】
次に、本発明の方法を、図３を参照しつつ要約して説明する。前述のように、当該方法はブールＳＡＴ公式を解くためにブールＳＡＴソルバー装置を使用し、このブールＳＡＴソルバーは複数個の再構成可能なハードウェア・モジュールを備える。図３では、ステップＳ２００で、ブールＳＡＴ公式が読み取られる。次にステップ２１０では、当該方法は、ブールＳＡＴ公式を区分化し、各区分を事前に決定された各文節内の変数数に制限する。ステップＳ２２０では、複数個の再構成可能なモジュールの内部回路を回路アレーに構成する。このステップに続くステップＳ２３０では、ブールＳＡＴ公式区分を複数個の再構成可能なハードウェア・モジュールの回路アレーに割り当てる。最後に、ステップＳ２４０では、複数個の再構成可能なハードウェア・モジュールの各々の回路アレー中で、ブールＳＡＴ公式の各区分に固有な機能及び接続をプログラムする。
【００５８】
次に、上記で説明した本発明の方法の各ステップについてさらに詳細に説明する。
【００５９】
図３に示すように、ステップＳ２００では、ブールＳＡＴ公式はステップＳ２００で読み取られる。ブールＳＡＴ公式は、論理積正規形で表現される。
【００６０】
上記のように、ステップＳ２１０では、当該方法は、次にブールＳＡＴ公式を区分化し、事前に決定された各文節内の変数数に制限する。ブールＳＡＴ公式の各区分は、論理積正規形表現に区分化される。この好適な実施の形態では、各文節は３個の変数に制限される。各ブールＳＡＴ公式は、新規変数を導入することにより、多項式時間に３文節に変換することができる。本発明では、ブールＳＡＴ公式を事前に決定された各文節内の変数数に制限することにより、さまざまなサイズの文節モジュールを使用するのではなく、すべての文節に対して単一タイプの文節モジュールを使用することが可能になる。
【００６１】
次に、複数個の再構成可能なモジュールの内部回路を回路アレーに構成することに関して、さらに詳細に説明する。当該方法は、ＦＰＧＡでの使用のために、区分化された３文節用の基本テンプレートを作成する。第１のステップでは、概略設計により単一文節モジュールを設計する。この手法では、設計と実装の間に単純な対応関係が与えられる。この設計は、原点として使用される。この好適な実施の形態では、ＸＩＬＩＮＸ  Ｆｏｕｎｄａｔｉｏｎ実装ツールを使用して、ＦＰＧＡ内における当該設計の場所と経路が指定される。
【００６２】
次のステップでは、文節モジュールの整形が行われる。コンパイルされた文節モジュールは、ＦＰＧＡ全体の上に配置される。コンパイルされた文節モジュールは、多数のモジュールを１つのＦＰＧＡにタイル状に並べて配置できるように、規則正しい形であることが望ましい。ＣＬＢは再配置され、文節用の長方形のモジュールが作成される。この好適な実施の形態では、ＦＰＧＡの実際のレイアウトを編集するためのグラフィカル・ユーザー・インターフェースとして、ＥＰＩＣツールが使用される。
【００６３】
最後に、ＳＡＴテンプレートが作成される。コンパイルされた文節モジュールはＦＰＧＡ内で複製され、グローバル経路指定が回路に付加される。これにより、ＳＡＴソルバー実装のための汎用テンプレートが提供される。文節モジュールと主要な経路指定はテンプレート内で定義される。文節モジュールとパイプライン・バス間のデコーダーと相互接続は、個々の文節に基づいてプログラムされる。この汎用テンプレートは、ブールＳＡＴ公式に従ってさらにカスタマイズする必要がある。各文節モジュール内では、２つのエンティティーをカスタマイズする必要がある。これらのエンティティーとは、（１）パイプライン・バス上の変数を識別するためのコンパレーター、及び（２）パイプライン・バスへの接続、である。図５を参照すると、ＦＰＧＡ  ３０−３３がパイプライン・バス１０に接続されている。各ＦＰＧＡ  ３０−３３内には、個々のＦＰＧＡ上に実装される各文節用の文節モジュール・デコーダー  ３０Ａ−３３Ａがある。この文節モジュール・デコーダーは、文節モジュールにより実装された変数がパイプライン・バス１０上に存在している場合に、文節モジュールに対してそれを示す。
【００６４】
このステップに続くステップＳ２３０では、当該方法は、ブールＳＡＴ公式区分を複数個の再構成可能なハードウェア・モジュール内の回路アレーに割り当てる。ここでは、再構成可能なハードウェア・モジュール内の回路アレーに公式区分を割り当てるための手法として知られる標準的な手法が使用される。
【００６５】
最後に、ステップＳ２４０では、当該方法は、複数個の再構成可能なハードウェア・モジュールの各々の回路アレー内でブールＳＡＴ公式の各区分に固有な機能及び接続をプログラムする。ここでもまた、再構成可能なハードウェア・モジュール内の各公式区分に固有な機能及び接続をプログラムするための手法として知られる標準的な手法が使用される。
【００６６】
本発明の第２の実施の形態は、ブールＳＡＴソルバー・アルゴリズム及び公式をダウンロード、及び対応するブールＳＡＴ問題の解決を行うための装置である。第３の実施の形態の装置については、要約して説明する。当該装置の第１の要素は、文節モジュールである。すでに述べたように、文節モジュールはブールＳＡＴソルバー・アルゴリズムを実装する。ブールＳＡＴソルバーの実装には、ブールＳＡＴ公式の収容に必要な個数の文節モジュールが含まれる。当該装置の第２の要素は、ブールＳＡＴソルバー・アルゴリズム及びブールＳＡＴ公式を受け取り、ブールＳＡＴソルバー・アルゴリズム及び公式を１つまたは複数の文節モジュールに分配するための制御装置である。当該装置の第３の要素は、制御装置と１つまたは複数の文節モジュールを環状トポロジーに相互接続するパイプライン・バスである。この構成により、ブールＳＡＴソルバー・アルゴリズム、公式、及び変数値を制御装置と文節モジュールとの間で引き渡すことが可能になる。
【００６７】
当該装置の最後の要素は、ブールＳＡＴソルバー・アルゴリズム及び公式を制御装置にダウンロードし、そこから結果を受け取るためのホスト・コンピューターである。
【００６８】
次に、本発明の第２の実施の形態についてさらに詳細に説明する。回路トポロジーは、図４に示すような規則的な環状構成をベースとする。そのリング上には、制御装置１及び一連の要素プロセッサー（ＰＥ：  ｐｒｏｃｅｓｓｉｎｇ  ｅｌｅｍｅｎｔ）２−５が備えられる。各ＰＥは少なくとも１つの文節モジュールを有する１つのＦＰＧＡである。パイプライン・バス１０は、リング全体にまたがる。各ＰＥはパイプライン・バス１０上の１段を成すため、１本のワイヤーが横断するＦＰＧＡ境界は１つだけである。リングのサイズは、ＳＡＴ公式のサイズにより決定される。文節が多いと、必要な文節モジュールの数が増え、したがってＦＰＧＡの数も多くなる。
【００６９】
パイプライン・バス１０は、更新された変数といくつかの制御信号をＰＥ  ２−５のすべてに送出するために使用される。パイプライン・バス１０の幅は、ＦＰＧＡチップの利用可能なＩ／Ｏピンの数によって決まる。図４を参照すると、パイプライン・バス１０が幅４０ビットである場合、ＦＰＧＡチップは入力信号用として４０本のＩ／Ｏピンを使用し、次のＦＰＧＡに出力するためにさらに４０本のピンを使用している。４０ビットのバスは、３２本のデータ・ワイヤー及び８個の制御ビットから成り、１クロック・サイクル中に１６個の変数を引き渡す。信号は、一連のＤフリップ・フロップによりパイプライン化される。すべての変数データ・ビットは、冒頭の同期信号に続いて、固定順序でパイプライン・バス１０を通過する。
【００７０】
各ＦＰＧＡ内では、文節モジュールはバス上の値にアクセスすることができ、さらにはバス上の値を更新することもできる。例えば、新規の含意が作成された場合、その含意に対応するビットが１に設定される。新たに更新されたリテラルはリング内を巡るため、すべての文節が数サイクル以内にその更新を知ることができる。
【００７１】
このリング構成では、多数のボードを１つのシステムに接続できるようにすることにより、容量拡張の柔軟性が実現されている。また、大規模なシステムを数個の小規模なＳＡＴソルバーに分割することもできる。容量の拡張や、ハードウェアの複数問題への分割が可能なこの柔軟性により、ハードウェアの利用率と効率が高まる。
【００７２】
次に、制御装置１についてさらに詳細に説明する。制御装置１は、グローバル状態を維持し、環状トポロジー・パイプライン・バス１０を監視して値の変化と競合を検出する。制御装置１の機能は固定なので、１度コンパイルするだけでよい。制御装置１は、１つのＦＰＧＡを占有し、パイプライン・バス１０とホスト・コンピューター６への通信インターフェース１１の両方に接続される。ホスト・コンピューター６は、さらにＩ／Ｏ装置７、モニター８、及びメモリー１２を備える。Ｉ／Ｏ装置７、モニター８、及びメモリー１２は、バス９によってホスト・コンピューター６に接続される。
【００７３】
制御装置１の１つの機能は、ＳＡＴソルバー装置の４つの主要な状態（すなわち、分岐、含意、分析、及びバックトラック）の間の状態遷移を管理することである。制御装置１は、パイプライン・バス１０上の制御信号を、文節モジュールの演算が適切に実行されるように設定する。制御装置１は、競合する信号と値の変化に基づいて、状態の遷移を決定しなければならない。また、制御装置１は、該当する演算を実行できるように制御信号を文節モジュールに送出する必要がある。
【００７４】
制御装置１は競合を識別するために変数の値を監視し、また、新規の値が生成されたかどうかについても監視する。競合分析の間、制御装置１は、競合の先行点として識別された変数を記録する。この情報は、バックトラックの行き先を決定するため、及び新規付加文節を構築するために使用される。
【００７５】
変数の両方のリテラルが１に設定された場合、競合が生じ、競合分析とバックトラックが実行される。競合分析が必要となった場合は、どの変数が競合を生じているかを識別する必要がある。１個の変数の各リテラル・ペアは、論理積ゲートを供給して変数競合信号を生成する。これらの競合信号は、グローバル競合信号用としてワイドな論理和ゲートを供給する。この競合信号はまた、競合変数の識別を格納するための優先順位エンコーダーも供給する。制御装置１は、競合分析の起点としてこの変数をパイプライン・バス１０上に記入する。
【００７６】
分岐決定とは、未決定変数の新規の値を選択することである。競合装置１は、次に利用可能な自由変数がどれかを決定しなければならない。含意の実行中、制御装置１は、変数の両方のリテラルが０であるかどうかをチェックする。制御装置１は、上記の競合チェック用の優先順位エンコーダーと類似した優先順位エンコーダーを供給する。その後、分岐の実行中に、デコーダーにより、選択された変数に１が割り当てられる。分岐決定がなされた後、制御装置１は含意モードに切り替わる。
【００７７】
バックトラックが指示されているかどうかを判断するための分析の間、制御装置１はすべての値が解決されるまで待機する。制御装置１は、競合に至る変数割り当てを収集する。直近の割り当てがバックトラックの行き先となる。文節付加を要する場合、制御装置１はこの変数セットをホスト・コンピューター６に転送する。
【００７８】
制御装置１は終了信号を送出し、解をシフトアウトするために、ホスト・コンピューター６に接続されなければならない。バックトラックの決定のために文節付加が必要な場合、制御装置１は付加文節に関する付加情報をホスト・コンピューターに送出する。制御装置１は、付加文節モジュールの再構成を調整する。
【００７９】
次に、パイプライン・バス１０についてさらに詳細に説明する。パイプライン・バス１０は、何よりもまず、文節モジュール同士の間、及び制御装置１と文節モジュール自身との間で変数値を時間多重化方式で引き渡すことを可能にする。パイプライン・バス１０はそのほかにも、ブールＳＡＴソルバーの多数の機能を提供する。
【００８０】
次に、図６を参照しつつ、パイプライン・データ・バス・インターフェース２７についてさらに詳細に説明する。パイプライン・データ・バス・インターフェース２７は、ダウンロードされた文節に含まれるブール変数の現在の状態をパイプライン・バス１０に出力する。パイプライン・データ・バス・インターフェース２７は、現在のクロック・サイクルが文節中に１つまたはそれ以上の変数を含むかどうかを判断するためのデコーダー（図示していない）を備え、パイプライン・バス１０上に存在するブール変数を識別する。パイプライン・データ・バス・インターフェース２７はまた、ゲート出力を有する第１ゲート２１を備え、第１ゲート２１への入力はパイプライン・バス１０のデータ伝送路及び文節モジュール２０のセット信号出力に接続される。この好適な実施の形態では、この第１ゲート２１は論理和ゲートである。この第１ゲートは、各データ伝送路ごとに反復される。パイプライン・データ・バス・インターフェース２７はまた、ゲート出力を有する第２ゲート２３を備え、第２ゲート２３の入力は文節モジュール２０のリセット信号出力及び第１ゲート２１出力に接続される。この好適な実施の形態では、第２ゲート２３は論理積ゲートである。第２ゲートもまた各データ伝送路ごとに反復される。最後に、パイプライン・データ・バス・インターフェース２７はさらに、第２ゲート出力に接続されたデータ・レジスター２５を備える。パイプライン・バスの各データ伝送路には、データ・レジスターが割り当てられている。
【００８１】
次に、パイプライン・バス１０のパイプライン信号バス・インターフェース３１についてさらに詳細に説明する。パイプライン信号バス・インターフェース３１は、ダウンロードされた文節のブール変数のいずれかが更新されると信号を送り、その更新された変数をパイプライン・バス１０上に配置する。パイプライン信号バス・インターフェース３１は、ゲート出力を有するゲート３０を備え、ゲート３０の入力は、パイプライン・バス１０の更新伝送路及び文節モジュール２０からの更新信号出力に接続される。この好適な実施の形態では、ゲート３０は論理和ゲートである。パイプライン信号バス・インターフェース３１はさらに、ゲート３０の出力に接続されたデータ・レジスター２９を備える。
【００８２】
次に、文節モジュール２０の構成についてさらに詳細に説明する。文節モジュール２０は含意を計算し、ダウンロードされた文節から成るブール変数に対し競合分析を実行する。文節モジュール２０は、ＳＡＴ公式内の文節の計算タスクを実行する。文節モジュール２０は含意を計算し、競合分析を実行する。文節モジュール２０は、パイプライン・バス１０に接続されているので、パイプライン・バス１０へのインターフェースも備える。図６は、１パイプライン段の文脈における１つの文節モジュール２０を示す。文節モジュール２０は、含意または分析の実行中に、パイプライン・バス上の値をセットもしくはリセットする。図６を参照すると分かるように、各文節モジュール２０は、データ信号入力、セット信号出力、リセット信号出力、状態信号入力、及び更新信号出力から成る。
【００８３】
パイプライン・バス１０は、固定シーケンスで変数値を循環させる。文節モジュール２０は、パイプライン・バス１０上の変数を識別する。この実施の形態では、この識別はカウンター及びコンパレーターを使用して実行される。カウンターは、同一パイプライン段内の複数の文節間で共用することができる。各ＦＰＧＡは１段のパイプラインを表すので、１個のチップ上に存在するすべての文節が同一のカウンターを共用できる。カウンターは変数のシーケンスの冒頭で０にリセットされる。カウンターは、１クロック・サイクルにつき１増加する。カウンター用のビット数は、パイプライン・バス１０の幅と変数の個数によって異なる。カウンターは、特定の変数がそのパイプライン段にあるかどうかを判断するために事前に記憶された値と比較される。
【００８４】
この実施の形態では、数値が定数と比較されるので、完全なコンパレーターの必要はない。文節モジュール２０は、１つの入力ベクトルについて１を出力する単純な組み合わせゲートを必要とするだけである。この実施の形態では、ＣＬＢは９入力まで取ることができる。１入力をフラグとして使用することにより、ＣＬＢは最大２５６パイプライン段の定数チェッカーとしての役割を果たすことができる。１段で１６個の変数を処理できるるとすると、わずか１つのＣＬＢから成るコンパレーターと８ビット・カウンターで、最大４０９６変数を有するＳＡＴ公式に対応できる。
【００８５】
各段内には、多数の変数ワイヤーがある。文節モジュール２０は、その変数に該当するワイヤーに接続する必要がある。例えば、データ・ワイヤーの本数を３２本と想定すると、リテラルｖが段ｉ／１６のワイヤー（ｉｍｏｄ１６）＊２に配置され、一方、リテラルｖ’は、同じ段のワイヤー（ｉｍｏｄ１６）＊２＋１に配置される。カウンター及びチェッカーにより実行された識別により、パイプライン・データ・バス・インターフェース２７は、パイプライン・バス１０から文節モジュール２０、及び文節モジュール２０からパイプライン・バス１０の両方向で値の更新が行わなければならない。このタスクは、１組のレジスターといくつかの制御回路（図示していない）によって処理される。各文節モジュール２０は、関連の変数値を格納するための１組のローカル・レジスターを有する。これらのレジスターは、変数が利用可能になると、パイプライン・バス１０から更新される。各文節モジュール２０はさらに、パイプライン・バス１０上に置く予定の値を格納するための１組のレジスターを有している。その値は、変数がアクセス可能になると更新される。各文節モジュール２０はまた、更新信号を設定して、新規の値が表明されたことを制御装置１に通知する。
【００８６】
文節モジュール２０は、含意の実行中に、ローカル変数レジスターをチェックし、その結果に応じて新規の含意を生成する。新規の含意はその後、パイプライン・バス１０上を循環している変数値を更新する。文節モジュール２０はまた、このような含意が生成されたことを記憶しておき、この情報を分析プロセスで使用する。
【００８７】
文節モジュール２０により実行される分析プロセスは、含意プロセスの逆である。文節モジュール２０は、競合の先行点を決定する。文節モジュール２０は、競合変数の両方のリテラルを１にセットすることにより開始する。ある文節が含意を生成すると、文節モジュール２０が、この暗黙リテラルがパイプライン・バス１０上で１にセットされているかどうかをチェックする。１にセットされている場合は、分析プロセスはこのリテラルの先行点を探していることを意味する。文節モジュール２０はその後、文節内のその他のリテラルの補数を１にセットする。それは、これらの値が含意に至ったからである。暗黙リテラルはすでに対処されているので、このリテラルはパイプライン・バス１０上で０にリセットされる。このプロセスは、パイプライン・バス１０上のすべての真の値が分岐決定により決定されたときに終了する。この時点で、制御装置１は先行点セットを生成し、バックトラックの行き先を決定しなければならない。
【００８８】
本発明の第３の実施の形態は、複数個のブール変数を有するブールＳＡＴ公式を解決するための方法において実施されている。図７〜図８を参照すると分かるように、本発明はステップＳ３００で、ブールＳＡＴ公式の複数個のブール変数を既知の状態にセットする。上記のように、ブール変数はゼロにセットされる。
【００８９】
次のステップＳ３１０−Ｓ３１２では、自由変数が複数個のブール変数から選択される。自由変数とは、値をまだ割り当てられていない変数のことである。割り当て可能なブール変数が尽きると、本発明は、すべての変数が割り当てられ、ブールＳＡＴ公式が解決されたことを示す。
【００９０】
ステップＳ３２０では、本発明は、事前に決定された値を新規に選択された自由変数に割り当てる。この割り当てで、選択された変数が１にセットされる。
【００９１】
次のステップＳ３３０−Ｓ３３１では、自由変数への割り当ての論理含意が計算される。論理含意分析で競合の存在が示された場合、本発明は、ブール変数及びその割り当てに対し競合分析を実行する。割り当ての論理含意が変数の中に競合が存在することを示さない場合、次のステップでは、複数個のブール変数から使用可能な次の自由変数が選択される。
【００９２】
ステップＳ３３１で競合が存在することが示された場合、ステップＳ３４０では、自由変数の論理含意から生じた競合に対して競合分析が実行される。競合分析では、競合に至る分岐割り当てが識別される。これは、含意プロセスの逆である。２つのリテラルがいずれも暗黙であるかまたは１に割り当てられている競合変数から、競合に至った値を暗黙に示した推移先行点を検出する必要がある。この機能を付加するには、ハードウェアを追加する必要がある。文節が含意を生成すると、この事象は記憶されなければならない。分析モードでは、この記憶された含意情報は先行点を識別するために使用される。
【００９３】
例えば、文節を（ｖｉ＋ｖｊ＋ｖｋ）とすると、ｖｉ＝０の場合はｖｋ＝１がこの文節により暗黙に示される。分析モードでは、バス上にｖｋ＝１があれば、ｖｋの先行点を探していることを意味する。この文節の回路は、ｖｋをリセットし、ｖ’ｉ及びｖ’ｊをセットしなければならない。それは、この２つのリテラルが含意の原因だからである。当該分析は先行点をｖ’ｉ及びｖ’ｊとして識別することにより、処理を継続することができる。
【００９４】
真のリテラルが含意に基づいて割り当てられる場合、これらのリテラルが偽にリセットされる間にその先行点がバス上に通知される。リテラルが分岐に基づいて割り当てられる場合、そのリテラルには先行点がない。そのリテラルはバスを循環しつづける。この分析プロセスは、バス上のリテラルに値の変化が生じなくなると終了する。この時点では、分岐に基づいて割り当てられた先行点のみが、値１にセットされて循環している。これらの値を収集すると、競合に至る割り当ての集合が出来上がる。
【００９５】
本発明では、ステップ３４０の競合分析の結果を、ブールＳＡＴ公式のバックトラックのために使用する。このバックトラック・プロセスは、割り当てられた自由変数から値を得た先行の変数のバックトラックと論理含意の再開が保証されるかどうかを決定する。バックトラックの決定はまた、ブールＳＡＴ公式が解決不能であること、及び先行の変数のバックトラックが不要であることを示す。
【００９６】
先行点のリストでは、バックトラックの対象は、このリスト内の直近の割り当てとなる。基本バックトラック・アルゴリズムは直近の割り当てにバックトラックするが、このバックトラック・プロセスではそれよりもバックトラックするレベル数が多くなる傾向がある。
【００９７】
当該方法の追加のステップは、ブールＳＡＴ公式に動的文節を付加することである。競合分析の結果により、最終結果に影響を及ぼさないでアルゴリズムを高速化する冗長文節を付加することができる。例えば、ｖｍ＝０及びｖｍ＝１の両方の割り当てが競合に至る場合、当該分析は競合に至る２セットを生成する。これらをｖｉ、ｖｊ、ｖｍ及びｖｋ、ｖｌ、ｖ’ｍの２セットと想定する。２つの競合の後、新規の文節（ｖ’ｉ＋ｖ’ｊ＋ｖ’ｋ＋ｖｋ）を付加し、それら４変数のうち直近の割り当てにバックトラックすることができる。新規の文節は、他の文節上に引き出されているので、冗長である。しかしそれは、隠れた制約を明らかにする。この文節は、今後の探索空間をプルーニングするのに役立つ。
【００９８】
理解を助けるため、本発明による第３の実施の形態のプロセスを説明する図９が含められている。この図には、第３の実施の形態の方法が進行する過程のさまざまな状態が図示されている。
【００９９】
本発明の第４の実施の形態は、複数個のブール変数を有するブールＳＡＴ公式をソルバー装置によって解決する方法である。当該ソルバー装置は、複数個の要素プロセッサー、制御装置、当該複数個の要素プロセッサー及び制御装置を環状トポロジーに相互接続するパイプライン・バス、及び当該制御装置に相互接続したホスト・コンピューターを備える。
【０１００】
図１０〜図１１を参照すると分かるように、ステップＳ４００では、ホスト・コンピューターはブールＳＡＴ公式をすでに受け取っている。ブールＳＡＴ公式は、２つの装置間の電気的リンクを介して制御装置へとダウンロードされる。
【０１０１】
次のステップＳ４１０では、制御装置はダウンロードされたブールＳＡＴ公式を区分し、その区分を複数個の要素プロセッサーにロードする。ブールＳＡＴ公式の区分は上記と同様に実行される。
【０１０２】
ステップＳ４２０では、制御装置は、ブールＳＡＴ公式の複数個の変数を既知の値に初期化する。ここでは、パイプライン・バス上に置かれる各変数が初期化される。
【０１０３】
ステップＳ４３０−Ｓ４３２では、制御装置は、当該複数個のブール変数から自由変数を選択することを試みる。選択プロセスに成功した場合は、ステップＳ４４０で事前に決定された値が選択されたブール変数に割り当てられる。当該複数個のブール変数から自由変数を選択する試みが成功しなかった場合、制御装置はブールＳＡＴ公式が解決されたことを示す。
【０１０４】
次のステップＳ４５０−Ｓ４５１では、制御装置は自由変数への割り当ての論理含意を計算する。論理含意が競合を示さなかった場合、制御装置は複数個のブール変数から別の自由変数を選択し、再びそのプロセスが開始する。競合が発見された場合、競合分析がその自由変数に対して実行される。
【０１０５】
ステップＳ４６０では、制御装置は、論理含意の結果に対して競合分析を実行する。当該変数に対する競合分析は、上記と同様に実行される。
【０１０６】
ステップＳ４７０−Ｓ４７２では、制御装置は、割り当てられた自由変数から値を得た先行の変数のバックトラックを行うかどうかを判断する。バックトラックが必要であると判断された場合、先行の変数のバックトラックが実行され、ステップＳ４８０に示すように、論理含意が再び開始される。必要でないと判断された場合、制御装置はブールＳＡＴ公式が解決不能であることを示す。
【０１０７】
本明細書の中で使用される「コンピューター・システム」という用語は、少なくともメモリーとプロセッサーを備えると理解されるべきである。一般に、メモリーは同時または異なる時期に、実行可能プログラム・コードの少なくともいくつかの部分を格納し、プロセッサーはその実行可能プログラム・コードに含まれる１つまたはそれ以上の命令を実行する。「実行可能プログラム・コード」という用語と「ソフトウェア」という用語は、この説明の趣旨においては実質的に同じものを意味することは理解されるであろう。本発明を実施する上では、メモリーとプロセッサーを物理的に同じ場所に配置することは必要とされない。換言すれば、プロセッサーとメモリーは、設備の物理的に異なる部分に配置され、ときには地理的に離れた場所に配置されることさえありうると予測される。
【０１０８】
図４を参照すると分かるように、本発明は、ホスト・コンピューター６、Ｉ／Ｏ装置７、及びモニター（ビデオ表示用端末装置）８を備える、ブールＳＡＴ公式を解決するために適応されたコンピューター・システムによって実施される。コンピューター・システムはさらに、コンピューター・システムが、複数個のブール変数を有するブールＳＡＴ公式を解くための本発明のステップを実行することを可能にするように適応されたソフトウェア命令を格納するメモリー１２を備える。データ・バス９は、Ｉ／Ｏ装置７、ビデオ表示用端末装置８、及びメモリー１２を互いに接続し、さらにホスト・コンピューター６に接続する。
【０１０９】
ソフトウェア命令は、コンピューター・システムがブールＳＡＴ公式の複数個のブール変数を既知の状態にセットできるようにするように適応されている。上記のように、ブール変数はゼロにセットされる。
【０１１０】
コンピューター・システムのソフトウェア命令は次に、複数個のブール変数から自由変数を選択する。自由変数とは、値をまだ割り当てられていない変数である。割り当てに使用可能なブール変数が尽きると、コンピューター・システムはユーザーに対し、すべての変数が割り当てられ、ブールＳＡＴ公式か解決されたことを示す。
【０１１１】
自由変数が複数個のブール変数から選択されると、続いてコンピューター・システムは事前に決定された値を新規に選択された自由変数に割り当てる。この割り当てにより、選択された変数が１にセットされる。
【０１１２】
次に、コンピューター・システムは、当該自由変数への割り当ての論理含意を計算する。論理含意分析により競合が存在することが示された場合、コンピューター・システムはブール変数及びその割り当てに対して競合分析を実行する。割り当ての論理含意により変数内の競合の存在が示されなかった場合、コンピューター・システムは複数個のブール変数から使用可能な次の自由変数を選択する。
【０１１３】
論理含意の結果により競合の存在が示された場合、コンピューター・システムは、自由変数の論理含意によって示された競合に対して競合分析を実行する。
【０１１４】
コンピューター・システムは、競合分析の結果を使用して、ブールＳＡＴ公式をバックトラックする。このバックトラック・プロセスは、割り当てられた自由変数から値を得た先行の変数のバックトラックと論理含意の再開が保証されるかどうかを決定する。コンピューター・システムによるバックトラックの決定はまた、ブールＳＡＴ公式が解決不能であること、及び先行の変数のバックトラックが不要であることを示す。
【０１１５】
次に、本説明の中で使用される「コンピューター・プログラム製品」という用語について説明する。実用レベルでは、コンピューター・システムが演算を実行することを可能にするソフトウェア（下記に詳細に説明する）は、さまざまな媒体のうちいずれの媒体上にも供給することができる。さらに、本発明の手法と演算の実際の実装は、実際にはプログラム言語で記述されたステートメントである。このようなプログラム言語のステートメントがコンピューターによって実行されると、コンピューターはそのステートメントの内容に従って動作する。さらに、コンピューターが本発明に従って動作することを可能にするソフトウェアは、オリジナル・ソース・コード、アセンブリー・コード、オブジェクト・コード、機械語、前述の圧縮版または暗号化版、及びその他のあらゆる同等物を含みそれに限定されない任意の数の形態で提供することができる。
【０１１６】
本書で使用される「媒体」または「コンピューター読取り可能媒体」はディスケット、テープ、コンパクト・ディスク、集積回路、ＲＯＭ、ＣＤ、カートリッジ、通信回線による遠隔伝送、及びコンピューターによって使用可能なその他類似の媒体などであることは、当該技術に精通する当業者には明らかであろう。例えば、コンピューター・システムが本発明に従って動作することを可能にするためのソフトウェアを供給するため、サプライヤーは、ディスケットを提供することも、あるいは衛星通信、直接電話リンク、もしくはインターネットを経由して何らかの形態のソフトウェアを伝送することもできる。したがって、「コンピューター読取り可能媒体」という用語は、前述のすべてと、ソフトウェアをコンピュータに供給することのできるその他の媒体を含むことが意図される。
【０１１７】
イネーブリング・ソフトウェアは、ディスケットに「書き込む」ことも、集積回路に「格納する」ことも、通信回線によって「搬送する」ことも可能であるが、本出願の趣旨においては、コンピューター使用可能媒体はソフトウェアを「保持する」と表現されることは理解されるであろう。従って、「保持する」という用語は、上記及びソフトウェアがコンピューター使用可能媒体に関連付けられるあらゆる同等の方法を含むことが意図される。
【０１１８】
したがって、表現の簡素化のため、「プログラム製品」という用語は、上記で定義されるコンピュータ・システムが上記で識別された本発明に従って動作することを可能にする何らかの形態のソフトウェアを保持するコンピューター使用可能媒体を示すために使用される。
【０１１９】
本発明はまた、コンピューターが本発明に従い、複数個のブール変数を有するブールＳＡＴ公式を解決するための本発明のステップを実行することを可能にするソフトウェアを保持するプログラム製品において実施される。コンピューター・プログラム製品は、コンピューター・システムが、複数個のブール変数を有するブールＳＡＴ公式を解決するための本発明のステップを実行することを可能にする。ここでは、ソフトウェア命令により、コンピューターが本発明を実行することが可能になる。コンピューター読取り可能媒体はソフトウェア命令を保持する。
【０１２０】
コンピューター・プログラム製品上で実施されたソフトウェア命令は、コンピューター・システムがブールＳＡＴ公式の複数個のブール変数を既知の状態に設定することを可能にするように適応されている。上記のように、ブール変数は、ソフトウェア命令によって最初にゼロに設定される。
【０１２１】
コンピューター・プログラム製品上で実施されたソフトウェア命令は、コンピューター・システムが複数個のブール変数から自由変数を選択することを可能にする。自由変数とは、値をまだ割り当てられていない変数である。コンピューター・プログラム製品上のソフトウェア命令は、割り当てに使用可能なブール変数が尽きると、コンピューター・システムがユーザーに対し、すべての変数が割り当てられ、ブールＳＡＴ公式か解決されたことを示すことを可能にする。
【０１２２】
自由変数が複数個のブール変数から選択された場合、ソフトウェア命令は事前に決定された値を当該の新規に選択された自由変数に割り当てる。この割り当てにより、選択された変数は１にセットされる。
【０１２３】
次に、コンピューター・プログラム製品上で実施されたソフトウェア命令は、コンピューター・システムが自由変数への割り当ての論理含意を計算することを可能にする。論理含意分析により競合の存在が示された場合、ソフトウェア命令は、ブール変数及びその割り当てに対して競合分析を実行する。割り当ての論理含意により変数内の競合の存在が示されなかった場合、ソフトウェア命令はコンピューター・システムに対し、複数個のブール変数から使用可能な次の自由変数を選択するよう命令する。
【０１２４】
論理含意の結果により競合の存在が示された場合、ソフトウェア命令は、コンピューター・システムに、自由変数の論理含意によって示される競合に対して競合分析を実行させる。
【０１２５】
コンピューター・プログラム製品上のソフトウェア命令は、コンピューター・システムに、競合分析の結果を使用して、ブールＳＡＴ公式をバックトラックするよう命令する。このバックトラック・プロセスは、割り当てられた自由変数から値を得た先行の変数のバックトラックと論理含意の再開が保証されるかどうかを決定する。コンピューター・プログラム製品によるバックトラックの決定はまた、ブールＳＡＴ公式が解決不能であること、及び先行の変数によるバックトラックが不要であることを示す。
【０１２６】
本発明の好適な実施の形態に関する前述の説明は、解説及び説明の目的で提示したものである。本発明を網羅的に示したり、厳密な開示形態に限定することは意図されておらず、上記の教示に照らして、あるいは本発明の実践から、変更態様や異型を得ることが可能である。実施の形態は、本発明の原理を説明するために選ばれ、説明されたものであり、当該技術に精通する当業者は、本発明を実際に適用することにより、さまざまな実施の形態において、また意図される特定の使用に適したさまざまな変更態様において、本発明を利用することができる。
【０１２７】
以上好ましい実施の形態及び実施例をあげて本発明を説明したが、本発明は必ずしも上記実施の形態及び実施例に限定されるものではなく、その技術的思想の範囲内において様々に変形して実施することができる。
【０１２８】
【発明の効果】
以上説明したように本発明によれば、ブールＳＡＴ問題の異なるインスタンスの回路を、微細で局所的な違いを除いて同一とすることを可能にする。ブールＳＡＴ問題の各インスタンスで必要とされる増分合成及び場所と経路の指定を行うための労力は、ＳＡＴ問題を実際に解決するための時間に比較して無視できるほどにわずかなものとなる。この時間多重化機能により、文節をＳＡＴソルバー・アルゴリズムに動的に付加することが可能になる。このパイプライン・アーキテクチャーは、ほんの数本の長いワイヤーを使用し、ＦＰＧＡ境界を横断するワイヤーを排除して高度にパイプライン化することにより、高速なクロック速度を提供する。
【図面の簡単な説明】
【図１】  変数割り当て後の競合を説明する含意グラフを表す図である。
【図２】  変更された変数割り当て後の競合を説明する含意グラフを表す図である。
【図３】  ブールＳＡＴソルバーを作成するための処理を説明するフローチャートである。
【図４】  本発明の第１の実施の形態の構成を示すブロック図である。
【図５】  ＦＰＧＡがパイプライン・バスに接続された本発明の一実施の形態を示すブロック図である。
【図６】  本発明の文節モジュールの一実施の形態をさらに詳細な構成を示すブロック図である。
【図７】  ブールＳＡＴ公式を解決するための方法の処理を説明するフローチャートである。
【図８】  ブールＳＡＴ公式を解決するための方法の処理を説明するフローチャートである。
【図９】  ブールＳＡＴ公式を解決する方法の状態ダイアグラムを表す図である。
【図１０】  ブールＳＡＴ公式をダウンロードし、ブールＳＡＴソルバー装置を使用してそれを解決するための処理を説明するフローチャートである。
【図１１】  ブールＳＡＴ公式をダウンロードし、ブールＳＡＴソルバー装置を使用してそれを解決するための処理を説明するフローチャートである。
【図１２】  基本Ｄａｖｉｓ−Ｐｕｔｎａｍアルゴリズムの擬似コード・リストである。
【図１３】  基本Ｄａｖｉｓ−Ｐｕｔｎａｍアルゴリズムの処理を説明するフローチャートである。
【符号の説明】
１  制御装置
２〜５  要素プロセッサー
６  ホスト・コンピューター
７  Ｉ／Ｏ装置
８  モニター
９  データ・バス
１０  パイプライン・バス
１１  通信インターフェース
１２  メモリー
２０  文節モジュール
２１、２２  第１ゲート
２３、２４  第２ゲート
２５、２６  データ・レジスター
２７  パイプライン・データ・バス・インターフェース
２８、２９  データ・レジスター
３０〜３３  ＦＰＧＡ
３０Ａ〜３３Ａ  文節モジュール・デコーダー
３１  パイプライン信号バス・インターフェース
【図１】
0004404438.tif 000004
【図２】
0004404438.tif 000005
【図３】
0004404438.tif 000006
【図４】
0004404438.tif 000007
【図５】
0004404438.tif 000008
【図６】
0004404438.tif 000009
【図７】
0004404438.tif 000010
【図８】
0004404438.tif 000011
【図９】
0004404438.tif 000012
【図１０】
0004404438.tif 000013
【図１１】
0004404438.tif 000014
【図１２】
0004404438.tif 000015
【図１３】
0004404438.tif 000016