Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Blochinger, W., Sinz, C., Küchlin, W.: Parallel Propositional Satisfiability Checking with Distributed Dynamic Learning. Parallel Computing 29, 969–994 (2003)
Blochinger, W.: Towards Robustness in Parallel SAT Solving. In: Proc. ParCo 2005, John von Neumann Institute for Computing, pp. 301–308 (2006)
Eén, N., Sörensson, N.: An Extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004)
Gil, L., Flores, P., Silveira, L.M.: PMSat: a Parallel Version of MiniSAT. JSAT 6, 71–98 (2008)
Hamadi, Y., Jabbour, S., Sais, L.: ManySat: Solver Description. Technical Report MSR-TR-2008-83, Microsoft Research (2008)
Hyvärinen, A., Junttila, T., Niemelä, I.: Incorporating Learning in Grid-Based Randomized SAT Solving. In: Dochev, D., Pistore, M., Traverso, P. (eds.) AIMSA 2008. LNCS, vol. 5253, pp. 247–261. Springer, Heidelberg (2008)
Inoue, K., Soh, T., Ueda, S., Sasaura, Y., Banbara, M., Tamura, N.: A Competitive and Cooperative Approach to Propositional Satisfiability. Discrete Applied Mathematics 154(16), 2291–2306 (2006)
Lewis, M., Schubert, T., Becker, B.: Multithreaded SAT Solving. In: Proc. 12th Asia and South Pacific Design Automation Conference, pp. 926–931 (2007)
Plaza, S., Kountainis, I., Andraus, Z., Bertacco, V., Mudge, T.: Advanced and Insights into Parallel SAT Solving. In: Proc. 15th Int. Workshop on Logic & Synthesis (IWLS 2006), pp. 188–194 (2006)
SAT-Race 2008 Results (2008), http://baldur.iti.uka.de/sat-race-2008/results.html
Singer, D.: Parallel Resolution of the Satisfiability Problem: A Survey. In: Talbi, E.-G. (ed.) Parallel Combinatorial Optimization, ch. 5. Wiley, Chichester (2006)
Zhang, H.: On Subsumption Removal and On-the-Fly CNF Simplification. In: Bacchus, F., Walsh, T. (eds.) SAT 2005, vol. 3569, pp. 482–489. Springer, Heidelberg (2005)
Zhang, H., Bonacina, M.P., Hsiang, J.: PSATO: a Distributed Propositional Prover and Its Application to Quasigroup Problems. J. Symb. Comput. 21(4), 543–560 (1996)
Zhang, L., Malik, S.: The Quest for Efficient Boolean Satisfiability Solvers. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 17–36. Springer, Heidelberg (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ohmura, K., Ueda, K. (2009). c-sat: A Parallel SAT Solver for Clusters. In: Kullmann, O. (eds) Theory and Applications of Satisfiability Testing - SAT 2009. SAT 2009. Lecture Notes in Computer Science, vol 5584. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-02777-2_47
Download citation
DOI: https://doi.org/10.1007/978-3-642-02777-2_47
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-02776-5
Online ISBN: 978-3-642-02777-2
eBook Packages: Computer ScienceComputer Science (R0)