A Generalised Branch-and-Bound Approach and Its Application in SAT Modulo Nonlinear Integer Arithmetic
From MaRDI portal
Publication:2830009
DOI10.1007/978-3-319-45641-6_21zbMath1453.90186OpenAlexW2512649355MaRDI QIDQ2830009
Gereon Kremer, Erika Ábrahám, Florian Corzilius
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
Polyhedral combinatorics, branch-and-bound, branch-and-cut (90C57) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)
Related Items
Optimization modulo non-linear arithmetic via incremental linearization, Modular strategic SMT solving with \textbf{SMT-RAT}, Local Search For Satisfiability Modulo Integer Arithmetic Theories, Experiments with automated reasoning in the class, Solving Nonlinear Integer Arithmetic with MCSAT, Fully incremental cylindrical algebraic decomposition, Verifying Whiley programs with Boogie
Uses Software
Cites Work
- Quantifier elimination for real algebra -- the quadratic case and beyond
- An improved projection operation for cylindrical algebraic decomposition of three-dimensional space
- raSAT: An SMT Solver for Polynomial Constraints
- Virtual Substitution for SMT-Solving
- SMT-RAT: An Open Source C++ Toolbox for Strategic and Parallel SMT Solving
- SAT Solving for Termination Analysis with Polynomial Interpretations
- Efficient Term-ITE Conversion for Satisfiability Modulo Theories
- Cylindrical Algebraic Decomposition I: The Basic Algorithm
- Solving Non-linear Polynomial Arithmetic via SAT Modulo Linear Arithmetic
- The MathSAT5 SMT Solver
- Splitting on Demand in SAT Modulo Theories
- A machine program for theorem-proving
- Improved projection for cylindrical algebraic decomposition
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
