Cooperating techniques for solving nonlinear real arithmetic in the \texttt{cvc5} SMT solver (system description)

DOI10.1007/978-3-031-10769-6_7OpenAlexW4289104052MaRDI QIDQ2104500FDOQ2104500

Authors: Gereon Kremer, Andrew Reynolds, Clark Barrett, Cesare Tinelli 

Publication date: 7 December 2022

Full work available at URL: https://doi.org/10.1007/978-3-031-10769-6_7

zbMATH Keywords

abstraction refinementsatisfiability modulo theoriesnonlinear real arithmeticcylindrical algebraic coverings

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites Work

• dReal: an SMT solver for nonlinear theories over the reals
• \texttt{SMT-RAT}: an open source \texttt{C++} toolbox for strategic and parallel SMT solving
• The MathSAT5 SMT solver
• Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)
• Solving non-linear arithmetic
• A model-constructing satisfiability calculus
• Title not available (Why is that?)
• Solving systems of polynomial inequalities in subexponential time
• On the combinatorial and algebraic complexity of quantifier elimination
• Real quantifier elimination is doubly exponential
• Quantifier elimination for real algebra -- the quadratic case and beyond
• Validity proof of Lazard's method for CAD construction
• Title not available (Why is that?)
• A symbiosis of interval constraint propagation and cylindrical algebraic decomposition
• Designing theory solvers with extensions
• Subtropical satisfiability
• Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings
• Fully incremental cylindrical algebraic decomposition
• Incremental linearization for satisfiability and verification modulo nonlinear arithmetic and transcendental functions
• raSAT: An SMT Solver for Polynomial Constraints
• SAT Modulo the Theory of Linear Arithmetic: Exact, Inexact and Commercial Solvers
• Virtual substitution for SMT-solving
• Planning for hybrid systems via satisfiability modulo theories

Cited In (1)

• CVC4

Uses Software

• CoCoA
• CoCoALib
• REDLOG
• Yices
• z3
• libpoly
• dReal
• veriT
• MathSAT5
• SMT-RAT
• raSAT
• Zephyrus2

This page was built for publication: Cooperating techniques for solving nonlinear real arithmetic in the \texttt{cvc5} SMT solver (system description)

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