A Preprocessor for Linear Diophantine Equalities and Inequalities

René Thiemann 🌐

June 13, 2024

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

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.
In total, given some linear input constraints, the preprocessor will either detect unsatisfiability in \(\mathbb{Z}\), or it returns equi-satisfiable inequalities, which moreover are all strictly satisfiable in \(\mathbb{Q}\).

License

BSD 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

Session Linear_Diophantine_Preprocessor