raSAT: an SMT solver for polynomial constraints
From MaRDI portal
Publication:1688535
DOI10.1007/s10703-017-0284-9zbMath1377.68140OpenAlexW2730414357MaRDI QIDQ1688535
To Van Khanh, Mizuhito Ogawa, Vu Xuan Tung
Publication date: 8 January 2018
Published in: Formal Methods in System Design (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10703-017-0284-9
interval arithmetictestingSMT solvingintermediate value theorempolynomial constraintsinterval constraint propagation
Related Items
Modular strategic SMT solving with \textbf{SMT-RAT}, Handling polynomial and transcendental functions in SMT via unconstrained optimisation and topological degree test, Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings, raSAT: An SMT Solver for Polynomial Constraints
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Deciding floating-point logic with abstract conflict driven clause learning
- Interval-based projection method for under-constrained numerical systems
- Real quantifier elimination is doubly exponential
- raSAT: An SMT Solver for Polynomial Constraints
- Subtropical Real Root Finding
- Numeric Bounds Analysis with Conflict-Driven Learning
- Solving Non-linear Arithmetic
- Abstract conflict driven learning
- Automatic detection of floating-point exceptions
- Satisfiability of Non-linear (Ir)rational Arithmetic
- Solving SAT and SAT Modulo Theories
- Algorithm 852
- Combined Decision Techniques for the Existential Theory of the Reals
- Interval Methods for Systems of Equations
- A Symbiosis of Interval Constraint Propagation and Cylindrical Algebraic Decomposition
- dReal: An SMT Solver for Nonlinear Theories over the Reals
- Efficient solving of quantified inequality constraints over the real numbers
- Theory and Applications of Satisfiability Testing
- On stirling numbers of the second kind
