A generalised branch-and-bound approach and its application in SAT modulo nonlinear integer arithmetic
DOI10.1007/978-3-319-45641-6_21zbMATH Open1453.90186OpenAlexW2512649355MaRDI QIDQ2830009FDOQ2830009
Authors: Gereon Kremer, Florian Corzilius, Erika Ábrahám 
Publication date: 9 November 2016
Published in: Computer Algebra in Scientific Computing (Search for Journal in Brave)
Full work available at URL: http://publications.rwth-aachen.de/record/670551/files/670551.pdf
Recommendations
Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Polyhedral combinatorics, branch-and-bound, branch-and-cut (90C57)
Cites Work
- \texttt{SMT-RAT}: an open source \texttt{C++} toolbox for strategic and parallel SMT solving
- The MathSAT5 SMT solver
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Splitting on Demand in SAT Modulo Theories
- A machine program for theorem-proving
- An improved projection operation for cylindrical algebraic decomposition of three-dimensional space
- Improved projection for cylindrical algebraic decomposition
- Quantifier elimination for real algebra -- the quadratic case and beyond
- A practical approach to satisfiability modulo linear integer arithmetic
- Cylindrical Algebraic Decomposition I: The Basic Algorithm
- Title not available (Why is that?)
- SAT Solving for Termination Analysis with Polynomial Interpretations
- Solving Non-linear Polynomial Arithmetic via SAT Modulo Linear Arithmetic
- Efficient Term-ITE Conversion for Satisfiability Modulo Theories
- raSAT: An SMT Solver for Polynomial Constraints
- Virtual substitution for SMT-solving
Cited In (8)
- Verifying Whiley programs with Boogie
- Optimization modulo non-linear arithmetic via incremental linearization
- Solving nonlinear integer arithmetic with MCSAT
- Incomplete SMT techniques for solving non-linear formulas over the integers
- Fully incremental cylindrical algebraic decomposition
- Local Search For Satisfiability Modulo Integer Arithmetic Theories
- Experiments with automated reasoning in the class
- Modular strategic SMT solving with \textbf{SMT-RAT}
Uses Software
This page was built for publication: A generalised branch-and-bound approach and its application in SAT modulo nonlinear integer arithmetic
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2830009)
