raSAT: An SMT Solver for Polynomial Constraints
From MaRDI portal
Publication:2817923
DOI10.1007/978-3-319-40229-1_16zbMath1475.68359OpenAlexW2496780659MaRDI QIDQ2817923
To Van Khanh, Vu Xuan Tung, Mizuhito Ogawa
Publication date: 5 September 2016
Published in: Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-319-40229-1_16
Nonlinear programming (90C30) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Related Items
Satisfiability Checking: Theory and Applications, raSAT: an SMT solver for polynomial constraints, The ksmt calculus is a \(\delta \)-complete decision procedure for non-linear constraints, The \texttt{ksmt} calculus is a \(\delta \)-complete decision procedure for non-linear constraints, A Generalised Branch-and-Bound Approach and Its Application in SAT Modulo Nonlinear Integer Arithmetic, Cooperating techniques for solving nonlinear real arithmetic in the \texttt{cvc5} SMT solver (system description)
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- raSAT: an SMT solver for polynomial constraints
- Solving Non-linear Arithmetic
- Satisfiability of Non-linear (Ir)rational Arithmetic
- Interval arithmetic
- Algorithm 852
- Combined Decision Techniques for the Existential Theory of the Reals
- 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