Skip to Main content Skip to Navigation
Journal articles

A complete and terminating approach to linear integer solving

Martin Bromberger 1, 2 Thomas Sturm 3, 1, 4, 2 Christoph Weidenbach 1, 2
2 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
LORIA - FM - Department of Formal Methods , Inria Nancy - Grand Est, MPII - Max-Planck-Institut für Informatik
4 MOSEL - Proof-oriented development of computer-based systems
LORIA - FM - Department of Formal Methods
Abstract : We consider feasibility of linear integer problems in the context of verification systems such as SMT solvers or theorem provers. Although satisfiability of linear integer problems is decidable, many state-of-the-art implementations neglect termination in favor of efficiency. We present the calculus CutSat++ that is sound, terminating, complete, and leaves enough space for model assumptions and simplification rules in order to be efficient in practice. CutSat++ combines model-driven reasoning and quantifier elimination to the feasibility of linear integer problems.
Complete list of metadata
Contributor : Thomas Sturm Connect in order to contact the contributor
Submitted on : Tuesday, November 23, 2021 - 1:14:56 PM
Last modification on : Wednesday, November 24, 2021 - 10:23:07 AM


Files produced by the author(s)




Martin Bromberger, Thomas Sturm, Christoph Weidenbach. A complete and terminating approach to linear integer solving. Journal of Symbolic Computation, Elsevier, 2020, 100, pp.102-136. ⟨10.1016/j.jsc.2019.07.021⟩. ⟨hal-02397168⟩



Record views


Files downloads