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},
}