Let $\{x_1, ..., x_n\}$ be a set of $n$ distinct variables, and suppose given a finite set of $m$ inequalities such that, for all $1 \leq i \leq n$, the $i$-th inequality is of the form: $$y_i + a_i \leq z_i + b_i$$ where $y_i,z_i \in \{x_1,...,x_n\}$ are variables and $a_i, b_i \in \mathbb{Z}_{\geq 0}$ are non-negative integers.
Problem: To decide whether the set of inequalities can be satisfied by assigning integer values to all the variables ($x_i \in \mathbb{Z}$ for all $i$).
Question: Can the problem be decided in polynomial time?
Idea: Consider the directed multigraph whose nodes are the variables $\{x_1,...,x_n\}$ and there is an edge $y_i \to z_i$ of weight $b_i - a_i$ associated to the $i$-th equation. Conjecture: the inequalities can be satisfied if and only if the graph has no directed cycles of negative weight. For the 'only if' direction note that having a cycle of negative weight means that $x_j \leq x_j - k$ for some variable $x_j$ and $k > 0$. I have no idea whether 'if' direction holds, or how to prove it.
Note: I encountered this problem when attempting to solve constraints imposed by a type inference mechanism dealing with expressions that may belong to different "levels".