Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

PaInleSS: A Framework for Parallel SAT Solving

  • Conference paper
  • First Online:
Theory and Applications of Satisfiability Testing – SAT 2017 (SAT 2017)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 10491))

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

Notes

  1. 1.

    painless.lrde.epita.fr.

  2. 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. 3.

    If the result is sat the global solving ends.

  4. 4.

    www.labri.fr/perso/lsimon/downloads/softwares/glucose-syrup.tgz.

  5. 5.

    www.fmv.jku.at/lingeling/lingeling-bbc-9230380-160707.tar.gz.

  6. 6.

    baldur.iti.kit.edu/hordesat/files/hordesat.zip.

  7. 7.

    baldur.iti.kit.edu/sat-race-2015/downloads/sr15bench-hard.zip.

References

  1. Audemard, G., Lagniez, J.-M., Szczepanski, N., Tabary, S.: An adaptive parallel SAT solver. In: Rueher, M. (ed.) CP 2016. LNCS, vol. 9892, pp. 30–48. Springer, Cham (2016). doi:10.1007/978-3-319-44953-1_3

    Chapter  Google Scholar 

  2. Audemard, G., Simon, L.: Predicting learnt clauses quality in modern SAT solvers. In: IJCAI, vol. 9, pp. 399–404 (2009)

    Google Scholar 

  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

    Google Scholar 

  4. Balyo, T., Sanders, P., Sinz, C.: HordeSat: a massively parallel portfolio SAT Solver. In: Heule, M., Weaver, S. (eds.) SAT 2015. LNCS, vol. 9340, pp. 156–172. Springer, Cham (2015). doi:10.1007/978-3-319-24318-4_12

    Chapter  Google Scholar 

  5. Biere, A.: Splatz, lingeling, plingeling, treengeling, yalsat entering the SAT competition 2016. SAT COMPETITION 2016, p. 44 (2016)

    Google Scholar 

  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

    Chapter  Google Scholar 

  7. Blochinger, W.: Towards robustness in parallel SAT solving. In: PARCO, pp. 301–308 (2005)

    Google Scholar 

  8. Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. Commun. ACM 5(7), 394–397 (1962)

    Article  MathSciNet  MATH  Google Scholar 

  9. Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM 7(3), 201–215 (1960)

    Article  MathSciNet  MATH  Google Scholar 

  10. 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). doi:10.1007/978-3-540-24605-3_37

    Chapter  Google Scholar 

  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

    Chapter  Google Scholar 

  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)

    Google Scholar 

  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)

    Chapter  Google Scholar 

  14. Hamadi, Y., Jabbour, S., Sais, L.: ManySAT: a parallel SAT solver. J. Satisfiability Boolean Model. Comput. 6, 245–262 (2009)

    MATH  Google Scholar 

  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

    Chapter  Google Scholar 

  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

    Chapter  Google Scholar 

  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

    Chapter  Google Scholar 

  18. Hyvärinen, A.E.J., Manthey, N.: Designing scalable parallel SAT solvers. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 214–227. Springer, Heidelberg (2012). doi:10.1007/978-3-642-31612-8_17

    Chapter  Google Scholar 

  19. Kautz, H.A., Selman, B., et al.: Planning as satisfiability. In: ECAI, vol. 92, pp. 359–363 (1992)

    Google Scholar 

  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

    Google Scholar 

  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

    Google Scholar 

  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

    Chapter  Google Scholar 

  23. Manthey, N.: Coprocessor 2.0 – a flexible CNF simplifier. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 436–441. Springer, Heidelberg (2012). doi:10.1007/978-3-642-31612-8_34

    Chapter  Google Scholar 

  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

    Chapter  Google Scholar 

  25. Marques-Silva, J.P., Sakallah, K., et al.: GRASP: a search algorithm for propositional satisfiability. IEEE Trans. Comput. 48(5), 506–521 (1999)

    Article  MathSciNet  Google Scholar 

  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)

    Google Scholar 

  27. Massacci, F., Marraro, L.: Logical cryptanalysis as a SAT problem. J. Autom. Reasoning 24(1), 165–203 (2000)

    Article  MathSciNet  MATH  Google Scholar 

  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)

    Google Scholar 

  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)

    Google Scholar 

  30. Ohmura, K., Ueda, K.: c-sat: A parallel SAT solver for clusters. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 524–537. Springer, Heidelberg (2009). doi:10.1007/978-3-642-02777-2_47

    Chapter  Google Scholar 

  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)

    Google Scholar 

  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)

    Google Scholar 

  33. Sonobe, T., Inaba, M.: Portfolio with block branching for parallel SAT solvers. In: Nicosia, G., Pardalos, P. (eds.) LION 2013. LNCS, vol. 7997, pp. 247–252. Springer, Heidelberg (2013). doi:10.1007/978-3-642-44973-4_25

    Chapter  Google Scholar 

  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)

    Article  MathSciNet  MATH  Google Scholar 

  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)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. LRDE, EPITA, Kremlin-Bicêtre, France

    Ludovic Le Frioux & Souheib Baarir

  2. Sorbonne Universités, UPMC Univ Paris 06, UMR 7606, LIP6, Paris, France

    Ludovic Le Frioux, Souheib Baarir, Julien Sopena & Fabrice Kordon

  3. CNRS, UMR 7606, LIP6, Paris, France

    Ludovic Le Frioux, Souheib Baarir, Julien Sopena & Fabrice Kordon

  4. Université Paris, Nanterre, France

    Souheib Baarir

Authors
  1. Ludovic Le Frioux
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Souheib Baarir
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Julien Sopena
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Fabrice Kordon
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Ludovic Le Frioux .

Editor information

Editors and Affiliations

  1. UNSW Sydney, Sydney, New South Wales, Australia

    Serge Gaspers

  2. University of New South Wales , Sydney, New South Wales, Australia

    Toby Walsh

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Le Frioux, L., Baarir, S., Sopena, J., Kordon, F. (2017). PaInleSS: A Framework for Parallel SAT Solving. In: Gaspers, S., Walsh, T. (eds) Theory and Applications of Satisfiability Testing – SAT 2017. SAT 2017. Lecture Notes in Computer Science(), vol 10491. Springer, Cham. https://doi.org/10.1007/978-3-319-66263-3_15

Download citation

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

  • Published:

  • Publisher Name: Springer, Cham

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

  • Online ISBN: 978-3-319-66263-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation