Handling polynomial and transcendental functions in SMT via unconstrained optimisation and topological degree test

DOI10.1007/978-3-031-19992-9_9MaRDI QIDQ6160909zbMATH OpenOpenAlexFDO

Authors Alessandro Cimatti, Alberto Griggio, Enrico Lipparini, Roberto Sebastiani

Publication date 2 June 2023

Published in Automated Technology for Verification and Analysis (Search for Journal in Brave)

Full work available at URL https://hdl.handle.net/11572/369588

Mathematics Subject Classification ID

Nonlinear programming (90C30) Degree, winding number (55M25) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Satisfiability modulo transcendental functions via incremental linearization
• Incremental linearization for satisfiability and verification modulo nonlinear arithmetic and transcendental functions
• dReal: an SMT solver for nonlinear theories over the reals
• Subtropical satisfiability
• Deciding polynomial-transcendental problems

Cites work

• scientific article; zbMATH DE number 3497890 (Why is no real title available?)
• scientific article; zbMATH DE number 5263038 (Why is no real title available?)
• A model-constructing satisfiability calculus
• Algorithm 852
• Computation of Topological Degree Using Interval Arithmetic, and Applications
• Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings
• Effective topological degree computation based on interval arithmetic
• Incremental linearization for satisfiability and verification modulo nonlinear arithmetic and transcendental functions
• Interval Methods for Systems of Equations
• Introduction to Interval Analysis
• Quasi-decidability of a fragment of the first-order theory of real numbers
• Safety verification of non-linear hybrid systems is quasi-decidable
• Some undecidable problems involving elementary functions of a real variable
• The MathSAT5 SMT solver
• The \texttt{ksmt} calculus is a \(\delta \)-complete decision procedure for non-linear constraints
• Topological degree theory and applications.
• Understanding the Hastings algorithm
• -complete decision procedures for satisfiability over the reals
• \texttt{SMT-RAT}: an open source \texttt{C++} toolbox for strategic and parallel SMT solving
• dReal: an SMT solver for nonlinear theories over the reals
• raSAT: an SMT solver for polynomial constraints

Cited in

(4)

• Satisfiability of non-linear transcendental arithmetic as a certificate search problem
• Incremental linearization for satisfiability and verification modulo nonlinear arithmetic and transcendental functions
• Satisfiability modulo exponential integer arithmetic
• Boosting MCSat modulo nonlinear integer arithmetic via local search

This page was built for publication: Handling polynomial and transcendental functions in SMT via unconstrained optimisation and topological degree test

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