Advertisement

Parallel Satisfiability Modulo Theories

  • Antti E. J. Hyvärinen
  • Christoph M. Wintersteiger
Chapter

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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [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. [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. [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. [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. [5]
    Barrett, C., Fontaine, P., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB). www.SMT-LIB.org (2016)
  6. [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. [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. [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. [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. [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. [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. [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. [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. [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. [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. [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. [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. [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. [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. [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. [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. [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–368Google Scholar
  23. [23]
    Craig, W.: Linear reasoning. a new form of the Herbrand-Gentzen theorem. J. Symb. Log. 22(3), 250–268 (1957)Google Scholar
  24. [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. [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. [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. [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. [28]
    Dutertre, B.: Yices 2.2. In: Biere and Bloem [8], pp. 737–744Google Scholar
  29. [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. [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. [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–185Google Scholar
  32. [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. [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. [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. [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. [36]
    Gomes, C.P., Selman, B.: Algorithm portfolios. Artificial Intelligence 126(1–2), 43–62 (2001)Google Scholar
  37. [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. [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. [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. [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. [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. [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–695Google Scholar
  43. [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. [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. [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. [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. [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. [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. [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. [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. [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. [52]
    Hyvärinen, A.E.J., Manthey, N.: Designing scalable parallel SAT solvers. In: Cimatti and Sebastiani [20], pp. 214–227Google Scholar
  53. [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–553Google Scholar
  54. [54]
    Hyvärinen, A.E.J., Marescotti, M., Sharygina, N.: Search-space partitioning for parallelizing SMT solvers. In: Heule and Weaver [47], pp. 369–386Google Scholar
  55. [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. [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. [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. [58]
    Jonás, M., Strejcek, J.: Solving quantified bit-vector formulas using binary decision diagrams. In: Creignou and Berre [24], pp. 267–283Google Scholar
  59. [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. [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. [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. [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. [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. [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. [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. [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. [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. [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. [69]
    Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Trans. Program. Lang. Syst. 1(2), 245–257 (1979)Google Scholar
  70. [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. [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. [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. [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. [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. [75]
    Rice, J.R.: The algorithm selection problem. Advances in Computers 15, 65–118 (1976)Google Scholar
  76. [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. [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. [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. [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. [80]
    Tinelli, C., Zarba, C.G.: Combining nonstably infinite theories. J. Autom. Reasoning 34(3), 209–238 (2005)Google Scholar
  81. [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. [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. [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. [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

Copyright information

© Springer International Publishing AG, part of Springer Nature 2018

Authors and Affiliations

  • Antti E. J. Hyvärinen
    • 1
  • Christoph M. Wintersteiger
    • 2
  1. 1.Università della Svizzera italianaLuganoSwitzerland
  2. 2.Microsoft ResearchCambridgeUK

Personalised recommendations