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基盤技術)
• 6ZJ-7 並列SATソルバにおけるlemma共有およびプール制約伝播高速化(情報爆発時代における並列分散処理技術,学生セッション,「情報爆発」時代に向けた新しいIT基盤技術)
• SATソルバ MiniSat の並列化とそのチューニング手法(HPC-2 : 数値解析I)
• A-022 数式処理システムMathematica上における再帰除去システム(A分野:モデル・アルゴリズム・プログラミング)
• プロファイルを使用した並列LTLモデル検査のチューニング
• ハイブリッドシステムの高信頼シミュレーションのための区間に基づく制約伝播手法
• A-007 区間演算を用いたODE Solverにおける任意精度演算の導入とパラメタ最適化(モデル・アルゴリズム・プログラミング,一般論文)
• ハイブリッドシステムの高信頼シミュレーションのための区間に基づく制約伝播手法
• LMNtalモデル検査器における状態爆発対策(高信頼化,2010年並列/分散/協調処理に関する『金沢』サマー・ワークショップSWoPP2010)
• 強連結成分の特性を用いた並列モデル検査アルゴリズムSCC-OWCTYの設計と評価(高信頼化,2010年並列/分散/協調処理に関する『金沢』サマー・ワークショップSWoPP2010)
• ソフトウェア論文座談会
• 階層グラフ書換え言語LMNtalの処理系(ソフトウェア論文)
• LMNtal処理系および他言語インタフェースの設計と実装
• 制約に基づく解析による並行論理プログラムの自動デバッグ
• 6K-4 LMNtal処理系SLIMのモデル検査機能の並列化(情報爆発時代における並列分散処理技術,一般セッション,「情報爆発」時代に向けた新IT基盤技術,情報処理学会創立50周年記念(第72回)全国大会)
• 6K-2 クラスタ向け並列precosatの開発と性能評価(情報爆発時代における並列分散処理技術,一般セッション,「情報爆発」時代に向けた新IT基盤技術,情報処理学会創立50周年記念(第72回)全国大会)
• 1M-1 ハイブリッドシステムモデリング言語HydLaの区間制約に基づく全解シミュレーション実行処理系(モデリング・上流設計,学生セッション,アーキテクチャ,情報処理学会創立50周年記念)
• 論理・制約プログラミングと並行計算(論理と推論技術の展開)
• 特集「論理と推論技術の展開」の編集にあたって
• 6ZJ-8 軽量なLMNtal実行時処理系SLIMの設計と実装(情報爆発時代における並列分散処理技術,学生セッション,「情報爆発」時代に向けた新しいIT基盤技術)
• 4N-2 KLICへのデータ並列処理機能の導入について
• 3K-2 汎用並列組合せ最適化パッケージの構想
• C. A. R. Hoare : Communicating Sequential Processes(20世紀の名著名論)
• シンガポール国立大学
• 私はCrusoeを使いたい(インタラクティブ・エッセイ)
• A-014 LMNtalコンパイラにおける並び替えとグループ化を用いた命令列の最適化(A分野:モデル・アルゴリズム・プログラミング)
• 並列計算機システムFOLONの通信ライブラリの設計と評価
• 見込み計算を用いたニュースリーダの応答性改善法
• 10. 21世紀COEプロジェクト「プロダクティブICTアカデミア」(21世紀卓越した情報研究拠点プログラムの目指す研究(前編))
• 21世紀COEプロジェクト「プロダクティブICTアカデミア」
• 4T-7 WWW全文検索システムVernoのアーキテクチャ
• 4T-6 WWW全文検索システムVernoのデータベース
• 分散型WWW全文収集ロボットIron33
• 学習型WWW検索エンジンVerno
• LA_003 後継関数を持つリスト型非線形再帰プログラムに対する再帰除去法(A分野:モデル・アルゴリズム・プログラミング)
• 制約プログラミングに関する日本・フランス間の研究交流
• E-026 JPドメインにおける茶筌を用いた中国語ページの抽出(E分野:自然言語)
• B-030 キャッシュヒント自動付加を用いたソフトウェア高速化(B分野:ソフトウェア)
• LA-003 LMNtal処理系におけるグラフ構造の操作機能の設計と実装(A分野:モデル・アルゴリズム・プログラミング)
• SATソルバzchaffのMPIによる並列化(HPC-1 : 並列プログラミング)(2004年並列/分散/協調処理に関する『青森』サマー・ワークショップ(SWoPP青森2004) : 研究会・連続同時開催)
• 言語モデルLMNtal
• 萩谷昌己,横森 貴共編 : DNAコンピュータ,培風館(2001)
• J. A. Robinson : A Machine-Oriented Logic Based on the Resolution Principle(20世紀の名著名論)
• インタフェースに基づく並行論理プログラム最適化コンパイラの構成法
• 人工知能とソフトウェア文化
• 並列KLIC処理系上での配列演算の最適化
• 並行論理プログラムのプログラム空間に関する考察
• 並行論理型言語における同期ポイント移動の安全性について
• 自己調整二分木の並列操作
• 4N-4 並行論理プログラム静的解析系Kimaの実装
• 3N-2 オブジェクト共有空間を利用した分散プログラミング支援フレームワーク
• 並行論理プログラムの参照数解析
• 静的解析と制約充足によるプログラム自動デバッグ
• 基数制約に対応するクラスタ向け並列SATソルバとその評価(高信頼設計,2011年並列/分散/協調処理に関する『鹿児島』サマー・ワークショップ(SWoPP鹿児島2011))
• 仮想マシン移送における移送ホストの負荷軽減手法
• 理論と実際のギャップ : 並列プログラミング (<特別論説> 情報処理最前線)
• Moded Flat GHCのモード体系
• LMNtal並列モデル検査における状態生成数削減及び高速化

もっと見る 閉じる

スポンサーリンク