2
$\begingroup$

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.

$\endgroup$
  • 2
    $\begingroup$ 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. $\endgroup$ – Tyson Williams Apr 12 '13 at 12:04
  • $\begingroup$ That sounds plausible, I'll think about it! If that's correct, is there a nice way to treat those 'hybrid' graphs? $\endgroup$ – rostayob Apr 12 '13 at 12:09
  • 1
    $\begingroup$ 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. $\endgroup$ – rostayob Apr 12 '13 at 13:01
  • 1
    $\begingroup$ The variables don't 'represent' anything concrete initially. I only need to derive some ordering from the constraints that I have. $\endgroup$ – rostayob Apr 12 '13 at 13:57
  • 1
    $\begingroup$ 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. $\endgroup$ – András Salamon Apr 13 '13 at 9:13
2
$\begingroup$

You may find it helpful to think of your problem in terms of equalities and strict inequalities.

In the case of the constraints being equalities or disequalities there is a simple saturation procedure based on transitivity of equality. Strict inequalities can be represented by directed edges in a graph. You can then compute strongly connected components to reason about dependencies between sets of variables. If you have uninterpreted functions, you can use congruence closure.

I would imagine that the first results date to the 50s or at least the 70s, but I do not have a good reference for you. Recent literature in which these ideas occur is the paper below.

An Interpolating Decision Procedure for Transitive Relations with Uninterpreted Functions, Georg Weissenbacher.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.