Linear integer arithmetic revisited

DOI10.1007/978-3-319-21401-6_42MaRDI QIDQ3454126zbMATH OpenOpenAlexFDO

Authors Martin Bromberger, Thomas Sturm, Christoph Weidenbach

Publication date 2 December 2015

Published in Automated Deduction - CADE-25 (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1503.02948

zbMATH Keywords

DPLLinteger arithmeticlinear arithmeticlinear programmingSATSMT

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Computational aspects of satisfiability (68R07) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Symbolic computation and algebraic computation (68W30) Integer programming (90C10)

Abstract: We consider feasibility of linear integer programs in the context of verification systems such as SMT solvers or theorem provers. Although satisfiability of linear integer programs is decidable, many state-of-the-art solvers neglect termination in favor of efficiency. It is challenging to design a solver that is both terminating and practically efficient. Recent work by Jovanovic and de Moura constitutes an important step into this direction. Their algorithm CUTSAT is sound, but does not terminate, in general. In this paper we extend their CUTSAT algorithm by refined inference rules, a new type of conflicting core, and a dedicated rule application strategy. This leads to our algorithm CUTSAT++, which guarantees termination.

Recommendations

• A complete and terminating approach to linear integer solving
• Cutting to the chase. Solving linear integer arithmetic
• Cuts from Proofs: A Complete and Practical Technique for Solving Linear Inequalities over Integers
• A practical approach to satisfiability modulo linear integer arithmetic
• Cuts from proofs: a complete and practical technique for solving linear inequalities over integers

Cites work

• 50 Years of Integer Programming 1958-2008
• A practical approach to satisfiability modulo linear integer arithmetic
• Complete Sets of Reductions for Some Equational Theories
• Cuts from Proofs: A Complete and Practical Technique for Solving Linear Inequalities over Integers
• Cutting to the chase.
• scientific article; zbMATH DE number 3501006 (Why is no real title available?)
• scientific article; zbMATH DE number 3408928 (Why is no real title available?)
• Linear integer arithmetic revisited
• Splitting on Demand in SAT Modulo Theories
• Strongly mixing g-measures
• Termination of term rewriting using dependency pairs
• Weak quantifier elimination for the full linear theory of the integers

Cited in

(14)

• New techniques for linear arithmetic: cubes and equalities
• Cutting the mix
• A conflict-driven solving procedure for poly-power constraints
• SPASS-SATT. A CDCL(LA) solver
• SCL clause learning from simple models
• A complete and terminating approach to linear integer solving
• \textsf{SC}\(^2\): satisfiability checking meets symbolic computation. (Project paper)
• Fast cube tests for LIA constraint solving
• Linear integer arithmetic revisited
• Cuts from proofs: a complete and practical technique for solving linear inequalities over integers
• Rewrite systems for integer arithmetic
• Cutting to the chase. Solving linear integer arithmetic
• Constraint answer set programming: integrational and translational (or SMT-based) approaches
• Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs

This page was built for publication: Linear integer arithmetic revisited

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3454126)