Skip to main content
Springer Nature Link
Log in

A CDCL-Style Calculus for Solving Non-linear Constraints

  • Conference paper
  • First Online:
Frontiers of Combining Systems (FroCoS 2019)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 11715))

Included in the following conference series:

Abstract

In this paper we propose a novel approach for checking satisfiability of non-linear constraints over the reals, called ksmt. The procedure is based on conflict resolution in CDCL-style calculus, using a composition of symbolical and numerical methods. To deal with the non-linear components in case of conflicts we use numerically constructed restricted linearisations. This approach covers a large number of computable non-linear real functions such as polynomials, rational or trigonometrical functions and beyond. A prototypical implementation has been evaluated on several non-linear SMT-LIB examples and the results have been compared with state-of-the-art SMT solvers.

The research leading to these results has received funding from the DFG grant WERA MU 1801/5-1 and the DFG/RFBR grant CAVER BE 1267/14-1 and 14-01-91334. This project has received funding from the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie grant agreement No 731143.

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)
eBook
USD 54.99
Price excludes VAT (USA)
Softcover Book
USD 69.99
Price excludes VAT (USA)

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

Notes

  1. 1.

    http://informatik.uni-trier.de/~brausse/ksmt.

  2. 2.

    http://irram.uni-trier.de.

  3. 3.

    ksmt-0.1.3, cvc4-1.6+gmp, z3-4.7.1+gmp, mathsat-5.5.2, yices-2.6+lpoly-1.7, dreal-v3.16.08.01, rasat-0.3.

