Cristina Borralleras, Salvador Lucas, Albert Oliveras, Enric Rodríguez-Carbonell, and Albert Rubio. Sat modulo linear arithmetic for solving polynomial constraints. Journal of Automated Reasoning, 48(1):107–131, Jan 2012.

Martin Bromberger and Christoph Weidenbach. Fast cube tests for lia constraint solving. In Nicola Olivetti and Ashish Tiwari, editors, Automated Reasoning, pages 116–132, Cham, 2016. Springer International Publishing.

Christopher W. Brown. Improved projection for cylindrical algebraic decomposition. Journal of Symbolic Computation, 32(5):447 – 465, 2001.

Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, and Roberto Sebastiani. Satisfiability modulo transcendental functions via incremental linearization. In Leonardo de Moura, editor, Automated Deduction – CADE 26, pages 95–113, Cham, 2017. Springer International Publishing.

G. E. Collins. Quantifier elimination for real closed fields by cylindrical algebraic decomposition. In Automata Theory and Formal Languages, volume 33 of LNCS, pages 134–183. Springer, 1975.

F. Corzilius and E. Ábrahám. Virtual substitution for SMT solving. In 18th Int. Symp. on Fundamentals of Computation Theory, 2011.

Isil Dillig, Thomas Dillig, and Alex Aiken. Cuts from proofs: a complete and practical technique for solving linear inequalities over integers. Formal Methods in System Design, 39(3):246–260, 2011.

B. Dutertre and L. de Moura. A fast linear-arithmetic solver for DPLL(T). In Proc. of CAV'06, volume 4144 of LNCS, pages 81–94. Springer, 2006.

Pascal Fontaine, Mizuhito Ogawa, Thomas Sturm, and Xuan Tung Vu. Subtropical satisfiability. In International Symposium on Frontiers of Combining Systems, pages 189–206. Springer, 2017.

Carsten Fuhs, Jürgen Giesl, Aart Middeldorp, Peter Schneider-Kamp, René Thiemann, and Harald Zankl. Sat solving for termination analysis with polynomial interpretations. In João Marques-Silva and Karem A. Sakallah, editors, Theory and Applications of Satisfiability Testing – SAT 2007, pages 340–354, Berlin, Heidelberg, 2007. Springer Berlin Heidelberg.

S. Gao, M. K. Ganai, F. Ivancic, A. Gupta, S. Sankaranarayanan, and E. M. Clarke. Integrating ICP and LRA solvers for deciding nonlinear real arithmetic problems. In Proc. of FMCAD'10, pages 81–89. IEEE, 2010.

Alberto Griggio. A practical approach to satisfiability modulo linear integer arithmetic. Journal on Satisfiability, Boolean Modeling and Computation, 8:1–27, 2012.

Marta Grobelna. Solving pseudo-boolean constraints, 2017.

Stefan Herbort and Dietmar Ratz. Improving the efficiency of a nonlinear-system-solver using a componentwise newton method. 1997.

H. Hong. An improvement of the projection operator in cylindrical algebraic decomposition. In Proceedings of the International Symposium on Symbolic and Algebraic Computation, ISSAC '90, pages 261–264, New York, NY, USA, 1990. ACM.

Ahmed Irfan. Incremental linearization for satisfiability and verification modulo nonlinear arithmetic and transcendental functions. PhD thesis, University of Trento, 2018.

S. Junges, U. Loup, F. Corzilius, and E. Ábrahám. On Gröbner bases in the context of satisfiability-modulo-theories solving over the real numbers. Technical Report AIB-2013-08, RWTH Aachen University, 2013.

Gereon Kremer and Erika Ábrahám. Fully incremental cylindrical algebraic decomposition. Journal of Symbolic Computation, 2019.

Gereon Kremer, Florian Corzilius, and Erika Ábrahám. A Generalised Branch-and-Bound Approach and Its Application in SAT Modulo Nonlinear Integer Arithmetic. In Proc. of CASC'16, pages 315–335. Springer, 2016.

Andreas Krüger. Bitvectors in smt-rat and their application to integer arithmetics, 2015.

Daniel Lazard. An Improved Projection for Cylindrical Algebraic Decomposition, chapter 29, pages 467–476. Springer, 1994.

U. Loup, K. Scheibler, F. Corzilius, Erika E. Ábrahám, and Bernd Becker. A symbiosis of interval constraint propagation and cylindrical algebraic decomposition. In Proc. of CADE-24, volume 7898 of LNCS, pages 193–207. Springer, 2013.

Scott McCallum. An improved projection operation for cylindrical algebraic decomposition, pages 277–278. Springer Berlin Heidelberg, Berlin, Heidelberg, 1985.

Robert Nieuwenhuis and Albert Oliveras. Fast congruence closure and extensions. Information and Computation, 205(4):557 – 580, 2007. Special Issue: 16th International Conference on Rewriting Techniques and Applications.

Aklima Zaman. Incremental linearization for sat modulo real arithmetic solving, 2019.

Ömer Sali. Linearization techniques for nonlinear arithmetic problems in smt, 2018.