# Verifying consistency of strict and non-strict partial orders constraints

I am building a set of constraints of the kind $x < y$ and $x \leq y$, where $<$ is a strict order and $\leq$ is a non-strict order on the same set, and $x$ and $y$ are abstract variables representing elements of the set. The laws that relate the two orderings are the same as $<$ and $\leq$ for integers. I need to make sure that each constraint that I add does not make the set inconsistent (e.g. adding $x < y$ and then $y < x$ I'd get an error).

Now, if I had only the $<$ constraints I could get away with generating a graph and then doing a topological sort, or with disjoint-sets. The problem is that I'm not sure how to handle the additional $\leq$ constraints.

One idea is to express $x \leq y$ as $\neg (x > y)$, and to keep two graphs: one for the actual $<$ relations and one for the negated ones. Then we'd need to check, at each new constraints, whether there are overlapping paths between the two graphs, in which case we'd have a problem. However this seems rather costly since it seems to me that we'd need to analyze all the pairs each time.

Another idea would be to 'collapse' $\leq$ relations to equalities or $<$ when needed, but again I'm quite uncertain on the details.

Is this problem described somewhere? As a bonus, I'd like the data structures involved to be purely functional.

• If your graph has one type of edge for < and another type for $\le$, then I think an inconsistency is equivalent to a cycle that contains at least one edge of the first type. – Tyson Williams Apr 12 '13 at 12:04
• That sounds plausible, I'll think about it! If that's correct, is there a nice way to treat those 'hybrid' graphs? – bitonic Apr 12 '13 at 12:09
• I still don't get how you are proposing to solve the problem. Obviously if $x \leq y$ and $y \leq x$ then I can derive $x = y$, which is basically what I suggest when I say 'Another idea would be to...'. The problem is that you don't have any information about the variables themselves so you need to be careful to convert the $\leq$ constraint to an equality or a $<$ when you have the right constraints to do so. – bitonic Apr 12 '13 at 13:01
• The variables don't 'represent' anything concrete initially. I only need to derive some ordering from the constraints that I have. – bitonic Apr 12 '13 at 13:57
• You are describing a structure with three relations $x\le y$, $x < y$, and $x=y$. When $x < y$ then also $x \le y$, and when $x=y$ then $x \le y$. The transitive closure of $\le$ then gives you a directed graph (with variables as vertices) that represents a preorder (check Wikipedia). Any strongly connected components in this closure graph represent variables that are all equal. If you see $x < y$ and $x = y$ then you have an inconsistency, and if this does not occur then your system is consistent. – András Salamon Apr 13 '13 at 9:13