raSAT: An SMT Solver for Polynomial Constraints

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

Mathematics Subject Classification ID

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

• MiniSat
• RSOLVER
• RealPaver
• dReal
• SMT-RAT
• raSAT

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