Solving nonlinear integer arithmetic with MCSAT
From MaRDI portal
Publication:2961575
DOI10.1007/978-3-319-52234-0_18zbMATH Open1484.68220OpenAlexW2571168937MaRDI QIDQ2961575FDOQ2961575
Authors: Dejan Jovanović 
Publication date: 21 February 2017
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-319-52234-0_18
Recommendations
- Solving non-linear arithmetic
- Experimenting on solving nonlinear integer arithmetic with incremental linearization
- A generalised branch-and-bound approach and its application in SAT modulo nonlinear integer arithmetic
- Incomplete SMT techniques for solving non-linear formulas over the integers
- Interpolation and model checking for nonlinear arithmetic
Cites Work
- Theory and Applications of Satisfiability Testing
- \texttt{SMT-RAT}: an open source \texttt{C++} toolbox for strategic and parallel SMT solving
- Outline of an algorithm for integer solutions to linear programs
- Title not available (Why is that?)
- Title not available (Why is that?)
- Solving non-linear arithmetic
- A model-constructing satisfiability calculus
- Cutting to the chase.
- On the complexity of integer programming
- Quantifier elimination for real algebra -- the quadratic case and beyond
- A practical approach to satisfiability modulo linear integer arithmetic
- SAT Solving for Termination Analysis with Polynomial Interpretations
- Title not available (Why is that?)
- A generalised branch-and-bound approach and its application in SAT modulo nonlinear integer arithmetic
- Proving termination of programs automatically with AProVE
Cited In (19)
- Verifying Whiley programs with Boogie
- Optimization modulo non-linear arithmetic via incremental linearization
- Interpolation and model checking for nonlinear arithmetic
- Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs
- Minimal-model-guided approaches to solving polynomial constraints and extensions
- Levelwise construction of a single cylindrical algebraic cell
- A generalised branch-and-bound approach and its application in SAT modulo nonlinear integer arithmetic
- Incomplete SMT techniques for solving non-linear formulas over the integers
- Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings
- Solving bitvectors with MCSAT: explanations from bits and pieces
- Conflict-driven satisfiability for theory combination: transition system and completeness
- Satisfiability of non-linear (ir)rational arithmetic
- Experimenting on solving nonlinear integer arithmetic with incremental linearization
- Deciding Bit-Vector Formulas with mcSAT
- Local Search For Satisfiability Modulo Integer Arithmetic Theories
- Solving non-linear arithmetic
- Satisfiability modulo finite fields
- Modular strategic SMT solving with \textbf{SMT-RAT}
- A CDCL-style calculus for solving non-linear constraints
Uses Software
This page was built for publication: Solving nonlinear integer arithmetic with MCSAT
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2961575)
