@inproceedings{10.1007/978-3-319-94144-8_23,
    Abstract = {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.},
    Address = {Cham},
    Author = {Cimatti, Alessandro and Griggio, Alberto and Irfan, Ahmed and Roveri, Marco and Sebastiani, Roberto},
    BookTitle = {Theory and Applications of Satisfiability Testing -- SAT 2018},
    Editor = {Beyersdorff, Olaf and Wintersteiger, Christoph M.},
    File = {sat18 (0) (0) - a - a - c.pdf},
    ISBN = {978-3-319-94144-8},
    Pages = {383--398},
    Publisher = {Springer International Publishing},
    Title = {Experimenting on Solving Nonlinear Integer Arithmetic with Incremental Linearization},
    Year = {2018},
    date-added = {2019-03-12 20:27:05 +0100},
    date-modified = {2019-03-12 20:27:05 +0100},
    doi = {10.1007/978-3-319-94144-8_23}
}

@inproceedings{10.1007/978-3-319-94144-8_23, Abstract = {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.}, Address = {Cham}, Author = {Cimatti, Alessandro and Griggio, Alberto and Irfan, Ahmed and Roveri, Marco and Sebastiani, Roberto}, BookTitle = {Theory and Applications of Satisfiability Testing -- SAT 2018}, Editor = {Beyersdorff, Olaf and Wintersteiger, Christoph M.}, File = {sat18 (0) (0) - a - a - c.pdf}, ISBN = {978-3-319-94144-8}, Pages = {383--398}, Publisher = {Springer International Publishing}, Title = {Experimenting on Solving Nonlinear Integer Arithmetic with Incremental Linearization}, Year = {2018}, date-added = {2019-03-12 20:27:05 +0100}, date-modified = {2019-03-12 20:27:05 +0100}, doi = {10.1007/978-3-319-94144-8_23} }