Efficiently generating rankings from (in)equalities

Question

I have a bunch of constraints, each consisting of two symbols and a comparison operator: <, <=, !=, ==, >=, or >. So, for example:

A <= B
C >= B
A != C
C == D
D > E

I want to be able to do three things:

1. First, I want to check if there are any inconsistencies. So, for example, if I have A > B, B > C, and A == C, there's an inconsistency, as A must be both equal to C and greater than it.
2. I want to be able to query any two symbols, and get back the feasible relative ordering(s) between them. So for example query(A, C) should return {<} (a set consisting of a single element: less than), and query(B, E) should return {<, =, >}.
3. I want to be able to add a constraint (this could also add (an) additional symbol(s), for example adding F == G to the above example).

Queries are more common than adding constraints.

I've already come up with a method that works if you do not have any != constraints:

1. Translate every constraint into one(s) that only use(s) < or <= (So: X == Y turns into X <= Y and Y <= X, X > Y turns into Y < X, etc.).
2. Build a directed graph with the symbols, using the constraints as edges.
3. For all cycles in the graph, if the cycle includes at least one < edge, there is a contradiction.

To query(X, Y):

1. Find any path between X and Y.
   • If there is no such path, the result of this part is {<, =, >}.
   • If the path contains at least one <, the result of this part is {<}.
   • Otherwise, the result of this part is {<, =}.
2. Find any path between Y and X
   • If there is no such path, the result of this part is {<, =, >}.
   • If the path contains at least one <, the result of this part is {>}.
   • Otherwise, the result of this part is {=, >}.
3. The result is the union of the above two results.

(Obviously, I can cache the queries, at least until I add another constraint)

I can extend this to include !=, but then it becomes exponentially slower w.r.t. the number of constraints that use !=. (Keep a set of graphs instead of one. Every time you add a constraint with !=, for each graph in the set replace it with two copies, one where the constraint to be added is <, one where it is >. Any time one produces a contradiction, discard it. If the set of graphs is empty, there is a contradiction. On a query, check all graphs, unioning the answers together.)

So, is there a more efficient way to solve this problem? Or is it going to be exponential-time worst case regardless?

I am aware that I could use a SAT solver for this, but it seems a mite overkill, to put it mildly, especially as I cannot see it ever exceeding 100 constraints, with 10 being more typical.

(For those interested in what this came out of, I am working on a toy programming language and became interested in the idea of making custom infix operators, where priority is decided by relation to existing operators instead of a straight numerical value (which has issues when you want to add a new operator with higher priority than A but lower than B, but there is no gap between the two. != is not strictly required for that problem, but I became interested in how one would include it.)

Answer 1

There's some lovely mathematics to the effect that, unless you can prove that A <= B and B <= A using reflexivity and transitivity, there exists a model where A != B. The forced equality classes on variables correspond one-to-one with the strongly connected components of the graph of <=-related variables (where A = B induces A <= B and B <= A).

In total, the algorithm for determining feasibility is to extract all of the <= constraints (where A < B induces A <= B, and A = B induces A <= B and B <= A, and A != B induces nothing), find strong components in the directed graph, then verify, for every A < B and A != B, that A and B lie in different strong components. To query, add each possibility in turn and check feasibility.