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.

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

Cimatti, Alessandro;Griggio, Alberto;Lipparini, Enrico;
2022-01-01

Abstract

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.
2022
978-3-031-19991-2
978-3-031-19992-9
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11582/335886
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
social impact