System of linear diophantine inequalites

Question

are there any papers that deal with System of linear diophantine inequalites? I have a hard time finding any. The wikipedia entry calls it diophantine approximation, but i am not sure if this is the same. Do you know any literature/paper that deals with inequalities?

Answer 1

Diophantine inequalities are dealt with under the topic of "integer programming", under the sub-topic of satisfiability/feasibility, i.e. you don't have an objective function to deal with. Note that just solving linear inequalities over $\mathbb{Z}$ is NP-complete.

A broad overview although it might be a bit dated is in the citation I added to Wikipedia a while back on this issue (for inequalities in particular see sections 3.2 to 3.7 of the paper/chapter):

• Alexander Bockmayr, Volker Weispfenning (2001). "Solving Numerical Constraints". In John Alan Robinson and Andrei Voronkov. Handbook of Automated Reasoning Volume I. Elsevier and MIT Press. ISBN 0-444-82949-0 (Elsevier) ISBN 0-262-18221-1 (MIT Press).

If you need more specialized papers, let me know.

EDIT: I don't really know what you're after, but if you just want something newer, see Dillig et. al (2011) "Cuts from Proofs" -> free copy.

EDIT2: There is always a finite parametric description of the solutions over $\mathbb{Z}$ even when the solution itself is infinite. However, this last question is actually not so trivial in terms of listing relevant literature. There is a large amount of literature on finding the Hilbert basis for the solution of linear inequalities over $\mathbb{N}$; this focus is due to practical applications. Finding a Hilbert basis over $\mathbb{Z}$ has received much less attention, but see Chubarov and Voronkov (2005). They use the Hilbert basis for nonnegative intergers as building block. They consider only matrices with integer coefficients though.

Note that Hilbert bases for linear integer inequalities, while guaranteed to be finite can be huge: doubly exponential in the number of the original system's variables in the worst case. So a notion of incremental solvers was developed, which gives back a (specified) numbers of extra vectors starting with a previous (partial) solution. These incremental solvers are useful for testing entailment of two systems of inequalities. There's in fact not much in the way of practical applications for listing whole Hilbert bases.