References

  1. Benhamou, F., Granvilliers, L.: Continuous and interval constraints. In: Handbook of Constraint Programming, pp. 571–603. Elsevier (2006)

    Google Scholar 

  2. Brattka, V., Hertling, P., Weihrauch, K.: A tutorial on computable analysis. In: Cooper, S.B., Löwe, B., Sorbi, A. (eds.) New Computational Paradigms, pp. 425–491. Springer, Heidelberg (2008). https://doi.org/10.1007/978-0-387-68546-5_18

    Chapter  Google Scholar 

  3. Buchberger, B.: A theoretical basis for the reduction of polynomials to canonical forms. ACM SIGSAM Bull. 10(3), 19–29 (1976)

    Article  MathSciNet  Google Scholar 

  4. Cimatti, A., Griggio, A., Irfan, A., Roveri, M., Sebastiani, R.: Incremental linearization for satisfiability and verification modulo nonlinear arithmetic and transcendental functions. ACM Trans. Comput. Log. 19(3), 19:1–19:52 (2018)

    Article  MathSciNet  Google Scholar 

  5. Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decompostion. In: Brakhage, H. (ed.) GI-Fachtagung 1975. LNCS, vol. 33, pp. 134–183. Springer, Heidelberg (1975). https://doi.org/10.1007/3-540-07407-4_17

    Chapter  Google Scholar 

  6. de 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). https://doi.org/10.1007/978-3-642-35873-9_1

    Chapter  Google Scholar 

  7. Dolzmann, A., Sturm, T.: REDLOG: computer algebra meets computer logic. ACM SIGSAM Bull. 31(2), 2–9 (1997)

    Article  Google Scholar 

  8. Dragan, I., Korovin, K., Kovács, L., Voronkov, A.: Bound propagation for arithmetic reasoning in Vampire. In: Proceedings SYNASC 2013, pp. 169–176. IEEE (2013)

    Google Scholar 

  9. Fontaine, P., Ogawa, M., Sturm, T., To, V.K., Vu, X.T.: Wrapping computer algebra is surprisingly successful for non-linear SMT. In: SC-Square 2018, Oxford, United Kingdom, July 2018

    Google Scholar 

  10. Fränzle, M., Herde, C., Teige, T., Ratschan, S., Schubert, T.: Efficient solving of large non-linear arithmetic constraint systems with complex Boolean structure. JSAT 1(3–4), 209–236 (2007)

    MATH  Google Scholar 

  11. Gao, S., Avigad, J., Clarke, E.M.: \(\delta \)-complete decision procedures for satisfiability over the reals. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS (LNAI), vol. 7364, pp. 286–300. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-31365-3_23

    Chapter  Google Scholar 

  12. Hladík, M., Ratschan, S.: Efficient solution of a class of quantified constraints with quantifier prefix Exists-Forall. Math. Comput. Sci. 8(3–4), 329–340 (2014)

    Article  MathSciNet  Google Scholar 

  13. Jovanović, D., de Moura, L.: Solving non-linear arithmetic. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS (LNAI), vol. 7364, pp. 339–354. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-31365-3_27

    Chapter  Google Scholar 

  14. Kapur, D., Sun, Y., Wang, D.: A new algorithm for computing comprehensive Gröbner systems. In: Proceedings ISSAC 2010, pp. 29–36. ACM, New York, USA (2010)

    Google Scholar 

  15. Korovin, K., Kos̆ta, M., Sturm, T.: Towards conflict-driven learning for virtual substitution. In: Gerdt, V.P., Koepf, W., Seiler, W.M., Vorozhtsov, E.V. (eds.) CASC 2014. LNCS, vol. 8660, pp. 256–270. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-10515-4_19

    Chapter  Google Scholar 

  16. Korovin, K., Tsiskaridze, N., Voronkov, A.: Implementing conflict resolution. In: Clarke, E., Virbitskaite, I., Voronkov, A. (eds.) PSI 2011. LNCS, vol. 7162, pp. 362–376. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-29709-0_31

    Chapter  Google Scholar 

  17. Korovin, K., Tsiskaridze, N., Voronkov, A.: Conflict resolution. In: Gent, I.P. (ed.) CP 2009. LNCS, vol. 5732, pp. 509–523. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-04244-7_41

    Chapter  Google Scholar 

  18. Korovin, K., Voronkov, A.: Solving systems of linear inequalities by bound propagation. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS (LNAI), vol. 6803, pp. 369–383. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22438-6_28

    Chapter  Google Scholar 

  19. Lefévre, V.: Moyens arithmetiques pour un calcul fiable. PhD thesis, École normale supérieure de Lyon (2000)

    Google Scholar 

  20. Loos, R., Weispfenning, V.: Applying linear quantifier elimination. Comput. J. 36(5), 450–462 (1993)

    Article  MathSciNet  Google Scholar 

  21. Maréchal, A., Fouilhé, A., King, T., Monniaux, D., Périn, M.: Polyhedral approximation of multivariate polynomials using Handelman’s theorem. In: Jobstmann, B., Leino, K.R.M. (eds.) VMCAI 2016. LNCS, vol. 9583, pp. 166–184. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-49122-5_8

    Chapter  Google Scholar 

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

  23. McMillan, K.L., Kuehlmann, A., Sagiv, M.: Generalizing DPLL to richer logics. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 462–476. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-02658-4_35

    Chapter  Google Scholar 

  24. Müller, N.T.: The iRRAM: exact arithmetic in C++. In: Blanck, J., Brattka, V., Hertling, P. (eds.) CCA 2000. LNCS, vol. 2064, pp. 222–252. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-45335-0_14

    Chapter  Google Scholar 

  25. 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  Google Scholar 

  26. Niven, I.: Irrational Numbers. Mathematical Association of America, Washington, D.C. (1956)

    MATH  Google Scholar 

  27. Passmore, G.O., Paulson, L.C., de Moura, L.: Real algebraic strategies for MetiTarski proofs. In: Jeuring, J., et al. (eds.) CICM 2012. LNCS (LNAI), vol. 7362, pp. 358–370. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-31374-5_24

    Chapter  Google Scholar 

  28. Reger, G., Bjorner, N., Suda, M., Voronkov, A.: AVATAR modulo theories. In: Benzmüller, C., Sutcliffe, G., Rojas, R. (eds.), 2nd Global Conference on Artificial Intelligence, EPiC Series in Computing, vol. 41, pp. 39–52. EasyChair (2016)

    Google Scholar 

  29. Reynolds, A., Tinelli, C., Jovanović, D., Barrett, C.: Designing theory solvers with extensions. In: Dixon, C., Finger, M. (eds.) FroCoS 2017. LNCS (LNAI), vol. 10483, pp. 22–40. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-66167-4_2

    Chapter  Google Scholar 

  30. Richardson, D.: Some undecidable problems involving elementary functions of a real variable. J. Symb. Log. 33(4), 514–520 (1968)

    Article  MathSciNet  Google Scholar 

  31. Tarski, A.: A decision method for elementary algebra and geometry. In: 2nd edn. University of California (1951)

    Google Scholar 

  32. Weihrauch, K.: Computable Analysis: An Introduction. Springer, Secaucus (2000). https://doi.org/10.1007/978-3-642-56999-9

    Book  MATH  Google Scholar 

Download references

Acknowledgements

We thank the anonymous reviewers and Stefan Ratschan for their helpful comments.

Author information

Authors and Affiliations

  1. Abteilung Informatikwissenschaften, Universität Trier, Trier, Germany

    Franz Brauße & Norbert Müller

  2. The University of Manchester, Manchester, UK

    Konstantin Korovin

  3. A.P. Ershov Institute of Informatics Systems, Novosibirsk, Russia

    Margarita Korovina

Authors
  1. Franz Brauße
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Konstantin Korovin
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Margarita Korovina
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Norbert Müller
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Franz Brauße .

Editor information

Editors and Affiliations

  1. CNRS, University of Toulouse, Toulouse, France

    Andreas Herzig

  2. Middlesex University London, London, UK

    Andrei Popescu

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Brauße, F., Korovin, K., Korovina, M., Müller, N. (2019). A CDCL-Style Calculus for Solving Non-linear Constraints. In: Herzig, A., Popescu, A. (eds) Frontiers of Combining Systems. FroCoS 2019. Lecture Notes in Computer Science(), vol 11715. Springer, Cham. https://doi.org/10.1007/978-3-030-29007-8_8

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-29007-8_8

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-29006-1

  • Online ISBN: 978-3-030-29007-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation