SATソルバzchaffのMPIによる並列化

• Item type: SIG Technical Reports(1)
• 公開日: 2004-07-30
• タイトル: SATソルバzchaffのMPIによる並列化
• タイトル / 言語: en
• タイトル: Parallelization of the SAT solver zchaff with MPI
• 言語: jpn
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_18gh
• 資源タイプ: technical report
• 著者所属: 早稲田大学大学院理工学研究科情報・ネットワーク専攻
• 著者所属: 早稲田大学大学院理工学研究科情報・ネットワーク専攻
• 著者所属: 早稲田大学大学院理工学研究科情報・ネットワーク専攻
• 著者名: 大橋, 智昭; 稲垣, 良一; 上田, 和紀
• 著者名(英): Tomoaki, Oohashi; Ryoichi, Inagaki; Kazunori, Ueda
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 本研究では高性能SATソルバzchaffをクラスタ上で効率的に並列化する手法を提案している．近年のSATソルバは変数の衝突を学習し，節として追加する事で同じ変数の衝突を起こさないようする事で，SATの探索域を大幅に削減する．本研究の手法では各ノードがそれぞれランダムに決定した探索域の探索を行い，探索の途中でそれぞれのノードが学習した結果の中で探索域削減効果の高いと思われる節を交換することで効率的な並列化を実現している．本研究で作成した並列SATソルバMPI-zchaggffは，充足可能な問題の解の発見において高い性能向上を実現し，SAT Competiton 2003のunsolved problemの解を発見できた．
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: We propose an efficient parallelization method of the high-performance SAT solver zchaff. Nowadays, most SAT solvers learn conflicts of variables and by avoiding the same conflicts of variables reduce the search space. Our method has achieved effective parallelization by exchanging lemma each computation node learned in searching its own search space. We have implemented a parallel SAT solver by using zchaff and MPI and accelerated discovery of solutions. In particular, we discovered a solution of an unsolved problem in SAT Competition 2003.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AN10463942
• 書誌情報: 情報処理学会研究報告ハイパフォーマンスコンピューティング（HPC）; 巻 2004, 号 81(2004-HPC-099), p. 25-30, 発行日 2004-07-30
• Notice: SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc.
• 出版者 / 言語: ja
• 出版者: 情報処理学会