Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Probabilistic Model Counting with Short XORs Kapitel lesen Erstes Kapitel lesen

2017 | OriginalPaper | Buchkapitel

A Distributed Version of Syrup

verfasst von : Gilles Audemard, Jean-Marie Lagniez, Nicolas Szczepanski, Sébastien Tabary

Erschienen in: Theory and Applications of Satisfiability Testing – SAT 2017

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

A portfolio SAT solver has to share clauses in order to be efficient. In a distributed environment, such sharing implies additional problems: more information has to be exchanged and communications among solvers can be time consuming. In this paper, we propose a new version of the state-of-the-art SAT solver Syrup that is now able to run on distributed architectures. We analyze and compare different programming models of communication. We show that, using a dedicated approach, it is possible to share many clauses without penalizing the solvers. Experiments conducted on SAT 2016 benchmarks with up to 256 cores show that our solver is very effective and outperforms other approaches. This opens a broad range of possibilities to boost parallel solvers needing to share many data.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Jetzt informieren
Vorheriges Kapitel Introducing Pareto Minimal Correction Subsets
Nächstes Kapitel PaInleSS: A Framework for Parallel SAT Solving
Literatur
1.
Aigner, M., Biere, A., Kirsch, C.M., Niemetz, A., Preiner, M.: Analysis of portfolio-style parallel SAT solving on current multi-core architectures. In: Fourth Pragmatics of SAT Workshop, a Workshop of the SAT 2013 Conference, POS 2013, pp. 28–40 (2013)
2.
Amer, A., Lu, H., Balaji, P., Matsuoka, S.: Characterizing MPI and hybrid MPI+threads applications at scale: case study with BFS. In: 15th IEEE/ACM International Symposium on Cluster, Cloud and Grid Computing, CCGrid 2015, pp. 1075–1083 (2015)
3.
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). doi:10.​1007/​978-3-642-31612-8_​16 CrossRef
4.
Audemard, G., Lagniez, J.-M., Mazure, B., Saïs, L.: On freezing and reactivating learnt clauses. In: Sakallah, K.A., Simon, L. (eds.) SAT 2011. LNCS, vol. 6695, pp. 188–200. Springer, Heidelberg (2011). doi:10.​1007/​978-3-642-21581-0_​16 CrossRef
5.
6.
Audemard, G., Simon, L.: Predicting learnt clauses quality in modern SAT solvers. In: Proceedings of the 21st International Joint Conference on Artificial Intelligence, IJCAI 2009, pp. 399–404 (2009)
7.
Audemard, G., Simon, L.: Lazy clause exchange policy for parallel SAT solvers. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 197–205. Springer, Cham (2014). doi:10.​1007/​978-3-319-09284-3_​15
8.
Balaji, P., Buntinas, D., Goodell, D., Gropp, W., Thakur, R.: Fine-grained multithreading support for hybrid threaded MPI programming. Int. J. High Perform. Comput. Appl. IJHPCA 24(1), 49–57 (2010)CrossRef
9.
10.
11.
Carribault, P., Pérache, M., Jourdren, H.: Enabling low-overhead hybrid MPI/OpenMP parallelism with MPC. In: Sato, M., Hanawa, T., Müller, M.S., Chapman, B.M., Supinski, B.R. (eds.) IWOMP 2010. LNCS, vol. 6132, pp. 1–14. Springer, Heidelberg (2010). doi:10.​1007/​978-3-642-13217-9_​1 CrossRef
12.
13.
Ehlers, T., Nowotka, D., Sieweck, P.: Communication in massively-parallel SAT solving. In: Proceedings of the 26th IEEE International Conference on Tools with Artificial Intelligence, ICTAI 2014, pp. 709–716 (2014)
14.
Franco, J., Martin, J.: A history of satisfiability, Chap.1. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 3–74. IOS Press, Amsterdam (2009)
15.
16.
Gomes, C.P., Selman, B., Kautz, H.A.: Boosting combinatorial search through randomization. In: Proceedings of the Fifteenth National Conference on Artificial Intelligence and Tenth Innovative Applications of Artificial Intelligence Conference, AAAI 1998, IAAI 1998, pp. 431–437 (1998)
17.
Grant, R.E., Skjellum, A., Bangalore, P.V.: Lightweight threading with MPI using persistent communications semantics. National Nuclear Security Administration, USA (2015)
18.
Hamadi, Y., Jabbour, S., Sais, L.: ManySat: a parallel SAT solver. J. Satisf. Boolean Model. Comput. JSAT 6(4), 245–262 (2009)MATH
19.
Heule, M.J.H., Kullmann, O., Marek, V.W.: Solving and verifying the boolean pythagorean triples problem via cube-and-conquer. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 228–245. Springer, Cham (2016). doi:10.​1007/​978-3-319-40970-2_​15
20.
Konev, B., Lisitsa, A.: A SAT attack on the Erdős discrepancy conjecture. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 219–226. Springer, Cham (2014). doi:10.​1007/​978-3-319-09284-3_​17
21.
Kshemkalyani, A.D., Singhal, M.: Efficient detection and resolution of generalized distributed deadlocks. IEEE Trans. Softw. Eng. TSE 20(1), 43–54 (1994)CrossRef
22.
Lanti, D., Manthey, N.: Sharing information in parallel search with search space partitioning. In: Nicosia, G., Pardalos, P. (eds.) LION 2013. LNCS, vol. 7997, pp. 52–58. Springer, Heidelberg (2013). doi:10.​1007/​978-3-642-44973-4_​6 CrossRef
23.
Lodha, S., Kshemkalyani, A.D.: A fair distributed mutual exclusion algorithm. IEEE Tran. Parallel Distrib. Syst. (TPDS) 11(6), 537–549 (2000)CrossRef
24.
Silva, J.P.M., Sakallah, K.A.: GRASP - a new search algorithm for satisfiability. In: Proceedings of the 1996 IEEE/ACM International Conference on Computer-aided Design, ICCAD 1996, pp. 220–227 (1996)
25.
Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient sat solver. In: Proceedings of the 38th Design Automation Conference, DAC 2001, pp. 530–535 (2001)
26.
27.
Nishio, S., Li, K.F., Manning, E.G.: A resilient mutual exclusion algorithm for computer networks. IEEE Trans. Parallel Distrib. Syst. (TPDS) 1(3), 344–356 (1990)CrossRef
28.
Pipatsrisawat, K., Darwiche, A.: A lightweight component caching scheme for satisfiability solvers. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol. 4501, pp. 294–299. Springer, Heidelberg (2007). doi:10.​1007/​978-3-540-72788-0_​28 CrossRef
29.
Singhal, M.: A taxonomy of distributed mutual exclusion. J. Parallel Distrib. Comput. 18(1), 94–101 (1993)CrossRefMATH
30.
Smith, L., Bull, M.: Development of mixed mode MPI/OpenMP applications. Sci. Program. 9(2–3), 83–98 (2001)
31.
Thakur, R., Gropp, W.: Test suite for evaluating performance of MPI implementations that support MPI_THREAD_MULTIPLE. In: Cappello, F., Herault, T., Dongarra, J. (eds.) EuroPVM/MPI 2007. LNCS, vol. 4757, pp. 46–55. Springer, Heidelberg (2007). doi:10.​1007/​978-3-540-75416-9_​13 CrossRef
32.
33.
Weigang, W., Zhang, J., Luo, A., Cao, J.: Distributed mutual exclusion algorithms for intersection traffic control. IEEE Trans. Parallel Distrib. Syst. (TPDS) 26(1), 65–74 (2015)CrossRef
34.
Zhang, L., Madigan, C., Moskewicz, M., Malik, S.: Efficient conflict driven learning in boolean satisfiability solver. In: Proceedings of the International Conference on Computer Aided Design (ICCAD), pp. 279–285 (2001)
Metadaten
Titel
A Distributed Version of Syrup
verfasst von
Gilles Audemard
Jean-Marie Lagniez
Nicolas Szczepanski
Sébastien Tabary
Copyright-Jahr
2017
Buch
Theory and Applications of Satisfiability Testing – SAT 2017

Print ISBN: 978-3-319-66262-6

Electronic ISBN: 978-3-319-66263-3

Copyright-Jahr: 2017

DOI
https://doi.org/10.1007/978-3-319-66263-3_14