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.

Improve this question
$\endgroup$
13
  • 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, 2013 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$
    – user15617
    Apr 12, 2013 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$
    – user15617
    Apr 12, 2013 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$
    – user15617
    Apr 12, 2013 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, 2013 at 9:13

1 Answer 1

Reset to default
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.

Improve this answer
$\endgroup$
0

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.