Solving nonlinear integer arithmetic with MCSAT

DOI10.1007/978-3-319-52234-0_18MaRDI QIDQ2961575zbMATH OpenOpenAlexFDO

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

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

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

• scientific article; zbMATH DE number 42574 (Why is no real title available?)
• scientific article; zbMATH DE number 3349331 (Why is no real title available?)
• scientific article; zbMATH DE number 3068536 (Why is no real title available?)
• A generalised branch-and-bound approach and its application in SAT modulo nonlinear integer arithmetic
• A model-constructing satisfiability calculus
• A practical approach to satisfiability modulo linear integer arithmetic
• Cutting to the chase.
• On the complexity of integer programming
• Outline of an algorithm for integer solutions to linear programs
• Proving termination of programs automatically with AProVE
• Quantifier elimination for real algebra -- the quadratic case and beyond
• SAT Solving for Termination Analysis with Polynomial Interpretations
• Solving non-linear arithmetic
• Theory and Applications of Satisfiability Testing
• \texttt{SMT-RAT}: an open source \texttt{C++} toolbox for strategic and parallel SMT solving

Cited in

(19)

• A CDCL-style calculus for solving non-linear constraints
• 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
• Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings
• Incomplete SMT techniques for solving non-linear formulas over the integers
• 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
• Solving non-linear arithmetic
• Local Search For Satisfiability Modulo Integer Arithmetic Theories
• Satisfiability modulo finite fields
• Modular strategic SMT solving with \textbf{SMT-RAT}

Describes a project that uses

Uses Software

• SMT-RAT
• CVC4
• AProVE
• Chaff
• z3
• Yices
• SMT-LIB
• MiniSat

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)