SAT ソルバ MiniSat の並列化とそのチューニング手法

• Item type: SIG Technical Reports(1)
• 公開日: 2007-08-01
• タイトル: SAT ソルバ MiniSat の並列化とそのチューニング手法
• タイトル / 言語: en
• タイトル: Parallelization of SAT Solver MiniSat and the tuning technique
• 言語: jpn
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_18gh
• 資源タイプ: technical report
• 著者所属: 早稲田大学大学院基幹理工学研究科情報理工学専攻
• 著者所属: 早稲田大学大学院理工学研究科情報・ネットワーク専攻
• 著者所属: 早稲田大学大学院理工学研究科情報・ネットワーク専攻 現在，特許庁
• 著者所属: 早稲田大学理工学術院
• 著者所属(英): en
• 著者所属(英): Waseda University
• 著者所属(英): en
• 著者所属(英): Waseda University
• 著者所属(英): en
• 著者所属(英): Waseda University
• 著者所属(英): en
• 著者所属(英): Waseda University
• 著者名: 大村, 圭; 渋谷, 健介; 稲垣, 良一; 上田, 和紀
• 著者名(英): Kei, OHMURA; Kensuke, SHIBUYA; Ryoichi, INAGAKI; Kazunori, UEDA
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 本論文では、充足可能性問題（SAT）の逐次ソルバである MiniSat の lemma 共有を用いた並列化とそのチューニング手法について述べる。SAT ソルバは特定の探索域には解がないということを lemma と呼ばれる clause として学習する。この lemma は探索木の枝刈りに非常に有効であるが、全ての lemma を各 PE 間で共有するためには膨大な通信コストがかかってしまうため、効率の良い学習と通信が必要である。lemma の渡し方や各パラメタをチューニングし、24PE のクラスタで実行したところ、逐次版では解けなかった問題のうち、27 題を新たに解くことができた。
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: This paper describes parallelization of the SAT solver MiniSat based on lemma sharing and its tuning techniques. When an SAT solver finds that a specific branch of the search space does not have a solution, it learns new clauses called lemmas. Lemmas are very useful for pruning search space. However, since sharing lemmas between PEs can take enormous communication cost, developing efficient learning and communication techniques is very important. Using parameters obtained by various experiments on lemma sharing, our parallel MiniSAT solved many more SAT competition problems than the original MiniSAT on a PC cluster with 24 PEs.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AN10463942
• 書誌情報: 情報処理学会研究報告ハイパフォーマンスコンピューティング（HPC）; 巻 2007, 号 80(2007-HPC-111), p. 31-36, 発行日 2007-08-01
• Notice: SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc.
• 出版者 / 言語: ja
• 出版者: 情報処理学会