A complete and terminating approach to linear integer solving - Archive ouverte HAL Access content directly
Journal Articles Journal of Symbolic Computation Year : 2020

A complete and terminating approach to linear integer solving

(1, 2) , (3, 2, 4, 1, 5) , (1, 2)
1
2
3
4
5

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.
Fichier principal
Vignette du fichier
authors_version.pdf (309 Ko) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

hal-02397168 , version 1 (23-11-2021)

Identifiers

Cite

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⟩
70 View
72 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More