Abstract
In this paper we present an abstraction-refinement approach to Satisfiability Modulo the theory of transcendental functions, such as exponentiation and trigonometric functions. The transcendental functions are represented as uninterpreted in the abstract space, which is described in terms of the combined theory of linear arithmetic on the rationals with uninterpreted functions, and are incrementally axiomatized by means of upper- and lower-bounding piecewise-linear functions. Suitable numerical techniques are used to ensure that the abstractions of the transcendental functions are sound even in presence of irrationals. Our experimental evaluation on benchmarks from verification and mathematics demonstrates the potential of our approach, showing that it compares favorably with delta-satisfiability/interval propagation and methods based on theorem proving.
This work was funded in part by the H2020-FETOPEN-2016-2017-CSA project SC\(^2\) (712689). We thank James Davenport and Erika Abraham for useful discussions.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
For simplicity, we assume that this is always possible. If needed, this can be implemented e.g. by generating the two points at random while ensuring that \(l< \widehat{\mu }[x] < u\) and that l, u do not cross any inflection point.
- 2.
Although, as mentioned above, this is not the case in general (see e.g. [21]), it is true for some special values, e.g. \(\exp (0) = 1\), \(\sin (0) = 0\).
- 3.
We remark that our tool (see Sect. 6) can handle also \(\log \), \(\cos \), \(\tan \), \(\arcsin \), \(\arccos \), \(\arctan \) by means of rewriting. We leave as future work the possibility of handling such functions natively.
- 4.
Because (i) \(\exp (0)=1\), \(\sin (0)=0\), \(\cos (0)=1\), (ii) \(\exp ^{(i)}(x) = \exp (x)\) for all i, and (iii) \(|\sin ^{(i)}(x)|\) is \(|\cos (x)|\) if i is odd and \(|\sin (x)|\) otherwise.
- 5.
In the interval \([-\pi , \pi ]\), the concavity of \(\sin (c)\) is the opposite of the sign of c.
- 6.
Sometimes we used a relational encoding: e.g. if \(\varphi \) contains \(\arcsin (x)\), we rewrite it as
, where \(as_x\) is a fresh variable. - 7.
There was no case in which two tools reported Sat and Unsat for the same benchmark.
- 8.
According to the documentation of \({\textsc {MetiTarski}}\), the tool is ineffective for problems with more than 10 real variables. Our experiments on a subset of the instances confirmed this.
- 9.
We contacted the authors of dReal and they reported that this issue is currently under investigation.
, where References
Akbarpour, B., Paulson, L.C.: MetiTarski: an automatic theorem prover for real-valued special functions. JAR 44(3), 175–205 (2010)
Allamigeon, X., Gaubert, S., Magron, V., Werner, B.: Certification of inequalities involving transcendental functions: combining SDP and max-plus approximation. In: 2013 European Control Conference (ECC), pp. 2244–2250. IEEE (2013)
Bak, S., Bogomolov, S., Johnson, T.T.: HYST: a source transformation and translation tool for hybrid automaton models. In: Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, pp. 128–133. ACM (2015)
Cavada, R., Cimatti, A., Dorigatti, M., Griggio, A., Mariotti, A., Micheli, A., Mover, S., Roveri, M., Tonetta, S.: The nuXmv symbolic model checker. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 334–342. Springer, Cham (2014). doi:10.1007/978-3-319-08867-9_22
Cimatti, A., Griggio, A., Irfan, A., Roveri, M., Sebastiani, R.: Invariant checking of NRA transition systems via incremental reduction to LRA with EUF. In: Legay and Margaria [16], pp. 58–75. https://es-static.fbk.eu/people/griggio/papers/tacas17.pdf
Cimatti, A., Griggio, A., Mover, S., Tonetta, S.: HyComp: an SMT-Based model checker for hybrid systems. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 52–67. Springer, Heidelberg (2015). doi:10.1007/978-3-662-46681-0_4
Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The MathSAT5 SMT solver. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 93–107. Springer, Heidelberg (2013). doi:10.1007/978-3-642-36742-7_7
Cimatti, A., Mover, S., Sessa, M.: From electrical switched networks to hybrid automata. In: Fitzgerald, J., Heitmeyer, C., Gnesi, S., Philippou, A. (eds.) FM 2016. LNCS, vol. 9995, pp. 164–181. Springer, Cham (2016). doi:10.1007/978-3-319-48989-6_11
de Dinechin, F., Lauter, C., Melquiond, G.: Certifying the floating-point implementation of an elementary function using Gappa. IEEE Trans. Comput. 60(2), 242–253 (2011)
Eggers, A., Kruglov, E., Kupferschmid, S., Scheibler, K., Teige, T., Weidenbach, C.: Superposition modulo non-linear arithmetic. In: Tinelli, C., Sofronie-Stokkermans, V. (eds.) FroCoS 2011. LNCS (LNAI), vol. 6989, pp. 119–134. Springer, Heidelberg (2011). doi:10.1007/978-3-642-24364-6_9
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, vol. 7364, pp. 286–300. Springer, Heidelberg (2012). doi:10.1007/978-3-642-31365-3_23
Gao, S., Kong, S., Clarke, E.M.: dReal: An SMT solver for nonlinear theories over the reals. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol. 7898, pp. 208–214. Springer, Heidelberg (2013). doi:10.1007/978-3-642-38574-2_14
Gario, M., Micheli, A.: PySMT: a solver-agnostic library for fast prototyping of SMT-based algorithms. In: SMT, pp. 373–384 (2015)
Hazewinkel, M.: Encyclopaedia of Mathematics: Stochastic Approximation Zygmund Class of Functions. Encyclopaedia of Mathematics. Springer, Netherlands (1993). https://books.google.it/books?id=1ttmCRCerVUC
Legay, A., Margaria, T. (eds.): TACAS 2017. LNCS, vol. 10205. Springer, Heidelberg (2017)
Magron, V.: NLCertify: a tool for formal nonlinear optimization. In: Hong, H., Yap, C. (eds.) ICMS 2014. LNCS, vol. 8592, pp. 315–320. Springer, Heidelberg (2014). doi:10.1007/978-3-662-44199-2_49
Martin-Dorel, É., Melquiond, G.: Proving tight bounds on univariate expressions with elementary functions in Coq. J. Autom. Reasoning 57(3), 187–217 (2016)
Melquiond, G.: Coq-interval (2011)
Nemhauser, G.L., Wolsey, L.A.: Integer and Combinatorial Optimization. Wiley-Interscience, New York (1988)
Nieven, I.: Numbers: Rational and Irrational. Mathematical Association of America (1961)
Ratschan, S.: Efficient solving of quantified inequality constraints over the real numbers. TOCL 7(4), 723–748 (2006)
Roohi, N., Prabhakar, P., Viswanathan, M.: HARE: A hybrid abstraction refinement engine for verifying non-linear hybrid automata. In: Legay and Margaria [16], pp. 573–588
Scheibler, K., Kupferschmid, S., Becker, B.: Recent improvements in the SMT solver iSAT. MBMV 13, 231–241 (2013)
Solovyev, A., Hales, T.C.: Formal verification of nonlinear inequalities with taylor interval approximations. In: Brat, G., Rungta, N., Venet, A. (eds.) NFM 2013. LNCS, vol. 7871, pp. 383–397. Springer, Heidelberg (2013). doi:10.1007/978-3-642-38088-4_26
Townsend, E.: Functions of a Complex Variable. Read Books (2007)
Weidenbach, C., Dimova, D., Fietzke, A., Kumar, R., Suda, M., Wischnewski, P.: SPASS version 3.5. In: Schmidt, R.A. (ed.) CADE 2009. LNCS (LNAI), vol. 5663, pp. 140–145. Springer, Heidelberg (2009). doi:10.1007/978-3-642-02959-2_10
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
Cimatti, A., Griggio, A., Irfan, A., Roveri, M., Sebastiani, R. (2017). Satisfiability Modulo Transcendental Functions via Incremental Linearization. In: de Moura, L. (eds) Automated Deduction – CADE 26. CADE 2017. Lecture Notes in Computer Science(), vol 10395. Springer, Cham. https://doi.org/10.1007/978-3-319-63046-5_7
Download citation
DOI: https://doi.org/10.1007/978-3-319-63046-5_7
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-63045-8
Online ISBN: 978-3-319-63046-5
eBook Packages: Computer ScienceComputer Science (R0)