Satisfiability of Non-Linear Transcendental Arithmetic as a Certificate Search Problem

TL;DR

The paper investigates satisfiability for nonlinear real arithmetic augmented with transcendental functions ($\SMT(\mathcal{N\mkern-1muT\mkern-4muA})$), where direct finite representations of satisfying assignments are unavailable. It introduces a certifying satisfiability framework that searches for certificates in the form of a triple $(\sigma,\nu,\beta)$ and bases verification on the topological degree test together with interval arithmetic, enabling independent correctness checks. A suite of certificate-search strategies and a prototype solver demonstrate substantially more solved benchmarks than existing methods, and the work provides a theoretical classification of formulas solvable by such certificates via lower/upper bounds tied to known classes, plus termination results under robustness assumptions. The results motivate integrating certifying certificate search into SMT solvers and suggest extending the approach to richer theories, with practical implications for verification and automatic reasoning about systems involving nonlinear and transcendental real arithmetic.

Abstract

For typical first-order logical theories, satisfying assignments have a straightforward finite representation that can directly serve as a certificate that a given assignment satisfies the given formula. For non-linear real arithmetic augmented with trigonometric and exponential functions (NTA), however, there is no known direct representation of satisfying assignments that allows for a simple independent check of whether the represented numbers exist and satisfy the given formula. Hence, in this paper, we introduce a different form of satisfiability certificate for NTA, and formulate the satisfiability problem as the problem of searching for such a certificate. This does not only ease the independent verification of satisfiability, but also allows the design of new algorithms that show satisfiability by systematically searching for such certificates. Computational experiments document that the resulting algorithms are able to prove satisfiability of a substantially higher number of benchmark problems than existing methods. We also characterize the formulas whose satisfiability can be demonstrated by such a certificate, by providing lower and upper bounds in terms of relevant well-known classes. Finally we show the existence of a procedure for checking the satisfiability of NTA-formulas that terminates for formulas that satisfy certain robustness assumptions.