SATソルバzchaffのMPIによる並列化 Parallelization of the SAT solver zchaff with MPI

この論文にアクセスする

この論文をさがす

著者

抄録

本研究では高性能SATソルバzchaffをクラスタ上で効率的に並列化する手法を提案している.近年のSATソルバは変数の衝突を学習し,節として追加する事で同じ変数の衝突を起こさないようする事で,SATの探索域を大幅に削減する.本研究の手法では各ノードがそれぞれランダムに決定した探索域の探索を行い,探索の途中でそれぞれのノードが学習した結果の中で探索域削減効果の高いと思われる節を交換することで効率的な並列化を実現している.本研究で作成した並列SATソルバMPI-zchaggffは,充足可能な問題の解の発見において高い性能向上を実現し,SAT Competiton 2003のunsolved problemの解を発見できた.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.

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.

収録刊行物

  • 情報処理学会研究報告ハイパフォーマンスコンピューティング(HPC)

    情報処理学会研究報告ハイパフォーマンスコンピューティング(HPC) 2004(81(2004-HPC-099)), 25-30, 2004-07-30

    一般社団法人情報処理学会

参考文献:  12件中 1-12件 を表示

各種コード

  • NII論文ID(NAID)
    110002914106
  • NII書誌ID(NCID)
    AN10463942
  • 本文言語コード
    JPN
  • 資料種別
    Technical Report
  • ISSN
    09196072
  • NDL 記事登録ID
    7065953
  • NDL 雑誌分類
    ZM13(科学技術--科学技術一般--データ処理・計算機)
  • NDL 請求記号
    Z14-1121
  • データ提供元
    CJP書誌  NDL  NII-ELS  IPSJ 
ページトップへ