SATソルバ MiniSat の並列化とそのチューニング手法(HPC-2 : 数値解析I)
スポンサーリンク
概要
- 論文の詳細を見る
本論文では,充足可能性問題(SAT)の逐次ソルバであるMiniSatのlemma共有を用いた並列化とそのチューニング手法について述べる.SATソルバは特定の探索域には解がないということをlemmaと呼ばれるclauseとして学習する.このlemmaは探索木の枝刈りに非常に有効であるが,全てのlemmaを各PE間で共有するためには膨大な通信コストがかかってしまうため,効率の良い学習と通信が必要である.lemmaの渡し方や各パラメタをチューニングし,24PEのクラスタで実行したところ,逐次版では解けなかった問題のうち,27題を新たに解くことができた.
- 社団法人情報処理学会の論文
- 2007-08-01
著者
-
上田 和紀
早稲田大学理工学部情報学科
-
渋谷 健介
早稲田大学理工学研究科
-
大村 圭
早稲田大学大学院基幹理工学研究科情報理工学専攻
-
稲垣 良一
早稲田大学大学院理工学研究科情報・ネットワーク専攻
-
上田 和紀
早稲田大学大学院情報理工学専攻
-
稲垣 良一
早稲田大学大学院理工学研究科情報・ネットワーク専攻:(現)特許庁
-
上田 和紀
早稲田大学
関連論文
- 並列計算機システムFOLON上へのPVMの移植と評価
- 階層グラフ書換え言語における並行プロセスの型推論
- 双対モデリングを用いた充足可能性問題のCNF encoding
- 微分制約論理式によるハイブリッドシステムのモデリングと検証
- なぜソフトウェア論文を書くのは難しい(と感じる)のか
- 特集「ソフトウェア論文」の編集にあたって
- 3A-1 大規模メモリ環境下におけるモデル検査ツールSpinのマルチコア検証機能の性能評価(高性能計算,一般セッション,アーキテクチャ)
- 3A-2 強連結成分ベースのグラフ分割による分散並列LTLモデル検査の高速化(高性能計算,一般セッション,アーキテクチャ)
- 6ZJ-9 階層グラフ書換え言語LMNtalによるモデル検査(情報爆発時代における並列分散処理技術,学生セッション,「情報爆発」時代に向けた新しいIT基盤技術)
- 4K-2 分散検証環境DiVinEを用いた分散LTLモデル検査アルゴリズムの性能評価(情報爆発時代における分散処理とセキュリティ,一般セッション,「情報爆発」時代に向けた新しいIT基盤技術)