TY - GEN
T1 - C-sat
T2 - 12th International Conference on Theory and Applications of Satisfiability Testing, SAT 2009
AU - Ohmura, Kei
AU - Ueda, Kazunori
PY - 2009
Y1 - 2009
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=70350624361&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=70350624361&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-02777-2_47
DO - 10.1007/978-3-642-02777-2_47
M3 - Conference contribution
AN - SCOPUS:70350624361
SN - 3642027768
SN - 9783642027765
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 524
EP - 537
BT - Theory and Applications of Satisfiability Testing - SAT 2009 - 12th International Conference, SAT 2009, Proceedings
Y2 - 30 June 2009 through 3 July 2009
ER -