Incremental linearization is a conceptually simple, yet effective, technique that we have recently proposed for solving SMT problems over nonlinear real arithmetic constraints. In this paper, we show how the same approach can be applied successfully also to the harder case of nonlinear integer arithmetic problems. We describe in detail our implementation of the basic ideas inside the MathSAT SMT solver, and evaluate its effectiveness with an extensive experimental analysis over all nonlinear integer benchmarks in SMT-LIB. Our results show that MathSAT is very competitive with (and often outperforms) state-of-the-art SMT solvers based on alternative techniques.
CITATION STYLE
Cimatti, A., Griggio, A., Irfan, A., Roveri, M., & Sebastiani, R. (2018). Experimenting on solving nonlinear integer arithmetic with incremental linearization. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 10929 LNCS, pp. 383–398). Springer Verlag. https://doi.org/10.1007/978-3-319-94144-8_23
Mendeley helps you to discover research relevant for your work.