Satisfiability modulo Nonlinear Arithmetic and Transcendental Functions via Numerical and Topological methods

Satisfiability Modulo Theories (SMT) is the problem of deciding the satisfiability of a first-order formula with respect to some background theory. In this thesis, we focus on the theory of non-linear real arithmetic augmented with exponential and trigonometric functions, also known as Non-linear Transcendental Arithmetic (NTA). NTA is a very expressive theory, which can be used to model problems in different domains, such as physics, engineering, economics, and biology. Unfortunately, solving problems in NTA is very challenging: indeed, the problem is undecidable, there is no known finite representation of satisfying assignments, and symbolic methods struggle to reason precisely about transcendental functions. State-of-the-art SMT solvers usually rely on over-approximations of transcendental functions, and are thus unable to prove the existence of a model, except that in very simple cases. We propose a novel approach to SMT(NTA) that leverages techniques coming from the fields of numerical analysis and topology, and integrates them within the SMT context. Numerical methods are used to quickly obtain approximate candidate solutions, which can be used to reduce the search of a model to simpler local sub-problems. Topological methods are used to prove the existence of a solution in a bounded region without the need to explicitly express such a solution, thus circumventing the issue of representing satisfying assignments. We implement our procedure in the prototype tool ugotNL, and experimentally evaluate the tool performances over a wide range of NTA benchmarks. The experiments show that the tool significantly outperforms other state-of-the-art SMT solvers on satisfiable NTA problems, being able to solve more than four times the benchmarks solved by the best of the other tools. Furthermore, we characterize the class of problems for which our method can terminate successfully. Based on that, we contribute with an original theorem that proves that a weaker notion of decidability holds for bounded NTA formulas, namely that there exists an algorithm that always terminates successfully under certain assumptions on the robustness of the problem. Finally, we outline how our idea of leveraging fast numerical techniques to accelerate the search for a model can fit into a more general framework such as the model-constructing satisfiability calculus (MCSAT), and how it can be applied to other theories, such as non-linear integer arithmetic (NIA).