Skip to Main content Skip to Navigation

Decision Procedures for Linear Arithmetic

Martin Bromberger 1, 2
1 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
MPII - Max-Planck-Institut für Informatik, Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : In this thesis, we present new decision procedures for linear arithmetic in the context of SMT solvers and theorem provers: 1) CutSat++, a calculus for linear integer arithmetic that combines techniques from SAT solving and quantifier elimination in order to be sound, terminating, and complete. 2) The largest cube test and the unit cube test, two sound (although incomplete) tests that find integer and mixed solutions in polynomial time. The tests are especially efficient on absolutely unbounded constraint systems, which are difficult to handle for many other decision procedures. 3) Techniques for the investigation of equalities implied by a constraint system. Moreover, we present several applications for these techniques. 4) The Double-Bounded reduction and the Mixed-Echelon-Hermite transformation, two transformations that reduce any constraint system in polynomial time to an equisatisfiable constraint system that is bounded. The transformations are beneficial because they turn branch-and-bound into a complete and efficient decision procedure for unbounded constraint systems. We have implemented the above decision procedures (except for CutSat++) as part of our linear arithmetic theory solver SPASS-IQ and as part of our CDCL(LA) solver SPASS-SATT. We also present various benchmark evaluations that confirm the practical efficiency of our new decision procedures.
Document type :
Complete list of metadatas
Contributor : Stephan Merz <>
Submitted on : Friday, January 3, 2020 - 3:17:39 PM
Last modification on : Tuesday, January 7, 2020 - 1:50:51 AM
Long-term archiving on: : Monday, April 6, 2020 - 8:52:46 PM


Files produced by the author(s)


  • HAL Id : tel-02427371, version 1


Martin Bromberger. Decision Procedures for Linear Arithmetic. Logic in Computer Science [cs.LO]. Saarland University, 2019. English. ⟨tel-02427371⟩



Record views


Files downloads