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:
- 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.
- 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 {<, =, >}
.
- 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:
- 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.).
- Build a directed graph with the symbols, using the constraints as edges.
- For all cycles in the graph, if the cycle includes at least one
<
edge, there is a contradiction.
To query(X, Y)
:
- 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
{<, =}
.
- 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
{=, >}
.
- 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.)