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

Depends on

Cite

× 
@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},
}
Download

Download

× Download latest