2
$\begingroup$

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.

Improve this question
$\endgroup$
5
  • 1
    $\begingroup$ 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. $\endgroup$
    – Yoav Kallus
    Commented May 14, 2012 at 2:15
  • $\begingroup$ 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. $\endgroup$
    – Andreas Blass
    Commented May 14, 2012 at 10:19
  • $\begingroup$ Also, the OP is not looking for integers solutions, so this is general LP at worst (which is much easier). $\endgroup$
    – Igor Rivin
    Commented May 14, 2012 at 12:18
  • $\begingroup$ Ah. I thought "satisfiability with natural values" meant integer solutions were sought. $\endgroup$
    – Yoav Kallus
    Commented May 14, 2012 at 12:25
  • $\begingroup$ I am interested in natural (0 included) solutions only. $\endgroup$
    – Mark T
    Commented May 14, 2012 at 14:53

1 Answer 1

Reset to default
3
$\begingroup$

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.

Improve this answer
$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .