Satisfiability modulo transcendental functions via incremental linearization

DOI10.1007/978-3-319-63046-5_7MaRDI QIDQ2405243zbMATH OpenOpenAlexWikidataFDO

Authors Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, Roberto Sebastiani

Publication date 22 September 2017

Full work available at URL https://arxiv.org/abs/1801.08723

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

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.

Recommendations

• Incremental linearization for satisfiability and verification modulo nonlinear arithmetic and transcendental functions
• A practical approach to satisfiability modulo linear integer arithmetic
• Efficient representation of piecewise linear functions into Łukasiewicz logic modulo satisfiability
• Satisfiability modulo linear arithmetic over a finite ring
• Satisfiability modulo theories and assignments
• Tools and Algorithms for the Construction and Analysis of Systems
• Satisfiability of non-linear (ir)rational arithmetic
• Satisfiability modulo theories
• SAT Modulo the Theory of Linear Arithmetic: Exact, Inexact and Commercial Solvers

Cited in

(7)

• Lattice-based refinement in bounded model checking
• Flexible proof production in an industrial-strength SMT solver
• A conflict-driven solving procedure for poly-power constraints
• \textsc{OptiMathSAT}: a tool for optimization modulo theories
• scientific article; zbMATH DE number 1574496 (Why is no real title available?)
• Incremental linearization for satisfiability and verification modulo nonlinear arithmetic and transcendental functions
• Handling polynomial and transcendental functions in SMT via unconstrained optimisation and topological degree test

This page was built for publication: Satisfiability modulo transcendental functions via incremental linearization

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2405243)