Skip to main content
SpringerLink
Log in

Parallel Satisfiability Modulo Theories

  • Chapter
  • First Online:
Handbook of Parallel Constraint Reasoning

Abstract

Satisfiability Modulo Theories (SMT) is an extension of the propositional satisfiability problem (SAT) to other, well-chosen (first-order) theories such as integers, reals, and bit-vectors. This approach currently enjoys much popularity, especially in the field of software verification, where SMT solvers have become the de facto standard tool for the discharge of verification conditions. The development of parallel SMT solvers is still in its infancy, but the first general paradigms have been established. This chapter provides an overview of the recent advances in this area, specifically algorithm portfolio, search-space partitioning, and problem decomposition techniques, and how they relate to each other in theory and practice.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 89.00
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 119.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD 169.99
Price excludes VAT (USA)
  • Durable hardcover 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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Abdulla, P.A., Bjesse, P., Eén, N.: Symbolic reachability analysis based on SAT-solvers. In: S. Graf, M.I. Schwartzbach (eds.) Tools and Algorithms for Construction and Analysis of Systems, 6th International Conference, TACAS 2000, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS 2000, Berlin, Germany, March 25 - April 2, 2000, Proceedings, Lecture Notes in Computer Science, vol. 1785, pp. 411–425. Springer (2000)

    Google Scholar 

  2. Aloul, F.A., Ramani, A., Markov, I.L., Sakallah, K.A.: Solving difficult SAT instances in the presence of symmetry. In: Proceedings of the 39th Design Automation Conference, DAC 2002, New Orleans, LA, USA, June 10-14, 2002, pp. 731–736. ACM (2002)

    Google Scholar 

  3. Alt, L., Fedyukovich, G., Hyvärinen, A.E.J., Sharygina, N.: A proof-sensitive approach for small propositional interpolants. In: A. Gurfinkel, S.A. Seshia (eds.) Verified Software: Theories, Tools, and Experiments - 7th International Conference, VSTTE 2015, San Francisco, CA, USA, July 18-19, 2015. Revised Selected Papers, Lecture Notes in Computer Science, vol. 9593, pp. 1–18. Springer (2015)

    Google Scholar 

  4. Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanovic, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: G. Gopalakrishnan, S. Qadeer (eds.) Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings, Lecture Notes in Computer Science, vol. 6806, pp. 171–177. Springer (2011)

    Google Scholar 

  5. Barrett, C., Fontaine, P., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB). www.SMT-LIB.org (2016)

  6. Benque, D., Bourton, S., Cockerton, C., Cook, B., Fisher, J., Ishtiaq, S., Piterman, N., Taylor, A.S., Vardi, M.Y.: BMA: Visual tool for modeling and analyzing biological networks. In: P. Madhusudan, S.A. Seshia (eds.) Computer Aided Verification - 24th International Conference, CAV 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings, Lecture Notes in Computer Science, vol. 7358, pp. 686–692. Springer (2012)

    Google Scholar 

  7. Biere, A.: Lingeling, Plingeling, PicoSAT and PrecoSAT at SAT Race 2010. Technical Report 10/1, Institute for Formal Models and Verification, Johannes Kepler University (2010)

    Google Scholar 

  8. Biere, A., Bloem, R. (eds.): Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings, Lecture Notes in Computer Science, vol. 8559. Springer (2014)

    Google Scholar 

  9. Bonacina, M.P.: A taxonomy of parallel strategies for deduction. Annals of Mathematics and Artificial Intelligence 29(1–4), 223–257 (2000)

    Google Scholar 

  10. Bonacina, M.P.: Combination of distributed search and multi-search in Peersmcd. d. In: Proceedings of the 1st International Joint Conference on Automated Reasoning (IJCAR 2001), Lecture Notes in Artificial Intelligence, vol. 2083, pp. 448–452. Springer (2001)

    Google Scholar 

  11. Bordeaux, L., Hamadi, Y., Samulowitz, H.: Experiments with massively parallel constraint solving. In: Proceedings of the 21st International Joint Conference on Artificial Intelligence (IJCAI 2009), pp. 443–448 (2009)

    Google Scholar 

  12. Bouton, T., Oliveira, D.C.B.D., Déharbe, D., Fontaine, P.: veriT: An open, trustable and efficient SMT-solver. In: R.A. Schmidt (ed.) Automated Deduction - CADE-22, 22nd International Conference on Automated Deduction, Montreal, Canada, August 2-7, 2009. Proceedings, Lecture Notes in Computer Science, vol. 5663, pp. 151–156. Springer (2009)

    Google Scholar 

  13. Bozzano, M., Bruttomesso, R., Cimatti, A., Junttila, T.A., Ranise, S., van Rossum, P., Sebastiani, R.: Efficient satisfiability modulo theories via delayed theory combination. In: K. Etessami, S.K. Rajamani (eds.) Computer Aided Verification, 17th International Conference, CAV 2005, Edinburgh, Scotland, UK, July 6-10, 2005, Proceedings, Lecture Notes in Computer Science, vol. 3576, pp. 335–349. Springer (2005)

    Google Scholar 

  14. Bradley, A.R.: SAT-based model checking without unrolling. In: R. Jhala, D.A. Schmidt (eds.) Verification, Model Checking, and Abstract Interpretation - 12th International Conference, VMCAI 2011, Austin, TX, USA, January 23-25, 2011. Proceedings, Lecture Notes in Computer Science, vol. 6538, pp. 70–87. Springer (2011)

    Google Scholar 

  15. Brayton, R.K., Mishchenko, A.: ABC: an academic industrial-strength verification tool. In: T. Touili, B. Cook, P.B. Jackson (eds.) Computer Aided Verification, 22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010. Proceedings, Lecture Notes in Computer Science, vol. 6174, pp. 24–40. Springer (2010)

    Google Scholar 

  16. Brummayer, R., Biere, A.: Boolector: An efficient SMT solver for bit-vectors and arrays. In: S. Kowalewski, A. Philippou (eds.) Tools and Algorithms for the Construction and Analysis of Systems, 15th International Conference, TACAS 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009. Proceedings, Lecture Notes in Computer Science, vol. 5505, pp. 174–177. Springer (2009)

    Google Scholar 

  17. Bruttomesso, R., Cimatti, A., Franzén, A., Griggio, A., Sebastiani, R.: Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis. Ann. Math. Artif. Intell. 55(1-2), 63–99 (2009)

    Google Scholar 

  18. Christ, J., Hoenicke, J., Nutz, A.: SMTInterpol: An interpolating SMT solver. In: A.F. Donaldson, D. Parker (eds.) Model Checking Software - 19th International Workshop, SPIN 2012, Oxford, UK, July 23-24, 2012. Proceedings, Lecture Notes in Computer Science, vol. 7385, pp. 248–254. Springer (2012)

    Google Scholar 

  19. Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The MathSAT5 SMT solver. In: N. Piterman, S.A. Smolka (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 19th International Conference, TACAS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings, Lecture Notes in Computer Science, vol. 7795, pp. 93–107. Springer (2013)

    Google Scholar 

  20. Cimatti, A., Sebastiani, R. (eds.): Theory and Applications of Satisfiability Testing - SAT 2012 - 15th International Conference, Trento, Italy, June 17-20, 2012. Proceedings, Lecture Notes in Computer Science, vol. 7317. Springer (2012)

    Google Scholar 

  21. Conchon, S., Déharbe, D., Heizmann, M., Weber., T.: 11th International Satisfiability Modulo Theories Competition (SMT-COMP 2016). http://smtcomp.sourceforge.net/2016/ (2016)

  22. Corzilius, F., Kremer, G., Junges, S., Schupp, S., Ábrahám, E.: SMT-RAT: an open source C++ toolbox for strategic and parallel SMT solving. In: Heule and Weaver [47], pp. 360–368

    Google Scholar 

  23. Craig, W.: Linear reasoning. a new form of the Herbrand-Gentzen theorem. J. Symb. Log. 22(3), 250–268 (1957)

    Google Scholar 

  24. Creignou, N., Berre, D.L. (eds.): Theory and Applications of Satisfiability Testing - SAT 2016 - 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings, Lecture Notes in Computer Science, vol. 9710. Springer (2016)

    Google Scholar 

  25. Dequen, G., Vander-Swalmen, P., Krajecki, M.: Toward easy parallel SAT solving. In: Proceedings of the 21st IEEE International Concerence on Tools with Artificial Intelligence (ICTAI 2009), pp. 425–432. IEEE Press (2009)

    Google Scholar 

  26. Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. Journal of the ACM 52(3), 365–473 (2005)

    Google Scholar 

  27. D’Silva, V., Kroening, D., Purandare, M., Weissenbacher, G.: Interpolant strength. In: G. Barthe, M.V. Hermenegildo (eds.) Verification, Model Checking, and Abstract Interpretation, 11th International Conference, VMCAI 2010, Madrid, Spain, January 17-19, 2010. Proceedings, Lecture Notes in Computer Science, vol. 5944, pp. 129–145. Springer (2010)

    Google Scholar 

  28. Dutertre, B.: Yices 2.2. In: Biere and Bloem [8], pp. 737–744

    Google Scholar 

  29. Dutertre, B., de Moura, L.M.: A fast linear-arithmetic solver for DPLL(T). In: T. Ball, R.B. Jones (eds.) Computer Aided Verification, 18th International Conference, CAV 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings, Lecture Notes in Computer Science, vol. 4144, pp. 81–94. Springer (2006)

    Google Scholar 

  30. Eén, N., Sörensson, N.: An extensible SAT-solver. In: E. Giunchiglia, A. Tacchella (eds.) Theory and Applications of Satisfiability Testing, 6th International Conference, SAT 2003. Santa Margherita Ligure, Italy, May 5-8, 2003 Selected Revised Papers, Lecture Notes in Computer Science, vol. 2919, pp. 502–518. Springer (2003)

    Google Scholar 

  31. Ermon, S., LeBras, R., Gomes, C.P., Selman, B., van Dover, R.B.: SMT-aided combinatorial materials discovery. In: Cimatti and Sebastiani [20], pp. 172–185

    Google Scholar 

  32. Fagerberg, R., Flamm, C., Merkle, D., Peters, P.: Exploring chemistry using SMT. In: M. Milano (ed.) Principles and Practice of Constraint Programming - 18th International Conference, CP 2012, Québec City, QC, Canada, October 8-12, 2012. Proceedings, Lecture Notes in Computer Science, vol. 7514, pp. 900–915. Springer (2012)

    Google Scholar 

  33. Gebser, M., Kaminski, R., Kaufmann, B., Schaub, T., Schnor, B.: Cluster-based ASP solving with Claspar. In: Proceedings of the 11th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR 2011), Lecture Notes in Computer Science, vol. 6645, pp. 364–369. Springer (2011)

    Google Scholar 

  34. Ghilardi, S., Ranise, S.: MCMT: A model checker modulo theories. In: J. Giesl, R. Hähnle (eds.) Automated Reasoning, 5th International Joint Conference, IJCAR 2010, Edinburgh, UK, July 16-19, 2010. Proceedings, Lecture Notes in Computer Science, vol. 6173, pp. 22–29. Springer (2010)

    Google Scholar 

  35. Giesl, J., Brockschmidt, M., Emmes, F., Frohn, F., Fuhs, C., Otto, C., Plücker, M., Schneider-Kamp, P., Ströder, T., Swiderski, S., Thiemann, R.: Proving termination of programs automatically with AProVE. In: S. Demri, D. Kapur, C. Weidenbach (eds.) Automated Reasoning - 7th International Joint Conference, IJCAR 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 19-22, 2014. Proceedings, Lecture Notes in Computer Science, vol. 8562, pp. 184–191. Springer (2014)

    Google Scholar 

  36. Gomes, C.P., Selman, B.: Algorithm portfolios. Artificial Intelligence 126(1–2), 43–62 (2001)

    Google Scholar 

  37. Gomes, C.P., Selman, B., Crato, N., Kautz, H.: Heavy-tailed phenomena in satisfiability and constraint satisfaction problems. Journal of Automated Reasoning 24(1/2), 67–100 (2000)

    Google Scholar 

  38. Gomes, C.P., Selman, B., Kautz, H.: Boosting combinatorial search through randomization. In: Proceedings of the 15th National Conference on Artificial Intelligence (AAAI 1998), pp. 431–437. AAAI Press (1998)

    Google Scholar 

  39. Grama, A., Kumar, V.: State of the art in parallel search techniques for discrete optimization problems. IEEE Transactions on Knowledge and Data Engineering 11(1), 28–34 (1999)

    Google Scholar 

  40. Gregory, P., Long, D., Fox, M., Beck, J.C.: Planning modulo theories: Extending the planning paradigm. In: L. McCluskey, B.C. Williams, J.R. Silva, B. Bonet (eds.) Proceedings of the Twenty-Second International Conference on Automated Planning and Scheduling, ICAPS 2012, Atibaia, São Paulo, Brazil, June 25-19, 2012. AAAI (2012)

    Google Scholar 

  41. Guo, L., Hamadi, Y., Jabbour, S., Sais, L.: Diversification and intensification in parallel SAT solving. In: 16th International Conference on Principles and Practice of Constraint Programming (CP 2010), Lecture Notes in Computer Science, vol. 6308, pp. 252–265. Springer (2010)

    Google Scholar 

  42. Hadarean, L., Bansal, K., Jovanovic, D., Barrett, C., Tinelli, C.: A tale of two solvers: Eager and lazy approaches to bit-vectors. In: Biere and Bloem [8], pp. 680–695

    Google Scholar 

  43. Hamadi, Y., Jabbour, S., Sais, L.: Control-based clause sharing in parallel SAT solving. In: Proceedings of the 21st International Joint Conference on Artificial Intelligence (IJCAI 2009), pp. 499–504 (2009)

    Google Scholar 

  44. Hamadi, Y., Jabbour, S., Sais, L.: ManySAT: a parallel SAT solver. Journal on Satisfiability, Boolean Modeling and Computation 6(4), 245–262 (2009)

    Google Scholar 

  45. Hamadi, Y., Marques-Silva, J., Wintersteiger, C.M.: Lazy decomposition for distributed decision procedures. In: J. Barnat, K. Heljanko (eds.) Proceedings 10th International Workshop on Parallel and Distributed Methods in verifiCation, PDMC 2011, Snowbird, Utah, USA, July 14, 2011., EPTCS, vol. 72, pp. 43–54 (2011)

    Google Scholar 

  46. Heule, M., van Maaren, H.: Look-ahead based SAT solvers. In: A. Biere, M. Heule, H. van Maaren, T. Walsh (eds.) Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 155–184. IOS Press (2009)

    Google Scholar 

  47. Heule, M., Weaver, S. (eds.): Theory and Applications of Satisfiability Testing - SAT 2015 - 18th International Conference, Austin, TX, USA, September 24-27, 2015, Proceedings, Lecture Notes in Computer Science, vol. 9340. Springer (2015)

    Google Scholar 

  48. Huang, G.: Constructing Craig interpolation formulas. In: D. Du, M. Li (eds.) Computing and Combinatorics, First Annual International Conference, COCOON ’95, Xi’an, China, August 24-26, 1995, Proceedings, Lecture Notes in Computer Science, vol. 959, pp. 181–190. Springer (1995)

    Google Scholar 

  49. Huberman, B.A., Lukose, R.M., Hogg, T.: An economics approach to hard computational problems. Science 275(5296), 51–54 (1997)

    Google Scholar 

  50. Hyvärinen, A.E.J., Junttila, T., Niemelä, I.: A distribution method for solving SAT in grids. In: Proceedings of the 9th International Conference on Theory and Applications of Satisfiability Testing (SAT 2006), Lecture Notes in Computer Science, vol. 4121, pp. 430–435. Springer (2006)

    Google Scholar 

  51. Hyvärinen, A.E.J., Junttila, T.A., Niemelä, I.: Partitioning search spaces of a randomized search. Fundam. Inform. 107(2-3), 289–311 (2011)

    Google Scholar 

  52. Hyvärinen, A.E.J., Manthey, N.: Designing scalable parallel SAT solvers. In: Cimatti and Sebastiani [20], pp. 214–227

    Google Scholar 

  53. Hyvärinen, A.E.J., Marescotti, M., Alt, L., Sharygina, N.: OpenSMT2: An SMT solver for multi-core and cloud computing. In: Creignou and Berre [24], pp. 547–553

    Google Scholar 

  54. Hyvärinen, A.E.J., Marescotti, M., Sharygina, N.: Search-space partitioning for parallelizing SMT solvers. In: Heule and Weaver [47], pp. 369–386

    Google Scholar 

  55. Inoue, K., Soh, T., Ueda, S., Sasaura, Y., Banbara, M., Tamura, N.: A competitive and cooperative approach to propositional satisfiability. Discrete Applied Mathematics 154(16), 2291–2306 (2006)

    Google Scholar 

  56. Janakiram, V.K., Agrawal, D.P., Mehrotra, R.: A randomized parallel backtracking algorithm. IEEE Transactions on Computers 37(12), 1665–1676 (1988)

    Google Scholar 

  57. Janakiram, V.K., Gehringer, E.F., Agrawal, D.P., Mehrotra, R.: A randomized parallel branch-and-bound algorithm. International Journal of Parallel Programming 17(3), 277–301 (1988)

    Google Scholar 

  58. Jonás, M., Strejcek, J.: Solving quantified bit-vector formulas using binary decision diagrams. In: Creignou and Berre [24], pp. 267–283

    Google Scholar 

  59. Kalinnik, N., Ábrahám, E., Schubert, T., Wimmer, R., Becker, B.: Exploiting different strategies for the parallelization of an SMT solver. In: M. Dietrich (ed.) Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV), Dresden, Germany, February 22-24, 2010, pp. 97–106. Fraunhofer Verlag (2010)

    Google Scholar 

  60. Kovács, L., Voronkov, A.: First-order theorem proving and Vampire. In: N. Sharygina, H. Veith (eds.) Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings, Lecture Notes in Computer Science, vol. 8044, pp. 1–35. Springer (2013)

    Google Scholar 

  61. Krajícek, J.: Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic. J. Symb. Log. 62(2), 457–486 (1997)

    Google Scholar 

  62. Krings, S., Bendisposto, J., Leuschel, M.: From failure to proof: The prob disprover for B and Event-B. In: R. Calinescu, B. Rumpe (eds.) Software Engineering and Formal Methods - 13th International Conference, SEFM 2015, York, UK, September 7-11, 2015. Proceedings, Lecture Notes in Computer Science, vol. 9276, pp. 199–214. Springer (2015)

    Google Scholar 

  63. Li, G.J., Wah, B.W.: Computational efficiency of parallel combinatorial ORTree searches. IEEE Transactions on Software Engineering 16(1), 13–31 (1990)

    Google Scholar 

  64. Luby, M., Ertel, W.: Optimal parallelization of Las Vegas algorithms. In: Proceedings of the 11th Annual Symposium on Theoretical Aspects of Computer Science (STACS 1994), Lecture Notes in Computer Science, vol. 775, pp. 463–474. Springer (1994)

    Google Scholar 

  65. Marescotti, M., Hyvärinen, A.E.J., Sharygina, N.: Clause sharing and partitioning for cloud-based SMT solving. In: C. Artho, A. Legay, D. Peled (eds.) Automated Technology for Verification and Analysis - 14th International Symposium, ATVA 2016, Chiba, Japan, October 17-20, 2016, Proceedings, Lecture Notes in Computer Science, vol. 9938, pp. 428–443 (2016)

    Google Scholar 

  66. McMillan, K.L.: Interpolation and SAT-based model checking. In: W.A. Hunt Jr., F. Somenzi (eds.) Computer Aided Verification, 15th International Conference, CAV 2003, Boulder, CO, USA, July 8-12, 2003, Proceedings, Lecture Notes in Computer Science, vol. 2725, pp. 1–13. Springer (2003)

    Google Scholar 

  67. de Moura, L.M., Bjørner, N.: Model-based theory combination. Electr. Notes Theor. Comput. Sci. 198(2), 37–49 (2008)

    Google Scholar 

  68. de Moura, L.M., Bjørner, N.: Z3: an efficient SMT solver. In: C.R. Ramakrishnan, J. Rehof (eds.) Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings, Lecture Notes in Computer Science, vol. 4963, pp. 337–340. Springer (2008)

    Google Scholar 

  69. Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Trans. Program. Lang. Syst. 1(2), 245–257 (1979)

    Google Scholar 

  70. Ohmura, K., Ueda, K.: c-sat: A parallel SAT solver for clusters. In: Proceedings of the 12th International Conference on Theory and Applications of Satisfiability Testing (SAT 2009), Lecture Notes in Computer Science, vol. 5584, pp. 524–537. Springer (2009)

    Google Scholar 

  71. Petrik, M., Zilberstein, S.: Learning parallel portfolios of algorithms. Annals of Mathematics and Artificial Intelligence 48(1-2), 85–106 (2006)

    Google Scholar 

  72. Prestwich, S., Mudambi, S.: Improved branch and bound in constraint logic programming. In: Proceedings of the 1st International Conference on Principles and Practice of Constraint Programming (CP 1995), Lecture Notes in Computer Science, vol. 976, pp. 534–548. Springer (1995)

    Google Scholar 

  73. Pudlák, P.: Lower bounds for resolution and cutting plane proofs and monotone computations. J. Symb. Log. 62(3), 981–998 (1997)

    Google Scholar 

  74. Reisenberger, C.: PBoolector: a parallel SMT solver for QF_BV by combining bit-blasting with look-ahead. Master’s thesis, Johannes Kepler Universität Linz, Linz, Austria (2014)

    Google Scholar 

  75. Rice, J.R.: The algorithm selection problem. Advances in Computers 15, 65–118 (1976)

    Google Scholar 

  76. de Salvo Braz, R., O’Reilly, C., Gogate, V., Dechter, R.: Probabilistic inference modulo theories. In: S. Kambhampati (ed.) Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence, IJCAI 2016, New York, NY, USA, 9-15 July 2016, pp. 3591–3599. IJCAI/AAAI Press (2016)

    Google Scholar 

  77. Sebastiani, R., Trentin, P.: OptiMathSAT: A tool for optimization modulo theories. In: D. Kroening, C.S. Pasareanu (eds.) Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I, Lecture Notes in Computer Science, vol. 9206, pp. 447–454. Springer (2015)

    Google Scholar 

  78. Segre, A.M., Forman, S.L., Resta, G., Wildenberg, A.: Nagging: A scalable fault-tolerant paradigm for distributed search. Artificial Intelligence 140(1/2), 71–106 (2002)

    Google Scholar 

  79. Speckenmeyer, E., Monien, B., Vornberger, O.: Superlinear speedup for parallel backtracking. In: Proceedings of the 1st international conference on Supercomputing (SC 1987), Lecture Notes in Computer Science, vol. 297, pp. 985–993. Springer (1988)

    Google Scholar 

  80. Tinelli, C., Zarba, C.G.: Combining nonstably infinite theories. J. Autom. Reasoning 34(3), 209–238 (2005)

    Google Scholar 

  81. Tung, V.X., Khanh, T.V., Ogawa, M.: raSAT: An SMT solver for polynomial constraints. In: N. Olivetti, A. Tiwari (eds.) Automated Reasoning - 8th International Joint Conference, IJCAR 2016, Coimbra, Portugal, June 27 - July 2, 2016, Proceedings, Lecture Notes in Computer Science, vol. 9706, pp. 228–237. Springer (2016)

    Google Scholar 

  82. Williams, R., Gomes, C.P., Selman, B.: Backdoors to typical case complexity. In: Proceedings of the 18th International Joint Conference on Artificial Intelligence (IJCAI 2003), pp. 1173–1178. Morgan Kaufmann (2003)

    Google Scholar 

  83. Wintersteiger, C.M., Hamadi, Y., de Moura, L.: A concurrent portfolio approach to SMT solving. In: A. Bouajjani, O. Maler (eds.) Computer Aided Verification, 21st International Conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009. Proceedings, Lecture Notes in Computer Science, vol. 5643, pp. 715–720. Springer (2009)

    Google Scholar 

  84. Yordanov, B.,Wintersteiger, C.M., Hamadi, Y., Kugler, H.: SMT-based analysis of biological computation. In: G. Brat, N. Rungta, A. Venet (eds.) NASA Formal Methods, 5th International Symposium, NFM 2013, Moffett Field, CA, USA, May 14-16, 2013. Proceedings, Lecture Notes in Computer Science, vol. 7871, pp. 78–92. Springer (2013)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Università della Svizzera italiana, Lugano, Switzerland

    Antti E. J. Hyvärinen

  2. Microsoft Research, 21 Station Rd, Cambridge, CB1 2FB, UK

    Christoph M. Wintersteiger

Authors
  1. Antti E. J. Hyvärinen
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Christoph M. Wintersteiger
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Antti E. J. Hyvärinen .

Editor information

Editors and Affiliations

  1. Laboratoire d'informatique (LIX) de l'École polytechnique, Palaiseau, France

    Youssef Hamadi

  2. CRIL, CNRS UMR 8188, Université d'Artois, Lens, France

    Lakhdar Sais

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer International Publishing AG, part of Springer Nature

About this chapter

Check for updates. Verify currency and authenticity via CrossMark

Cite this chapter

Hyvärinen, A.E.J., Wintersteiger, C.M. (2018). Parallel Satisfiability Modulo Theories. In: Hamadi, Y., Sais, L. (eds) Handbook of Parallel Constraint Reasoning. Springer, Cham. https://doi.org/10.1007/978-3-319-63516-3_5

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-63516-3_5

  • Published:

  • Publisher Name: Springer, Cham

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

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

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation