MathOverflow is a question and answer site for professional mathematicians. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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

share|cite|improve this question
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
up vote 3 down vote accepted

This looks very much like the "difference constraints" that are explored in the big white textbook "Introduction to Algorithms" by Cormen, Leiserson, Rivest and Stein. The graph seems about the same and there is a theorem about negative weight cycles. I suggest you will find what you need there.

share|cite|improve this answer

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.