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

PaInleSS: A Framework for Parallel SAT Solving

verfasst von : Ludovic Le Frioux, Souheib Baarir, Julien Sopena, Fabrice Kordon

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

Over the last decade, parallel SAT solving has been widely studied from both theoretical and practical aspects. There are now numerous solvers that differ by parallelization strategies, programming languages, concurrent programming, involved libraries, etc.
Hence, comparing the efficiency of the theoretical approaches is a challenging task. Moreover, the introduction of a new approach needs either a deep understanding of the existing solvers, or to start from scratch the implementation of a new tool.
We present PaInleSS: a framework to build parallel SAT solvers for many-core environments. Thanks to its genericity and modularity, it provides the implementation of basics for parallel SAT solving like clause exchanges, Portfolio and Divide-and-Conquer strategies. It also enables users to easily create their own parallel solvers based on new strategies. Our experiments show that our framework compares well with some of the best state-of-the-art solvers.

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 A Distributed Version of Syrup
Nächstes Kapitel A Propagation Rate Based Splitting Heuristic for Divide-and-Conquer Solvers
Fußnoten
1
painless.lrde.epita.fr.
 
2
The unitPropagation function implements the Boolean Constraint Propagation (BCP) procedure that forces (in cascade) the values of the variables in asserting clauses [8].
 
3
If the result is sat the global solving ends.
 
Literatur
1.
2.
Audemard, G., Simon, L.: Predicting learnt clauses quality in modern SAT solvers. In: IJCAI, vol. 9, pp. 399–404 (2009)
3.
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
4.
5.
Biere, A.: Splatz, lingeling, plingeling, treengeling, yalsat entering the SAT competition 2016. SAT COMPETITION 2016, p. 44 (2016)
6.
Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193–207. Springer, Heidelberg (1999). doi:10.​1007/​3-540-49059-0_​14 CrossRef
7.
Blochinger, W.: Towards robustness in parallel SAT solving. In: PARCO, pp. 301–308 (2005)
8.
9.
10.
11.
Eén, N., Biere, A.: Effective preprocessing in SAT through variable and clause elimination. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 61–75. Springer, Heidelberg (2005). doi:10.​1007/​11499107_​5 CrossRef
12.
Guo, L., Hamadi, Y., Jabbour, S., Sais, L.: Diversification and intensification in parallel SAT solving. In: International Conference on Principles and Practice of Constraint Programming, pp. 252–265. Springer (2010)
13.
Hamadi, Y., Jabbour, S., Sais, J.: Control-based clause sharing in parallel SAT solving. In: Hamadi, Y., Monfroy, E., Saubion, F. (eds.) Auton. Search, pp. 245–267. Springer, Heidelberg (2011)CrossRef
14.
Hamadi, Y., Jabbour, S., Sais, L.: ManySAT: a parallel SAT solver. J. Satisfiability Boolean Model. Comput. 6, 245–262 (2009)MATH
15.
Heule, M.J.H., 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). doi:10.​1007/​978-3-642-34188-5_​8 CrossRef
16.
Hyvärinen, A.E.J., Junttila, T., Niemelä, I.: A distribution method for solving SAT in grids. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 430–435. Springer, Heidelberg (2006). doi:10.​1007/​11814948_​39 CrossRef
17.
Hyvärinen, A.E.J., Junttila, T., Niemelä, I.: Partitioning search spaces of a randomized search. In: Serra, R., Cucchiara, R. (eds.) AI*IA 2009. LNCS, vol. 5883, pp. 243–252. Springer, Heidelberg (2009). doi:10.​1007/​978-3-642-10291-2_​25 CrossRef
18.
19.
Kautz, H.A., Selman, B., et al.: Planning as satisfiability. In: ECAI, vol. 92, pp. 359–363 (1992)
20.
Lazaar, N., Hamadi, Y., Jabbour, S., Sebag, M.: Cooperation control in Parallel SAT Solving: a Multi-armed Bandit Approach. Research Report RR-8070, INRIA, September 2012
21.
Liang, J.H., Ganesh, V., Poupart, P., Czarnecki, K.: Learning rate based branching heuristic for SAT solvers. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 123–140. Springer, Cham (2016). doi:10.​1007/​978-3-319-40970-2_​9
22.
Lynce, I., Marques-Silva, J.: SAT in bioinformatics: making the case with haplotype inference. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 136–141. Springer, Heidelberg (2006). doi:10.​1007/​11814948_​16 CrossRef
23.
24.
Manthey, N.: Coprocessor – a standalone SAT preprocessor. In: Tompits, H., Abreu, S., Oetsch, J., Pührer, J., Seipel, D., Umeda, M., Wolf, A. (eds.) INAP/WLP -2011. LNCS, vol. 7773, pp. 297–304. Springer, Heidelberg (2013). doi:10.​1007/​978-3-642-41524-1_​18 CrossRef
25.
Marques-Silva, J.P., Sakallah, K., et al.: GRASP: a search algorithm for propositional satisfiability. IEEE Trans. Comput. 48(5), 506–521 (1999)MathSciNetCrossRef
26.
Martins, R., Manquinho, V., Lynce, I.: Improving search space splitting for parallel SAT solving. In: IEEE International Conference on Tools with Artificial Intelligence, vol. 1, pp. 336–343. IEEE (2010)
27.
28.
Michael, M.M., Scott, M.L.: Simple, fast, and practical non-blocking and blocking concurrent queue algorithms. In: Proceedings of the Fifteenth Annual ACM Symposium on Principles of Distributed Computing, pp. 267–275. ACM (1996)
29.
Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient SAT solver. In: 38th annual Design Automation Conference, pp. 530–535. ACM (2001)
30.
31.
Schulz, S., Blochinger, W.: Cooperate and compete! a hybrid solving strategy for task-parallel SAT solving on peer-to-peer desktop grids. In: High Performance Computing and Simulation, pp. 314–323. IEEE (2010)
32.
Silva, J.P.M., Sakallah, K.A.: GRASP–a new search algorithm for satisfiability. In: IEEE/ACM International Conference on Computer-Aided Design, pp. 220–227. IEEE (1997)
33.
34.
Zhang, H., Bonacina, M.P., Hsiang, J.: PSATO: a distributed propositional prover and its application to quasigroup problems. J. Symbolic Comput. 21(4), 543–560 (1996)MathSciNetCrossRefMATH
35.
Zhang, L., Madigan, C.F., Moskewicz, M.H., Malik, S.: Efficient conflict driven learning in a boolean satisfiability solver. In: IEEE/ACM International Conference on Computer-Aided Design, pp. 279–285. IEEE Press (2001)
Metadaten
Titel
PaInleSS: A Framework for Parallel SAT Solving
verfasst von
Ludovic Le Frioux
Souheib Baarir
Julien Sopena
Fabrice Kordon
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_15