A Preprocessor for Linear Diophantine Equalities and Inequalities
René ThiemannArchive of Formal Proofs 2024.
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 Z, or it returns equi-satisfiable inequalities,
which moreover are all strictly satisfiable in Q.
BibTeX
@article{Linear_Diophantine_Preprocessor-AFP, author = {René Thiemann}, title = {A Preprocessor for Linear Diophantine Equalities and Inequalities}, journal = {Archive of Formal Proofs}, month = {June}, year = {2024}, note = {\url{https://isa-afp.org/entries/Linear_Diophantine_Preprocessor.html}, Formal proof development}, ISSN = {2150-914x}, }