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

Solving Nonlinear Integer Arithmetic with MCSAT

  • Conference paper
  • First Online:
Verification, Model Checking, and Abstract Interpretation (VMCAI 2017)

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

Abstract

We present a new method for solving nonlinear integer arithmetic constraints. The method relies on the MCSat approach to solving nonlinear constraints, while using branch and bound in a conflict-directed manner. We report encouraging experimental results where the new procedure outperforms state-of-the-art SMT solvers based on bit-blasting.

The research presented in this paper has been supported by NSF grant 1528153, NASA Cooperative Agreements NNX14AI05A and NNA10DE73C, and by DARPA under agreement number FA8750-16-C-0043.

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.

    yices2 won the nonlinear categories of the 2016 SMT competition http://smtcomp.sourceforge.net/2016/.

  2. 2.

    Root isolation for univariate polynomials with integer coefficients can be done efficiently with algorithms based on Strum sequences or Descartes’ rule of signs [1].

  3. 3.

    For simplicity, we denote formulas asserted to the solver as propagations with no explanation.

  4. 4.

    By reducing the number of intervals we guarantee termination.

  5. 5.

    Available at http://yices.csl.sri.com/.

  6. 6.

    Available at http://sri-csl.github.io/libpoly/.

  7. 7.

    All benchmarks are available at http://smtlib.cs.uiowa.edu/.

  8. 8.

    For convenience, we’ve made the detailed results is available at https://docs.google.com/spreadsheets/d/1Gu9PZMvgJ6dCjwXnTdggKRUP1uI6kz6lpI2dpWEsWVU.

