A generalised branch-and-bound approach and its application in SAT modulo nonlinear integer arithmetic

DOI10.1007/978-3-319-45641-6_21MaRDI QIDQ2830009zbMATH OpenOpenAlexFDO

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

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Polyhedral combinatorics, branch-and-bound, branch-and-cut (90C57)

Recommendations

• Solving nonlinear integer arithmetic with MCSAT
• Incomplete SMT techniques for solving non-linear formulas over the integers
• Solving non-linear arithmetic
• A practical approach to satisfiability modulo linear integer arithmetic
• Satisfiability of non-linear (ir)rational arithmetic

Cites work

• scientific article; zbMATH DE number 4089320 (Why is no real title available?)
• scientific article; zbMATH DE number 3177183 (Why is no real title available?)
• scientific article; zbMATH DE number 5263038 (Why is no real title available?)
• scientific article; zbMATH DE number 5493266 (Why is no real title available?)
• A machine program for theorem-proving
• A practical approach to satisfiability modulo linear integer arithmetic
• An improved projection operation for cylindrical algebraic decomposition of three-dimensional space
• Cylindrical Algebraic Decomposition I: The Basic Algorithm
• Efficient Term-ITE Conversion for Satisfiability Modulo Theories
• Improved projection for cylindrical algebraic decomposition
• Quantifier elimination for real algebra -- the quadratic case and beyond
• SAT Solving for Termination Analysis with Polynomial Interpretations
• Solving Non-linear Polynomial Arithmetic via SAT Modulo Linear Arithmetic
• Splitting on Demand in SAT Modulo Theories
• The MathSAT5 SMT solver
• Virtual substitution for SMT-solving
• \texttt{SMT-RAT}: an open source \texttt{C++} toolbox for strategic and parallel SMT solving
• raSAT: An SMT Solver for Polynomial Constraints

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}

Describes a project that uses

Uses Software

• raSAT
• SMT-RAT
• MathSAT5
• CVC4
• Boogie
• veriT
• z3
• Yices

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)