### Abstract

We formalize a combination algorithm to preprocess a set of linear
diophantine equations and inequalities. It consists of three techniques that are applied
exhaustively.

- Pugh's technique of tightening linear inequalities,
- Bromberger and Weidenbach's algorithm to detect implicit equalities – here we make use of an incremental implementation of the simplex algorithm, and
- Griggio's diophantine equation solver to eliminate all detected equations.

### License

### Topics

### Related publications

- Bromberger, M., & Weidenbach, C. (2017). New techniques for linear arithmetic: cubes and equalities. Formal Methods in System Design, 51(3), 433–461. https://doi.org/10.1007/s10703-017-0278-7
- Griggio, A. (2012). A Practical Approach to Satisfiability Modulo Linear Integer Arithmetic. Journal on Satisfiability, Boolean Modeling and Computation, 8(1–2), 1–27. https://doi.org/10.3233/sat190086