Skip to Main content Skip to Navigation
New interface
Journal articles

New Techniques for Linear Arithmetic: Cubes and Equalities

Martin Bromberger 1, 2 Christoph Weidenbach 3, 2 
2 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 : We present several new techniques for linear arithmetic constraint solving. They are all based on the linear cube transformation, a method presented here, which allows us to efficiently determine whether a system of linear arithmetic constraints contains a hypercube of a given edge length. Our first findings based on this transformation are two sound tests that find integer solutions for linear arithmetic constraints. While many complete methods search along the problem surface for a solution, these tests use cubes to explore the interior of the problems. The tests are especially efficient for constraints with a large number of integer solutions, e.g., those with infinite lattice width. Inside the SMT-LIB benchmarks, we have found almost one thousand problem instances with infinite lattice width. Experimental results confirm that our tests are superior on these instances compared to several state-of-the-art SMT solvers. We also discovered that the linear cube transformation can be used to investigate the equalities implied by a system of linear arithmetic constraints. For this purpose, we developed a method that computes a basis for all implied equalities, i.e., a finite representation of all equalities implied by the linear arithmetic constraints. The equality basis has several applications. For instance, it allows us to verify whether a system of linear arithmetic constraints implies a given equality. This is valuable in the context of Nelson-Oppen style combinations of theories.
Document type :
Journal articles
Complete list of metadata

Cited literature [29 references]  Display  Hide  Download
Contributor : Stephan Merz Connect in order to contact the contributor
Submitted on : Tuesday, December 5, 2017 - 3:58:13 PM
Last modification on : Friday, July 8, 2022 - 10:07:00 AM


Files produced by the author(s)




Martin Bromberger, Christoph Weidenbach. New Techniques for Linear Arithmetic: Cubes and Equalities. Formal Methods in System Design, 2017, 51 (3), pp.433-461. ⟨10.1007/s10703-017-0278-7⟩. ⟨hal-01656397⟩



Record views


Files downloads