Satisfiability Modulo Transcendental Functions via Incremental Linearization

TL;DR

This paper introduces an abstraction-refinement method for solving satisfiability problems involving transcendental functions, using incremental linearization and numerical techniques to ensure soundness and efficiency.

Contribution

It presents a novel approach that combines abstraction, incremental linearization, and numerical methods to handle transcendental functions in SMT solving.

Findings

Outperforms delta-satisfiability and interval propagation methods.

Effective on benchmarks from verification and mathematics.

Ensures soundness with irrational numbers.

Abstract

In this paper we present an abstraction-refinement approach to Satisfiability Modulo the theory of transcendental functions, such as exponentiation and trigonometric functions. The transcendental functions are represented as uninterpreted in the abstract space, which is described in terms of the combined theory of linear arithmetic on the rationals with uninterpreted functions, and are incrementally axiomatized by means of upper- and lower-bounding piecewise-linear functions. Suitable numerical techniques are used to ensure that the abstractions of the transcendental functions are sound even in presence of irrationals. Our experimental evaluation on benchmarks from verification and mathematics demonstrates the potential of our approach, showing that it compares favorably with delta-satisfiability /interval propagation and methods based on theorem proving.