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.
Keywords for this software
References in zbMATH (referenced in 7 articles )
Showing results 1 to 7 of 7.
- Balyo, Tomáš; Sanders, Peter; Sinz, Carsten: HordeSat: a massively parallel portfolio SAT solver (2015)
- Caniou, Yves; Codognet, Philippe; Richoux, Florian; Diaz, Daniel; Abreu, Salvador: Large-scale parallelism for constraint-based local search: the costas array case study (2015)
- Martins, Ruben; Manquinho, Vasco; Lynce, In^es: An overview of parallel SAT solving (2012)
- Ohmura, Kei; Ueda, Kazunori: c-sat: a parallel SAT solver for clusters (2009)
- Castellini, Claudio; Giunchiglia, Enrico; Tacchella, Armando: SAT-based planning in complex domains: Concurrency, constraints and nondeterminism (2003)
- Cai, Liming; Juedes, David: Subexponential parameterized algorithms collapse the W-hierarchy (2001)
- Dubois, O.; Andre, P.; Boufkhad, Y.; Carlier, J.: SAT versus UNSAT (1996)