[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to main content
Springer Nature Link
Log in

Clause Sharing and Partitioning for Cloud-Based SMT Solving

  • Conference paper
  • First Online:
Automated Technology for Verification and Analysis (ATVA 2016)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 9938))

  • 904 Accesses

Abstract

Satisfiability modulo theories (SMT) allows the modeling and solving of constraint problems arising from practical domains by combining well-engineered and powerful solvers for propositional satisfiability with expressive, domain-specific background theories in a natural way. The increasing popularity of SMT as a modelling approach means that the SMT solvers need to handle increasingly complex problem instances. This paper studies how SMT solvers can use cloud computing to scale to challenging problems through sharing of learned information in the form of clauses with approaches based on both divide-and-conquer and algorithm portfolios. Our initial experiments, executed on the OpenSMT2 solver, show that parallelization with clause sharing speeds up the solving of instances, on average, by a factor of four or five depending on the problem domain.

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
£29.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
GBP 19.95
Price includes VAT (United Kingdom)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
GBP 35.99
Price includes VAT (United Kingdom)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
GBP 44.99
Price includes VAT (United Kingdom)
  • 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.

    We equate x and \(\lnot \lnot x\).

  2. 2.

    http://smtlib.cs.uiowa.edu.

  3. 3.

    http://opensource.org/licenses/MIT.

  4. 4.

    http://redis.io.

  5. 5.

    http://smtlib.cs.uiowa.edu/benchmarks.shtml.

References

  1. Audemard, G., Hoessen, B., Jabbour, S., Piette, C.: Dolius: A distributed parallel SAT solving framework. In: Berre, D.L. (ed.) POS-14. EPiC Series, vol. 27, pp. 1–11. EasyChair (2014)

    Google Scholar 

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

    Chapter  Google Scholar 

  3. Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanović, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171–177. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  4. 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)

    Chapter  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  6. Dutertre, B.: Yices 2.2. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 737–744. Springer, Heidelberg (2014)

    Google Scholar 

  7. Dutertre, B., de Moura, L.: A fast linear-arithmetic solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 81–94. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

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

    MathSciNet  MATH  Google Scholar 

  9. Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Software verification with BLAST. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol. 2648, pp. 235–239. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  10. Holzmann, G.J.: Cloud-based verification of concurrent software. In: Jobstmann, B., et al. (eds.) VMCAI 2016. LNCS, vol. 9583, pp. 311–327. Springer, Heidelberg (2016). doi:10.1007/978-3-662-49122-5_15

    Chapter  Google Scholar 

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

    Article  Google Scholar 

  12. Hyvärinen, A.E.J., Junttila, T.A., 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)

    Chapter  Google Scholar 

  13. Hyvärinen, A.E.J., Marescotti, M., Alt, L., Sharygina, N.: OpenSMT2: an SMT solver for multi-core and cloud computing. In: Creignou, N., Le Berre, D., Le Berre, D., Le Berre, D., Le Berre, D., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 547–553. Springer, Heidelberg (2016). doi:10.1007/978-3-319-40970-2_35

    Chapter  Google Scholar 

  14. Hyvärinen, A.E.J., Marescotti, M., Sharygina, N.: Search-space partitioning for parallelizing SMT solvers. In: Heule, M., et al. (eds.) SAT 2015. LNCS, vol. 9340, pp. 369–386. Springer, Heidelberg (2015). doi:10.1007/978-3-319-24318-4_27

    Chapter  Google Scholar 

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

    MathSciNet  MATH  Google Scholar 

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

    Article  MathSciNet  Google Scholar 

  17. Martins, R., Manquinho, V.M., Lynce, I.: An overview of parallel SAT solving. Constraints 17(3), 304–347 (2012)

    Article  MathSciNet  MATH  Google Scholar 

  18. de Moura, L., Bjørner, N.S.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  19. Nieuwenhuis, R., Oliveras, A.: Proof-producing congruence closure. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 453–468. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  20. Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT modulo theories: from an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). J. ACM 53(6), 937–977 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  21. Palikareva, H., Cadar, C.: Multi-solver support in symbolic execution. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 53–68. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  22. Rakadjiev, E., Shimosawa, T., Mine, H., Oshima, S.: Parallel SMT solving and concurrent symbolic execution. In: 2015 IEEE TrustCom/BigDataSE/ISPA, Helsinki, Finland, August 20–22, 2015, vol. 3, pp. 17–26 (2015). http://dx.doi.org/10.1109/Trustcom.2015.608

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

    Google Scholar 

  24. Sebastiani, R., Tomasi, S.: Optimization modulo theories with linear rational costs. ACM Trans. Comput. Logic 16(2), 12:1–12:3 (2015)

    Article  MathSciNet  MATH  Google Scholar 

  25. Wintersteiger, C.M., Hamadi, Y., de Moura, L.: A concurrent portfolio approach to SMT solving. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 715–720. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  26. Yordanov, B., Wintersteiger, C.M., Hamadi, Y., Kugler, H.: SMT-based analysis of biological computation. In: Brat, G., Rungta, N., Venet, A. (eds.) NFM 2013. LNCS, vol. 7871, pp. 78–92. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

Download references

Acknowledgements

This work was financially supported by SNF project number 200021_153402.

Author information

Authors and Affiliations

  1. Università della Svizzera italiana, Lugano, Switzerland

    Matteo Marescotti, Antti E. J. Hyvärinen & Natasha Sharygina

Authors
  1. Matteo Marescotti
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Antti E. J. Hyvärinen
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Natasha Sharygina
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Matteo Marescotti .

Editor information

Editors and Affiliations

  1. AIST , Osaka, Japan

    Cyrille Artho

  2. Inria Rennes , Rennes, France

    Axel Legay

  3. Bar Ilan University , Ramat Gan, Israel

    Doron Peled

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing AG

About this paper

Cite this paper

Marescotti, M., Hyvärinen, A.E.J., Sharygina, N. (2016). Clause Sharing and Partitioning for Cloud-Based SMT Solving. In: Artho, C., Legay, A., Peled, D. (eds) Automated Technology for Verification and Analysis. ATVA 2016. Lecture Notes in Computer Science(), vol 9938. Springer, Cham. https://doi.org/10.1007/978-3-319-46520-3_27

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-46520-3_27

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-46519-7

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

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation