Skip to Main content Skip to Navigation
Theses

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 :
Theses
Complete list of metadatas

https://hal.inria.fr/tel-02427371
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

File

thesis_v20191212.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : tel-02427371, version 1

Citation

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

Share

Metrics

Record views

155

Files downloads

220