A complete and terminating approach to linear integer solving
DOI10.1016/j.jsc.2019.07.021zbMath1432.68597OpenAlexW2966563153WikidataQ127434706 ScholiaQ127434706MaRDI QIDQ2307624
Christoph Weidenbach, Martin Bromberger, Thomas Sturm
Publication date: 24 March 2020
Published in: Journal of Symbolic Computation (Search for Journal in Brave)
Full work available at URL: https://hal.inria.fr/hal-02397168/file/authors_version.pdf
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 (1)
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- The complexity of almost linear diophantine problems
- Weak quantifier elimination for the full linear theory of the integers
- Deciding effectively propositional logic using DPLL and substitution sets
- The complexity of logical theories
- The complexity of Presburger arithmetic with bounded quantifier alternation depth
- A \(2^{2^{2^{pn}}}\) upper bound on the complexity of Presburger arithmetic
- The computational complexity of logical theories
- Refutational theorem proving for hierarchic first-order theories
- Superposition as a decision procedure for timed automata
- Cutting to the chase.
- Automated model building
- NRCL - A Model Building Approach to the Bernays-Schönfinkel Fragment
- Automated Reasoning Building Blocks
- Linear Integer Arithmetic Revisited
- Solving SAT and SAT Modulo Theories
- Cuts from Proofs: A Complete and Practical Technique for Solving Linear Inequalities over Integers
- 50 Years of Integer Programming 1958-2008
- On the complexity of integer programming
- A Decision Procedure for the First Order Theory of Real Addition with Order
- A Bound on Solutions of Linear Integer Equalities and Inequalities
- Hierarchic Superposition with Weak Abstraction
- Cutting to the Chase Solving Linear Integer Arithmetic
- The MathSAT5 SMT Solver
- Splitting on Demand in SAT Modulo Theories
This page was built for publication: A complete and terminating approach to linear integer solving
