Linear Integer Arithmetic Revisited

DOI10.1007/978-3-319-21401-6_42zbMath1432.68596arXiv1503.02948OpenAlexW4299514408MaRDI QIDQ3454126

Christoph Weidenbach, Martin Bromberger, Thomas Sturm

Publication date: 2 December 2015

Published in: Automated Deduction - CADE-25 (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1503.02948

zbMATH Keywords

linear programminglinear arithmeticinteger arithmeticSATSMTDPLL

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Integer programming (90C10) Specification and verification (program logics, model checking, etc.) (68Q60) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Computational aspects of satisfiability (68R07)

Related Items

Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs ⋮ Linear Integer Arithmetic Revisited ⋮ New techniques for linear arithmetic: cubes and equalities ⋮ A conflict-driven solving procedure for poly-power constraints ⋮ $$\mathsf {SC}^\mathsf{2} $$ : Satisfiability Checking Meets Symbolic Computation ⋮ Fast Cube Tests for LIA Constraint Solving ⋮ SPASS-SATT. A CDCL(LA) solver ⋮ SCL clause learning from simple models ⋮ A complete and terminating approach to linear integer solving

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Weak quantifier elimination for the full linear theory of the integers
• Termination of term rewriting using dependency pairs
• Cutting to the chase.
• Strongly mixing g-measures
• Linear Integer Arithmetic Revisited
• Cuts from Proofs: A Complete and Practical Technique for Solving Linear Inequalities over Integers
• 50 Years of Integer Programming 1958-2008
• Complete Sets of Reductions for Some Equational Theories
• Splitting on Demand in SAT Modulo Theories