Abstract
Novel search space splitting techniques have recently been successfully exploited to paralleliz Constraint Programming and Mixed Integer Programming solvers. We first show how universal hashing can be used to extend one such interesting approach to a generalized setting that goes beyond discrepancy-based search, while still retaining strong theoretical guarantees. We then explain that such static or explicit splitting approaches are not as effective in the context of parallel combinatorial search with intensive knowledge acquisition and sharing such as parallel SAT, where implicit splitting through clause sharing appears to dominate. Furthermore, we show that in a parallel setting there exists a surprising tradeoff between the well-known communication cost for knowledge sharing across multiple compute nodes and the so far neglected cost incurred by the computational load per node. We provide experimental evidence that one can successfully exploit this tradeoff and achieve reasonable speedups in parallel SAT solving beyond 16 cores.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Aigner, M., Biere, A., Kirsch, C.M., Niemetz, A., Preiner, M.: Analysis of portfolio-style parallel SAT solving on current multi-core architectures. In: POS-2013: Intl. Workshop on Pragmatics of SAT, Helsinki, Finland (2013)
Audemard, G., Hoessen, B., Jabbour, S., Lagniez, J.-M., Piette, C.: Revisiting clause exchange in parallel sat solving. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 200–213. Springer, Heidelberg (2012)
Audemard, G., Simon, L.: Predicting learnt clauses quality in modern SAT solvers. In: 21st IJCAI, Pasadena, CA, pp. 399–404 (July 2009)
Balint, A., Belov, A., Heule, M., Järvisalo, M.: SAT competition (2013)
Bellare, M., Goldreich, O., Petrank, E.: Uniform generation of NP-witnesses using an NP-oracle. Information and Computation 163(2), 510–526 (2000)
Biere, A.: Lingeling, Plingeling and Treengeling entering the SAT Competition 2013. In: Proc. of SAT Competition 2013, Univ. of Helsinki. Dept. of Computer Science Series of Publications B, vol. B-2013-1, pp. 51–52 (2013)
Bloom, B., Grove, D., Herta, B., Sabharwal, A., Samulowitz, H., Saraswat, V.: SatX10: A scalable plug&play parallel SAT framework - (tool presentation). In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 463–468. Springer, Heidelberg (2012)
Bordeaux, L., Hamadi, Y., Samulowitz, H.: Experiments with massively parallel constraint solving. In: 21st IJCAI, pp. 443–448 (2009)
Chakraborty, S., Meel, K.S., Vardi, M.Y.: A scalable and nearly uniform generator of SAT witnesses. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 608–623. Springer, Heidelberg (2013)
Chu, G., Schulte, C., Stuckey, P.J.: Confidence-based work stealing in parallel constraint programming. In: Gent, I.P. (ed.) CP 2009. LNCS, vol. 5732, pp. 226–241. Springer, Heidelberg (2009)
Ermon, S., Gomes, C., Sabharwal, A., Selman, B.: Taming the curse of dimensionality: Discrete integration by hashing and optimization. In: 30th ICML, pp. 334–342 (June 2013)
Ermon, S., Gomes, C., Sabharwal, A., Selman, B.: Low-density parity constraints for hashing-based discrete integration. In: 31st ICML (2014)
Fischetti, M., Monaci, M., Salvagnin, D.: Self-splitting of workload in parallel computation (May 2014)
Gomes, C.P., Sabharwal, A., Selman, B.: Model counting: A new strategy for obtaining good bounds. In: 21st AAAI, Boston, MA, pp. 54–61 (July 2006)
Hamadi, Y., Wintersteiger, C.M.: Seven challenges in parallel sat solving. In: 26th AAAI (2012)
Harvey, W.D., Ginsberg, M.L.: Limited discrepancy search. In: 14th IJCAI, Montreal, Canada, pp. 607–615 (August 1995)
Heule, M., Kullmann, O., Wieringa, S., Biere, A.: Cube and conquer: Guiding cdcl sat solvers by lookaheads. In: Eder, K., Lourenço, J., Shehory, O. (eds.) HVC 2011. LNCS, vol. 7261, pp. 50–65. Springer, Heidelberg (2012)
IBM ILOG. IBM ILOG CPLEX Optimization Studio 12.6 (2013)
Katsirelos, G., Sabharwal, A., Samulowitz, H., Simon, L.: Resolution and parallelizability: Barriers to the efficient parallelization of sat solvers. In: 27th AAAI (2013)
Kumar, S., Mamidala, A.R., Faraj, D., Smith, B., Blocksome, M., Cernohous, B., Miller, D., Parker, J., Ratterman, J., Heidelberger, P., Chen, D., Steinmacher-Burrow, B.: PAMI: A parallel active message interface for the Blue Gene/Q supercomputer. In: IPDPS-2012: 26th IEEE International Parallel & Distributed Processing Symposium, pp. 763–773 (2012)
Michel, L., See, A., Hentenryck, P.V.: Transparent parallelization of constraint programming. INFORMS Journal on Computing 21(3), 363–382 (2009)
Moisan, T., Gaudreault, J., Quimper, C.-G.: Parallel discrepancy-based search. In: Schulte, C. (ed.) CP 2013. LNCS, vol. 8124, pp. 30–46. Springer, Heidelberg (2013)
Moisan, T., Quimper, C.-G., Gaudreault, J.: Parallel depth-bounded discrepancy search. In: Simonis, H. (ed.) CPAIOR 2014. LNCS, vol. 8451, pp. 377–393. Springer, Heidelberg (2014)
Plaza, S.M., Markov, I.L., Bertacco, V.: Low-latency sat solving on multicore processors with priority scheduling and xor partitioning. In: International Workshop on Logic Synthesis (IWLS) (2008)
Régin, J.-C., Rezgui, M., Malapert, A.: Embarrassingly parallel search. In: Schulte, C. (ed.) CP 2013. LNCS, vol. 8124, pp. 596–610. Springer, Heidelberg (2013)
Rolf, C.C., Kuchcinski, K.: Load-balancing methods for parallel and distributed constraint solving. In: IEEE Conf. on Cluster Computing, pp. 304–309 (September 2008)
Shinano, Y., Achterberg, T., Berthold, T., Heinz, S., Koch, T.: ParaSCIP – a parallel extension of SCIP. In: Competence in High Performance Computing 2010, pp. 135–148. Springer (February 2012)
Stuckey, P.J.: Lazy clause generation: Combining the power of SAT and CP (and MIP?) solving. In: Lodi, A., Milano, M., Toth, P. (eds.) CPAIOR 2010. LNCS, vol. 6140, pp. 5–9. Springer, Heidelberg (2010)
Valiant, L.G., Vazirani, V.V.: NP is as easy as detecting unique solutions. Theoretical Comput. Sci. 47(3), 85–93 (1986)
van der Tak, P., Heule, M., Biere, A.: Concurrent cube-and-conquer - (poster presentation). In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 475–476. Springer, Heidelberg (2012)
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.: Cache performance of SAT solvers: a case study for efficient implementation of algorithms. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 287–298. Springer, Heidelberg (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Sabharwal, A., Samulowitz, H. (2014). Insights into Parallelism with Intensive Knowledge Sharing. In: O’Sullivan, B. (eds) Principles and Practice of Constraint Programming. CP 2014. Lecture Notes in Computer Science, vol 8656. Springer, Cham. https://doi.org/10.1007/978-3-319-10428-7_48
Download citation
DOI: https://doi.org/10.1007/978-3-319-10428-7_48
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-10427-0
Online ISBN: 978-3-319-10428-7
eBook Packages: Computer ScienceComputer Science (R0)