FPGAによるSAT問題のプリプロセッサの実現(アプリケーション)
スポンサーリンク
概要
- 論文の詳細を見る
充足可能性問題(SAT問題)は,論理式全体を真とするような変数への真偽の割り当てを求める問題である.回路検証やスケジューリングなど多くの問題がSATに変換できるため,数多くのSATソルバが構築されてきた.しかし,SAT問題はNP完全であり,その計算量は非常に大きい.計算量を減らす一つの方法として,プリプロセッサによる問題規模の削減がある.本論文ではFPGAを用いたプリプロセッサ(SatELite)の構築について述べる.論理式中の項や節の依存関係を調べることにより項や節を削除することができ,問題の探索空間を小さくすることができる.SatELiteで用いられているアルゴリズムは並列化しやすく,ハードウェア化に向いている.しかし,実際の回路から生成されたSAT問題は,非常に規模が大きく,外部メモリとのデータ転送により,性能が制約される.本システムでは,FPGA内にいくつかの節をキャッシュし,それらと他の節とを並列かつ連続的に比較する.また,比較された節は外部メモリのアクセス遅延を隠蔽するために再利用される.本システムの性能は問題規模に依存するが,大規模な問題では高い性能を達成した.
- 2011-09-19
著者
関連論文
- 幾つかの画像処理問題を用いたGPUとFPGAの性能比較(リコンフィギャラブル応用)
- FPGAグリッドを用いたHMMERの高速化 (リコンフィギャラブルシステム)
- FPGAを用いたHMMERの高速化(リコンフィギャラブル応用)
- 1H-5 モラル付き囚人のディレンマの高速計算
- FPGAを用いた繰り返し囚人のジレンマの高速計算
- 1H-4 FPGAを用いた将棋の高速計算の実現
- 1H-3 Field Programmable Gate Array による複雑適応系の計算の高速化
- 1H-2 Field Programmable Gate Array を用いた探索問題の高速化
- 1H-1 FPGAによるCPUアクセラレータ
- FPGAによるGAの計算の高速化
- FPGAを用いた全探索法による可変ブロックサイズ動き予測の実現 (リコンフィギャラブルシステム)
- FPGAを用いたCLAHEの実時間処理の実現(リコンフィギャラブル応用1)
- FPGAを用いた様々な大きさ,回転角を持つパターンの検出手法の検討(リコンフィギャラブル応用2)
- FPGAを用いた全探索法による可変ブロックサイズ動き予測の実現(リコンフィギャラブル応用1)
- FPGAを用いた回転パターンの実時間検出(応用1)
- FPGAを用いた局所的コントラスト強調の実時間処理の実現(リコンフィギャラブル応用)
- FPGAを用いた大規模な充足可能性問題の高速計算(アルゴリズム理論)
- FPGAを用いたWSATアルゴリズムの高速計算(応用技術,リコンフィギャラブルシステム論文)
- FPGAによる実時間線分抽出の実現(リコンフィギャラブル応用1)
- FPGAグリッドを用いたHMMERの高速化(数値計算)
- FPGAを用いたMean-Shiftフィルタの高速計算 (リコンフィギャラブルシステム)
- FPGAによるSAT問題のプリプロセッサの実現 (リコンフィギャラブルシステム)
- FPGAを用いたMean-Shiftフィルタの高速計算(画像処理)
- FPGAによるDP-Treeアルゴリズムを用いたステレオビジョンシステムの構築(画像処理)
- FPGAによるSAT問題のプリプロセッサの実現(アプリケーション)
- FPGAを用いたグラフカットセグメンテーションの高速化(画像処理(1))
- FPGAを用いたショートリードマッピングの高速化(FPGA応用(1),リコンフィギャラブルシステム,一般)
- FPGAを用いたグラフカットセグメンテーションの高速化