Cuts from proofs: a complete and practical technique for solving linear inequalities over integers

DOI10.1007/s10703-011-0127-zzbMath1250.90057OpenAlexW2027402438MaRDI QIDQ453505

Thomas Dillig, Isil Dillig, Alex Aiken

Publication date: 27 September 2012

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10703-011-0127-z

zbMATH Keywords

algorithmsconstraint solvinglinear inequalities over integers

Mathematics Subject Classification ID

Integer programming (90C10) Linear programming (90C05)

Related Items (4)

\textsc{Diffy}: inductive reasoning of array programs using difference invariants ⋮ Data abstraction: a general framework to handle program verification of data structures ⋮ Lemmaless induction in trace logic ⋮ A Survey of Satisfiability Modulo Theory

Uses Software

• gmp
• Yices
• GLPK
• cvc3
• z3

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Hermite Normal Form Computation Using Modulo Determinant Arithmetic
• Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory
• Efficient Craig Interpolation for Linear Diophantine (Dis)Equations and Linear Modular Equations
• Deciding Quantifier-Free Presburger Formulas Using Parameterized Solution Bounds
• Tools and Algorithms for the Construction and Analysis of Systems

This page was built for publication: Cuts from proofs: a complete and practical technique for solving linear inequalities over integers