References

  1. Albrecht, R., Buchberger, B., Collins, G.E., Loos, R.: Computer Algebra: Symbolic and Algebraic Computation, vol. 4. Springer, Vienna (2012)

    Google Scholar 

  2. 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). doi:10.1007/978-3-642-22110-1_14

    Chapter  Google Scholar 

  3. Barrett, C., Stump, A., Tinelli, C.: The satisfiability modulo theories library (SMT-LIB), vol. 15, pp. 18–52 (2010). www.SMT-LIB.org

  4. Barrett, C.W., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories. Handb. Satisf. 185, 825–885 (2009)

    Google Scholar 

  5. Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decomposition. In: Automata Theory and Formal Languages 2nd GI Conference Kaiserslautern, 20–23 May, pp. 134–183 (1975)

    Google Scholar 

  6. 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, M., Weaver, S. (eds.) SAT 2015. LNCS, vol. 9340, pp. 360–368. Springer, Heidelberg (2015). doi:10.1007/978-3-319-24318-4_26

    Chapter  Google Scholar 

  7. de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). doi:10.1007/978-3-540-78800-3_24

    Chapter  Google Scholar 

  8. Moura, L., Jovanović, D.: A model-constructing satisfiability calculus. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 1–12. Springer, Heidelberg (2013). doi:10.1007/978-3-642-35873-9_1

    Chapter  Google Scholar 

  9. Dutertre, B.: Yices 2.2. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 737–744. Springer, Heidelberg (2014). doi:10.1007/978-3-319-08867-9_49

    Google Scholar 

  10. Dutertre, B., 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). doi:10.1007/11817963_11

    Chapter  Google Scholar 

  11. 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 

  12. Fuhs, C., Giesl, J., Middeldorp, A., Schneider-Kamp, P., Thiemann, R., Zankl, H.: SAT solving for termination analysis with polynomial interpretations. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol. 4501, pp. 340–354. Springer, Heidelberg (2007). doi:10.1007/978-3-540-72788-0_33

    Chapter  Google Scholar 

  13. Giesl, J., et al.: Proving termination of programs automatically with AProVE. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS (LNAI), vol. 8562, pp. 184–191. Springer, Heidelberg (2014). doi:10.1007/978-3-319-08587-6_13

    Google Scholar 

  14. Gomory, R.E.: Outline of an algorithm for integer solutions to linear programs. Bull. Am. Math. Soc. 64(5), 275–278 (1958)

    Article  MathSciNet  MATH  Google Scholar 

  15. Griggio, A.: A practical approach to satisfiability modulo linear integer arithmetic. J. Satisf. Boolean Model. Comput. 8, 1–27 (2012)

    MathSciNet  MATH  Google Scholar 

  16. Heizmann, M., Hoenicke, J., Podelski, A.: Software model checking for people who love automata. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 36–52. Springer, Heidelberg (2013). doi:10.1007/978-3-642-39799-8_2

    Chapter  Google Scholar 

  17. Jovanović, D.: SMT beyond DPLL(T): a new approach to theory solvers and theory combination. Ph.D. thesis, Courant Institute of Mathematical Sciences, New York (2012)

    Google Scholar 

  18. Jovanović, D., Barrett, C., De Moura, L.: The design and implementation of the model constructing satisfiability calculus. In: Formal Methods in Computer-Aided Design (FMCAD), pp. 173–180 (2013)

    Google Scholar 

  19. Jovanović, D., De Moura, L.: Solving non-linear arithmetic. In: International Joint Conference on Automated Reasoning, pp. 339–354 (2012)

    Google Scholar 

  20. Jovanović, D., De Moura, L.: Cutting to the chase: solving linear integer arithmetic. J. Autom. Reason. 51(1), 79–108 (2013)

    Article  MATH  Google Scholar 

  21. King, T.: Effective algorithms for the satisfiability of quantifier-free formulas over linear real and integer arithmetic. Ph.D. thesis, Courant Institute of Mathematical Sciences, New York (2014)

    Google Scholar 

  22. Kremer, G., Corzilius, F., Ábrahám, E.: A generalised branch-and-bound approach and its application in SAT modulo nonlinear integer arithmetic. In: Gerdt, V.P., Koepf, W., Seiler, W.M., Vorozhtsov, E.V. (eds.) CASC 2016. LNCS, vol. 9890, pp. 315–335. Springer, Heidelberg (2016). doi:10.1007/978-3-319-45641-6_21

    Chapter  Google Scholar 

  23. Leike, J., Heizmann, M.: Geometric series as nontermination arguments for linear lasso programs. In: 14th International Workshop on Termination, p. 55 (2014)

    Google Scholar 

  24. Lopes, N.P., Aksoy, L., Manquinho, V., Monteiro, J.: Optimally solving the MCM problem using pseudo-boolean satisfiability (2011)

    Google Scholar 

  25. Matiyasevich, Y.V.: Hilbert’s Tenth Problem. The MIT Press, Cambridge (1993)

    MATH  Google Scholar 

  26. Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient SAT solver. In: Proceedings of the 38th Annual Design Automation Conference, pp. 530–535 (2001)

    Google Scholar 

  27. Papadimitriou, C.H.: On the complexity of integer programming. J. ACM 28(4), 765–768 (1981)

    Article  MathSciNet  MATH  Google Scholar 

  28. Robinson, G., Wos, L.: Paramodulation and theorem-proving in first-order theories with equality. Mach. Intell. 4, 135–150 (1969)

    MathSciNet  MATH  Google Scholar 

  29. Tarski, A.: A decision method for elementary algebra and geometry. Technical report R-109, Rand Corporation (1951)

    Google Scholar 

  30. Weispfenning, V.: Quantifier elimination for real algebra - the quadratic case and beyond. Appl. Algebra Eng. Commun. Comput. 8(2), 85–101 (1997)

    Article  MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. SRI International, Menlo Park, USA

    Dejan Jovanović

Authors
  1. Dejan Jovanović
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Dejan Jovanović .

Editor information

Editors and Affiliations

  1. IRIF, Université Paris Diderot, Paris, France

    Ahmed Bouajjani

  2. VERIMAG, CNRS & Université Grenoble Alpes, Grenoble, France

    David Monniaux

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Jovanović, D. (2017). Solving Nonlinear Integer Arithmetic with MCSAT. In: Bouajjani, A., Monniaux, D. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2017. Lecture Notes in Computer Science(), vol 10145. Springer, Cham. https://doi.org/10.1007/978-3-319-52234-0_18

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-52234-0_18

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-52233-3

  • Online ISBN: 978-3-319-52234-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation