A complete and terminating approach to linear integer solving

摘要

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. (c) 2019 Elsevier Ltd. All rights reserved.