Advertisement

Parallel Satisfiability

  • Tomáš Balyo
  • Carsten Sinz
Chapter

Abstract

The propositional satisfiability problem (SAT) is one of the fundamental problems in theoretical computer science, but it also has many practical applications. Parallel algorithms for the SAT problem have been proposed and implemented since the 1990s. This chapter provides an overview of current approaches and their evolution over recent decades towards efficiently solving hard combinatorial problems on multi-core computers and clusters.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Notes

Acknowledgements

We would like to thank Wolfgang Blochinger for allowing us to use material from an unpublished draft in Section 1.3.1.

References

  1. [1]
    Arbelaez, A., Codognet, P.: Massively parallel local search for SAT. In: 2012 IEEE 24th International Conference on Tools with Artificial Intelligence. vol. 1, pp. 57–64. IEEE (2012)Google Scholar
  2. [2]
    Arbelaez, A., Hamadi, Y.: Improving parallel local search for SAT. In: International Conference on Learning and Intelligent Optimization. pp. 46–60. Springer (2011)Google Scholar
  3. [3]
    Audemard, G., Lagniez, J.M., Szczepanski, N., Tabary, S.: An adaptive parallel SAT solver. In: International Conference on Principles and Practice of Constraint Programming. pp. 30–48. Springer (2016)Google Scholar
  4. [4]
    Audemard, G., Simon, L.: Predicting learnt clauses quality in modern SAT solvers. In: International Joint Conference on Artificial Intelligence (IJCAI). vol. 9, pp. 399–404 (2009)Google Scholar
  5. [5]
    Audemard, G., Simon, L.: Lazy clause exchange policy for parallel SAT solvers. In: Theory and Applications of Satisfiability Testing (SAT), pp. 197–205. Springer (2014)Google Scholar
  6. [6]
    Balyo, T., Sanders, P., Sinz, C.: Hordesat: A massively parallel portfolio SAT solver. In: Heule, M.,Weaver, S. (eds.) Theory and Applications of Satisfiability Testing (SAT), Lecture Notes in Computer Science, vol. 9340, pp. 156–172. Springer International Publishing (2015)Google Scholar
  7. [7]
    Biere, A., Heule, M., van Maaren, H., Walsh, T.: Handbook of Satisfiability: Volume 185 Frontiers in Artificial Intelligence and Applications. IOS Press, Amsterdam, The Netherlands (2009)Google Scholar
  8. [8]
    Biere, A.: Lingeling, plingeling, picosat and precosat at SAT race 2010. In: Technical Report 10/1, FMV Reports Series, Institute for Formal Models and Verification, Johannes Kepler University (2010)Google Scholar
  9. [9]
    Biere, A.: Lingeling, plingeling and treengeling entering the SAT competition 2013. In: Proceedings of SAT Competition 2013, University of Helsinki. pp. 51–52 (2013)Google Scholar
  10. [10]
    Blochinger, W., Sinz, C., Küchlin, W.: Distributed parallel SAT checking with dynamic learning using DOTS. In: Gonzales, T. (ed.) Proc. of the IASTED Intl. Conference Parallel and Distributed Computing and Systems (PDCS 2001). pp. 396–401. ACTA Press, Anaheim, CA (Aug 2001)Google Scholar
  11. [11]
    Blochinger,W., Sinz, C., Küchlin,W.: Parallel propositional satisfiability checking with distributed dynamic learning. Parallel Computing 29(7), 969–994 (2003)Google Scholar
  12. [12]
    Blochinger, W., Westje, W., Küchlin, W., Wedeniwski, S.: ZetaSAT – boolean SATisfiability solving on desktop grids. In: IEEE International Symposium on Cluster Computing and the Grid. pp. 1079–1086 (2005)Google Scholar
  13. [13]
    Bloom, B.H.: Space/time trade-offs in hash coding with allowable errors. Communications of the ACM 13(7), 422–426 (1970)Google Scholar
  14. [14]
    Boehm, M., Speckenmeyer, E.: A fast parallel SAT-solver – efficient workload balancing. Annals of Mathematics and Artificial Intelligence 17(3-4), 381–400 (1996)Google Scholar
  15. [15]
    Chrabakh, W., Wolski, R.: GridSAT: A Chaff-based distributed SAT solver for the grid. In: Proc. of Supercomputing 03. Phoenix, Arizona, USA (2003)Google Scholar
  16. [16]
    Cook, S.A.: The complexity of theorem-proving procedures. In: ACM Symposium on Theory of Computing. pp. 151–158. ACM, New York, NY, USA (1971)Google Scholar
  17. [17]
    Davis, M., Logemann, G., Loveland, D.: A machine program for theoremproving. Communications of the ACM 5(7), 394–397 (1962)Google Scholar
  18. [18]
    Dijkstra, E.W., W.H.J.Feijen, van Gasteren, A.: Derivation of a termination detection algorithm for distributed computations. Inf. Proc. Letters 16, 217–219 (1983)Google Scholar
  19. [19]
    El Khalek, Y.A., Safar, M., El-Kharashi, M.W.: On the parallelization of sat solvers. In: Computer Engineering & Systems (ICCES), 2015 Tenth International Conference on. pp. 119–128. IEEE (2015)Google Scholar
  20. [20]
    Feldman, Y., Dershowitz, N., Hanna, Z.: Parallel multithreaded satisfiability solver: Design and implementation. Electr. Notes Theor. Comput. Sci. 128(3), 75–90 (2005)Google Scholar
  21. [21]
    Gu, J.: The multi-sat algorithm. Discrete Applied Mathematics 96-97, 111–126 (1999)Google Scholar
  22. [22]
    Guo, L., Jabbour, S., Lonlac, J., Saïs, L.: Diversification by clauses deletion strategies in portfolio parallel SAT solving. In: Tools with Artificial Intelligence (ICTAI), 2014 IEEE 26th International Conference on. pp. 701–708. IEEE (2014)Google Scholar
  23. [23]
    Hamadi, Y., Jabbour, S., Piette, C., Sais, L.: Deterministic parallel DPLL. Journal on Satisfiability, Boolean Modeling and Computation 7, 127–132 (2011)Google Scholar
  24. [24]
    Hamadi, Y., Jabbour, S., Sais, L.: Manysat: a parallel SAT solver. In: Satisfiability, Boolean Modeling and Computation. vol. 6, pp. 245–262 (2008)Google Scholar
  25. [25]
    Hamadi, Y., Jabbour, S., Sais, L.: Control-based clause sharing in parallel sat solving. In: Twenty-First International Joint Conference on Artificial Intelligence (2009)Google Scholar
  26. [26]
    Hamadi, Y., Wintersteiger, C.: Seven challenges in parallel SAT solving. AI Magazine 34(2), 99 (2013)Google Scholar
  27. [27]
    Heule, M., Manthey, N., Philipp, T.: Validating unsatisfiability results of clause sharing parallel SAT solvers. In: POS@ SAT. pp. 12–25 (2014)Google Scholar
  28. [28]
    Heule, M.J., Kullmann, O., Wieringa, S., Biere, A.: Cube and conquer: Guiding cdcl SAT solvers by lookaheads. In: Haifa Verification Conference. pp. 50–65. Springer (2011)Google Scholar
  29. [29]
    Hutter, F., Hoos, H.H., Leyton-Brown, K., Stuetzle, T.: ParamILS: an automatic algorithm configuration framework. Journal of Artificial Intelligence Research 36, 267–306 (October 2009)Google Scholar
  30. [30]
    Hyvärinen, A.E., Junttila, T., Niemelä, I.: A distribution method for solving SAT in grids. In: International Conference on Theory and Applications of Satisfiability Testing (SAT’06). pp. 430–435 (2006)Google Scholar
  31. [31]
    Järvisalo, M., Le Berre, D., Roussel, O.: The SAT 2011 Competition – Results of Phase 1 – slides. http://www.cril.univ-artois.fr/SAT11/phase1.pdf (2011), accessed: 2015-12-18
  32. [32]
    Jurkowiak, B., Li, C., Utard, G.: Parallelizing Satz using dynamic workload balancing. In: Kautz, H., Selman, B. (eds.) LICS 2001 Workshop on Theory and Applications of Satisfiability Testing (SAT 2001). Electronic Notes in Discrete Mathematics, vol. 9. Elsevier Science Publishers, Boston, MA (Jun 2001)Google Scholar
  33. [33]
    Jurkowiak, B., Li, C.M., Utard, G.: A parallelization scheme based on work stealing for a class of SAT solvers. Journal of Automated Reasoning 34(1), 73–101 (2005)Google Scholar
  34. [34]
    Katsirelos, G., Sabharwal, A., Samulowitz, H., Simon, L.: Resolution and parallelizability: Barriers to the efficient parallelization of SAT solvers. In: Proceedings of the Twenty-Seventh AAAI Conference on Artificial Intelligence, July 14-18, 2013, Bellevue, Washington, USA. (2013)Google Scholar
  35. [35]
    Kaufmann, M., Kottler, S.: Sartagnan parallel portfolio SAT solver with lockless physical clause sharing. In: Pragmatics of SAT. Citeseer (2011)Google Scholar
  36. [36]
    Kilby, P., Slaney, J., Thiébaux, S., Walsh, T.: Estimating search tree size. In: Proceedings of the 21st National Conference on Artificial Intelligence - Volume 2. pp. 1014–1019. AAAI’06, AAAI Press (2006)Google Scholar
  37. [37]
    Knuth, D.E.: Estimating the efficiency of backtrack programs. Mathematics of Computation 29(129), 121–136 (Jan 1975)Google Scholar
  38. [38]
    Kokotov, L.: Distributed SAT solver framework (1998)Google Scholar
  39. [39]
    Manolios, P., Zhang, Y.: Implementing survey propagation on graphics processing units. In: International Conference on Theory and Applications of Satisfiability Testing. pp. 311–324. Springer (2006)Google Scholar
  40. [40]
    Manthey, N.: Towards Next Generation Sequential and Parallel SAT Solvers. Ph.D. thesis, Technischen Universität Dresden, Fakultät Informatik (Jan 2014)Google Scholar
  41. [41]
    Marques-Silva, J.P., Sakallah, K.A.: GRASP: A search algorithm for propositional satisfiability. IEEE Transactions on Computers 48(5), 506–521 (1999)Google Scholar
  42. [42]
    Pham, D.N., Gretton, C.: gnovelty+ (v. 2). In: Proceedings of SAT Competition 2009, Artois University. pp. 9–10 (2009)Google Scholar
  43. [43]
    Roli, A., Blesa, M., Blum, C.: Random walk and parallelism in local search. In: Proceedings of MIC’2005 – Meta–heuristics International Conference. Vienna, Austria (2005)Google Scholar
  44. [44]
    Roli, A.: Criticality and parallelism in structured SAT instances. In: International Conference on Principles and Practice of Constraint Programming. pp. 714–719. Springer (2002)Google Scholar
  45. [45]
    Roussel, O.: Description of ppfolio 2012. Proc. SAT Challenge p. 46 (2012)Google Scholar
  46. [46]
    Schubert, T., Lewis, M., Becker, B.: PaMira - a parallel SAT solver with knowledge sharing. In: 6th International Workshop on Microprocessor Test and Verification (2005)Google Scholar
  47. [47]
    Schubert, T., Lewis, M.D.T., Becker, B.: Pamiraxt: Parallel SAT solving with threads and message passing. JSAT 6(4), 203–222 (2009)Google Scholar
  48. [48]
    Selman, B., Kautz, H.A., Cohen, B.: Noise strategies for improving local search. In: AAAI. vol. 94, pp. 337–343 (1994)Google Scholar
  49. [49]
    Selman, B., Levesque, H.J., Mitchell, D.G., et al.: A new method for solving hard satisfiability problems. In: AAAI. vol. 92, pp. 440–446 (1992)Google Scholar
  50. [50]
    Sinz, C., Blochinger, W., Küchlin, W.: PaSAT - parallel SAT-checking with lemma exchange: Implementation and applications. In: Kautz, H., Selman, B. (eds.) LICS 2001 Workshop on Theory and Applications of Satisfiability Testing (SAT 2001). Electronic Notes in Discrete Mathematics, vol. 9. Elsevier Science Publishers, Boston, MA (Jun 2001)Google Scholar
  51. [51]
    Sonobe, T., Inaba, M.: Counter implication restart for parallel SAT solvers. In: Learning and Intelligent Optimization, pp. 485–490. Springer (2012)Google Scholar
  52. [52]
    Sonobe, T., Inaba, M.: Portfolio with block branching for parallel SAT solvers. In: International Conference on Learning and Intelligent Optimization. pp. 247–252. Springer (2013)Google Scholar
  53. [53]
    Sonobe, T., Kondoh, S., Inaba, M.: Community branching for parallel portfolio SAT solvers. In: International Conference on Theory and Applications of Satisfiability Testing. pp. 188–196. Springer (2014)Google Scholar
  54. [54]
    Sorensson, N., Een, N.: Minisat v1.13 a SAT solver with conflict-clause minimization. Tech. rep., Chalmers University of Technology, Sweden (2005)Google Scholar
  55. [55]
    Speckenmeyer, E., Monien, B., Vornberger, O.: Superlinear speedup for parallel backtracking, pp. 985–993. Springer Berlin Heidelberg, Berlin, Heidelberg (1988)Google Scholar
  56. [56]
    Strohmaier, A.: Multi-flip networks: parallelizing gensat. In: Annual Conference on Artificial Intelligence. pp. 349–360. Springer (1997)Google Scholar
  57. [57]
    Xu, L., Hoos, H., Leyton-Brown, K.: Hydra: Automatically configuring algorithms for portfolio-based selection. AAAI Conference on Artificial Intelligence (2010)Google Scholar
  58. [58]
    Zhang, H., Bonacina, M.P.: Cumulating search in a distributed computing environment: A case study in parallel satisfiability. In: Proc. of the First Int. Symp. on Parallel Symbolic Computation. pp. 422–431. Linz, Austria (1994)Google Scholar
  59. [59]
    Zhang, H., Bonacina, M.P., Hsiang, J.: PSATO: A distributed propositional prover and its application to quasigroup problems. Journal of Symbolic Computation 21, 543–560 (1996)Google Scholar

Copyright information

© Springer International Publishing AG, part of Springer Nature 2018

Authors and Affiliations

  1. 1.Karlsruhe Institute of Technology (KIT)KarlsruheGermany

Personalised recommendations