Linear Integer Arithmetic Revisited
From MaRDI portal
Publication:3454126
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
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