C-sat: A parallel SAT solver for clusters

Kei Ohmura, Kazunori Ueda

研究成果: Conference contribution

31 被引用数 (Scopus)

抄録

Parallelizing modern SAT solvers for clusters such as Beowulf is an important challenge both in terms of performance scalability and stability. This paper describes a SAT Solver c-sat, a parallelization of MiniSat using MPI. It employs a layered master-worker architecture, where the masters handle lemma exchange, deletion of redundant lemmas and the dynamic partitioning of search trees, while the workers do search using different decision heuristics and random number seeds. With careful tuning, c-sat showed good speedup over MiniSat with reasonably small communication overhead on various clusters. On an eight-node cluster with two Dual-Core Opterons on each node (32 PEs), c-sat ran at least 23 times faster than MiniSat using 31 PEs (geometric mean; at least 31 times for satisfiable problems) for 189 large-scale problems from SAT Competition and two SAT-Races.

本文言語English
ホスト出版物のタイトルTheory and Applications of Satisfiability Testing - SAT 2009 - 12th International Conference, SAT 2009, Proceedings
ページ524-537
ページ数14
DOI
出版ステータスPublished - 2009 11 9
イベント12th International Conference on Theory and Applications of Satisfiability Testing, SAT 2009 - Swansea, United Kingdom
継続期間: 2009 6 302009 7 3

出版物シリーズ

名前Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
5584 LNCS
ISSN(印刷版)0302-9743
ISSN(電子版)1611-3349

Conference

Conference12th International Conference on Theory and Applications of Satisfiability Testing, SAT 2009
国/地域United Kingdom
CitySwansea
Period09/6/3009/7/3

ASJC Scopus subject areas

  • 理論的コンピュータサイエンス
  • コンピュータ サイエンス(全般)

フィンガープリント

「C-sat: A parallel SAT solver for clusters」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル