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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
- 2.
- 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
Benhamou, F., Granvilliers, L.: Continuous and interval constraints. In: Handbook of Constraint Programming, pp. 571–603. Elsevier (2006)
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
Buchberger, B.: A theoretical basis for the reduction of polynomials to canonical forms. ACM SIGSAM Bull. 10(3), 19–29 (1976)
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)
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
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
Dolzmann, A., Sturm, T.: REDLOG: computer algebra meets computer logic. ACM SIGSAM Bull. 31(2), 2–9 (1997)
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)
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
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)
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
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)
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
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)
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
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
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
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
Lefévre, V.: Moyens arithmetiques pour un calcul fiable. PhD thesis, École normale supérieure de Lyon (2000)
Loos, R., Weispfenning, V.: Applying linear quantifier elimination. Comput. J. 36(5), 450–462 (1993)
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
Marques-Silva, J.P., Sakallah, K.A.: GRASP: a search algorithm for propositional satisfiability. IEEE Trans. Comput. 48(5), 506–521 (1999)
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
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
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)
Niven, I.: Irrational Numbers. Mathematical Association of America, Washington, D.C. (1956)
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
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)
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
Richardson, D.: Some undecidable problems involving elementary functions of a real variable. J. Symb. Log. 33(4), 514–520 (1968)
Tarski, A.: A decision method for elementary algebra and geometry. In: 2nd edn. University of California (1951)
Weihrauch, K.: Computable Analysis: An Introduction. Springer, Secaucus (2000). https://doi.org/10.1007/978-3-642-56999-9
Acknowledgements
We thank the anonymous reviewers and Stefan Ratschan for their helpful comments.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this paper
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)