A complete and terminating approach to linear integer solving

Martin Bromberger (1, 2) , Thomas Sturm (3, 2, 4, 1, 5) , Christoph Weidenbach (1, 2)

1 MPII - Max-Planck-Institut für Informatik
2 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
3 CNRS - Centre National de la Recherche Scientifique
4 MOSEL - Proof-oriented development of computer-based systems
5 Saarland University [Saarbrücken]

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.

Mots clés: Linear arithmetic; SMT; SAT; CDCL; Linear programming; Integer arithmetic

Domaines: Informatique [cs]; Logique en informatique [cs.LO]

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