Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings
From MaRDI portal
Publication:1996869
DOI10.1016/j.jlamp.2020.100633OpenAlexW3010680447MaRDI QIDQ1996869
Matthew England, Erika Ábrahám, Gereon Kremer, James H. Davenport
Publication date: 26 February 2021
Published in: Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/2003.05633
cylindrical algebraic decompositionsatisfiability modulo theoriesnonlinear real arithmeticreal polynomial systems
Symbolic computation and algebraic computation (68W30) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Related Items
Optimization modulo non-linear arithmetic via incremental linearization, Proving an execution of an algorithm correct?, Levelwise construction of a single cylindrical algebraic cell, Handling polynomial and transcendental functions in SMT via unconstrained optimisation and topological degree test, Computing with Tarski formulas and semi-algebraic sets in a web browser, Flexible proof production in an industrial-strength SMT solver, Cooperating techniques for solving nonlinear real arithmetic in the \texttt{cvc5} SMT solver (system description), New heuristic to choose a cylindrical algebraic decomposition variable ordering motivated by complexity analysis
Uses Software
Cites Work
- Cylindrical algebraic sub-decompositions
- Quantifier elimination for real algebra -- the quadratic case and beyond
- Partial cylindrical algebraic decomposition for quantifier elimination
- TheoryGuru: a Mathematica package to apply quantifier elimination technology to economics
- Subtropical satisfiability
- raSAT: an SMT solver for polynomial constraints
- Validity proof of Lazard's method for CAD construction
- Using machine learning to improve cylindrical algebraic decomposition
- Enhancements to Lazard's method for cylindrical algebraic decomposition
- Comparing machine learning models to choose the variable ordering for cylindrical algebraic decomposition
- Editorial: Symbolic computation and satisfiability checking
- Fully incremental cylindrical algebraic decomposition
- Cylindrical algebraic decomposition with equational constraints
- A new decision method for elementary algebra
- Polyhedral Approximation of Multivariate Polynomials Using Handelman’s Theorem
- $$\mathsf {SC}^\mathsf{2} $$ : Satisfiability Checking Meets Symbolic Computation
- Building Bridges between Symbolic Computation and Satisfiability Checking
- Open Non-uniform Cylindrical Algebraic Decompositions
- Improving the Use of Equational Constraints in Cylindrical Algebraic Decomposition
- The Complexity of Cylindrical Algebraic Decomposition with Respect to Polynomial Degree
- Cylindrical Algebraic Decomposition in the RegularChains Library
- Solving Non-linear Arithmetic
- A Model-Constructing Satisfiability Calculus
- Solving Nonlinear Integer Arithmetic with MCSAT
- Adapting Real Quantifier Elimination Methods for Conflict Set Computation
- Virtual Substitution for SMT-Solving
- Mathematics by machine
- SMT-RAT: An Open Source C++ Toolbox for Strategic and Parallel SMT Solving
- New Domains for Applied Quantifier Elimination
- Incremental Linearization for Satisfiability and Verification Modulo Nonlinear Arithmetic and Transcendental Functions
- Improved Cross-Validation for Classifiers that Make Algorithmic Choices to Minimise Runtime Without Compromising Output Correctness
- A Case Study on the Parametric Occurrence of Multiple Steady States
- Projection and Quantifier Elimination Using Non-uniform Cylindrical Algebraic Decomposition
- CoCoALib: A C++ Library for Computations in Commutative Algebra... and Beyond
- Algorithms in real algebraic geometry
- Truth table invariant cylindrical algebraic decomposition
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
