A complete and terminating approach to linear integer solving. (September 2020)

• Record Type: Journal Article
• Authors: Bromberger, Martin; Sturm, Thomas; Weidenbach, Christoph
• Is Part Of: Journal of symbolic computation. Volume 100(2020)
• Page Start: 102
• Page End: 136
• Publication Date: 2020-09
• Subjects: Linear arithmetic -- SMT -- SAT -- CDCL -- Linear programming -- Integer arithmetic; Mathematics -- Data processing -- Periodicals; Numerical analysis -- Data processing -- Periodicals; Automatic programming (Computer science) -- Periodicals; Mathématiques -- Informatique -- Périodiques; Analyse numérique -- Informatique -- Périodiques; Programmation automatique -- Périodiques; Automatic programming (Computer science); Mathematics -- Data processing; Numerical analysis -- Data processing; Periodicals; Electronic journals; 510.285
• DOI: 10.1016/j.jsc.2019.07.021
• Languages: English
• ISSNs: 0747-7171

Abstract

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.