Handling Polynomial and Transcendental Functions in SMT via Unconstrained Optimisation and Topological Degree Test

We present a method for determining the satisfiability of quantifier-free first-order formulas modulo the theory of non-linear arithmetic over the reals augmented with transcendental functions. Our procedure is based on the fruitful combination of two main ingredients: unconstrained optimisation, to generate a set of candidate solutions, and a result from topology called the topological degree test to check whether a given bounded region contains at least a solution. We have implemented the procedure in a prototype tool called ugotNL, and integrated it within the MathSAT SMT solver. Our experimental evaluation over a wide range of benchmarks shows that it vastly improves the performance of the solver for satisfiable non-linear arithmetic formulas, significantly outperforming other available tools for problems with transcendental functions.