# Algorithm for satisfiability of inequalities.

I am looking for an algorithm for checking the satisfiability (with natural values) of a set of inequalities made of variables and natural numbers, for example: $u < v, u \leq z, 3 \leq v$.

In this paper, http://boole.stanford.edu/pub/sefnp.pdf , there's the following claim in the second page:

"Then the conjunction is satisfiable if and only if the graph contains a cycle of positive weight, i.e., one whose labels add up to a positive integer."

The graph it mentions consists of a node for each variable in the inequalities, plus one extra node for the number $0$. Then, for each inequality, we add an edge from node $x$ to node $y$ with weight $i$ if the inequality is written as $x + i \leq y$.

Is the claim true? I can't work out any example, indeed, I think that what makes sense is exactly the opposite: the conjunction is not satisfiable if and only if the graph contains a cycle of positive weight. (it would mean that $u + k \leq u$ for some node $u$ with positive $k$).

Btw, any other algorithm regarding this problem is welcome.

-
The problem you describe in the first paragraph is an integer linear program (albeit without an objective). There are many algorithms developed for solving these. – Yoav Kallus May 14 '12 at 2:15
This looks much easier than general integer linear programming, because these inequalities have, on each side, just a single variable or a constant. That's what makes characterizations in terms of positive (or negative) cycles possible. I think the OP is right in the belief that the quoted characterization is missing a "not" before "satisfiable". In fact, this should work somewhat more generally, namely when each side of each inequality involves at most one variable plus at most one constant. The graph (and its paths) keep track of how much smaller one variable must be than another. – Andreas Blass May 14 '12 at 10:19
Also, the OP is not looking for integers solutions, so this is general LP at worst (which is much easier). – Igor Rivin May 14 '12 at 12:18
Ah. I thought "satisfiability with natural values" meant integer solutions were sought. – Yoav Kallus May 14 '12 at 12:25
I am interested in natural (0 included) solutions only. – Mark T May 14 '12 at 14:53