Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings
From MaRDI portal
Publication:1996869
Recommendations
- Solving non-linear arithmetic
- A symbiosis of interval constraint propagation and cylindrical algebraic decomposition
- A CDCL-style calculus for solving non-linear constraints
- From simplification to a partial theory solver for non-linear real polynomial constraints
- SAT modulo linear arithmetic for solving polynomial constraints
Cites work
- \textsf{SC}\(^2\): satisfiability checking meets symbolic computation. (Project paper)
- \texttt{SMT-RAT}: an open source \texttt{C++} toolbox for strategic and parallel SMT solving
- A case study on the parametric occurrence of multiple steady states
- A model-constructing satisfiability calculus
- A new decision method for elementary algebra
- Adapting real quantifier elimination methods for conflict set computation
- Algorithms in real algebraic geometry
- Building bridges between symbolic computation and satisfiability checking
- CoCoALib: A C++ library for computations in commutative algebra and beyond
- Comparing machine learning models to choose the variable ordering for cylindrical algebraic decomposition
- Cylindrical algebraic decomposition in the RegularChains library
- Cylindrical algebraic decomposition with equational constraints
- Cylindrical algebraic sub-decompositions
- Editorial: Symbolic computation and satisfiability checking
- Enhancements to Lazard's method for cylindrical algebraic decomposition
- Fully incremental cylindrical algebraic decomposition
- scientific article; zbMATH DE number 589124 (Why is no real title available?)
- scientific article; zbMATH DE number 1157648 (Why is no real title available?)
- scientific article; zbMATH DE number 1157649 (Why is no real title available?)
- scientific article; zbMATH DE number 1157650 (Why is no real title available?)
- scientific article; zbMATH DE number 1157658 (Why is no real title available?)
- scientific article; zbMATH DE number 5263038 (Why is no real title available?)
- scientific article; zbMATH DE number 5493266 (Why is no real title available?)
- Improved Cross-Validation for Classifiers that Make Algorithmic Choices to Minimise Runtime Without Compromising Output Correctness
- Improving the use of equational constraints in cylindrical algebraic decomposition
- Incremental linearization for satisfiability and verification modulo nonlinear arithmetic and transcendental functions
- Mathematics by machine
- New Domains for Applied Quantifier Elimination
- Open non-uniform cylindrical algebraic decompositions
- Partial cylindrical algebraic decomposition for quantifier elimination
- Polyhedral approximation of multivariate polynomials using Handelman's theorem
- Projection and Quantifier Elimination Using Non-uniform Cylindrical Algebraic Decomposition
- Quantifier elimination for real algebra -- the quadratic case and beyond
- raSAT: an SMT solver for polynomial constraints
- SATzilla: portfolio-based algorithm selection for SAT
- Solving non-linear arithmetic
- Solving nonlinear integer arithmetic with MCSAT
- Subtropical satisfiability
- The complexity of cylindrical algebraic decomposition with respect to polynomial degree
- The complexity of quantifier elimination and cylindrical algebraic decomposition
- TheoryGuru: a Mathematica package to apply quantifier elimination technology to economics
- Truth table invariant cylindrical algebraic decomposition
- Using machine learning to improve cylindrical algebraic decomposition
- Validity proof of Lazard's method for CAD construction
- Virtual substitution for SMT-solving
Cited in
(20)- 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
- A CDCL-style calculus for solving non-linear constraints
- From simplification to a partial theory solver for non-linear real polynomial constraints
- Solving non-linear arithmetic
- A symbiosis of interval constraint propagation and cylindrical algebraic decomposition
- An SMT solver for non-linear real arithmetic inside maple
- 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
- Local search for solving satisfiability of polynomial formulas
- Satisfiability modulo finite fields
- Introducing asynchronicity to probabilistic hyperproperties
- Recent developments in real quantifier elimination and cylindrical algebraic decomposition (extended abstract of invited talk)
- Merging adjacent cells during single cell construction
- More is less: adding polynomials for faster explanations in NLSAT
- Iterated resultants and rational functions in real quantifier elimination
- Optimization modulo non-linear arithmetic via incremental linearization
Describes a project that uses
Uses Software
This page was built for publication: Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1996869)
