Solving Nonlinear Integer Arithmetic with MCSAT
From MaRDI portal
Publication:2961575
DOI10.1007/978-3-319-52234-0_18zbMath1484.68220OpenAlexW2571168937MaRDI QIDQ2961575
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
Related Items
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 ⋮ Modular strategic SMT solving with \textbf{SMT-RAT} ⋮ Local Search For Satisfiability Modulo Integer Arithmetic Theories ⋮ Levelwise construction of a single cylindrical algebraic cell ⋮ Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings ⋮ Conflict-driven satisfiability for theory combination: transition system and completeness ⋮ Solving bitvectors with MCSAT: explanations from bits and pieces ⋮ Verifying Whiley programs with Boogie
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Quantifier elimination for real algebra -- the quadratic case and beyond
- Cutting to the chase.
- A Generalised Branch-and-Bound Approach and Its Application in SAT Modulo Nonlinear Integer Arithmetic
- Solving Non-linear Arithmetic
- A Model-Constructing Satisfiability Calculus
- Proving Termination of Programs Automatically with AProVE
- Outline of an algorithm for integer solutions to linear programs
- SMT-RAT: An Open Source C++ Toolbox for Strategic and Parallel SMT Solving
- SAT Solving for Termination Analysis with Polynomial Interpretations
- On the complexity of integer programming
- Theory and Applications of Satisfiability Testing
This page was built for publication: Solving Nonlinear Integer Arithmetic with MCSAT
