Algebra for min/max bounds

Question

I am trying to model some set operations which are only well-defined if one is a subset of the other. The way the sets are constructed, I'll have a series of constraints of the form $x \subseteq y$, including the two sets in question and some other ones too. I won't know anything about individual element membership, so need to operate at the set level, and would like to be able to determine whether $a \subseteq b$ is implied by the given constraints.

This sounds like the sort of thing that's been studied before (e.g., for SMT solvers or linear programming), but I can't seem to hit the right keywords to search on. Are there known efficient representations/algorithms for this sort of problem?

---

Here's what I've roughly thought of doing:

type Set = Symbol;
type Bound = {kind: 'upper' | 'lower', arg: Set};
type Constraint = {kind: 'lt' | 'gt', arg: Bound};

const max = (b1: Bound, b2: Bound): Bound => ...;
const min = (b1: Bound, b2: Bound): Bound => ...;
const checker = (a: Constraint, b: Constraint): bool => ...;

My idea would be to build two Constraints, one for $a$ and one for $b$. $a$ would have a lt constraint and $b$ would have a gt constraint. I suspect Bound forms an algebra with max and min, which would allow me to put two Bounds in quasi-canonical form and break things down that way.

I'm not certain this will work, so before I spend several hours fleshing this out figured I'd ask if this had been solved before!

Answer 1

After posting the above I realized there was a possible solution with a different model. By viewing sets as nodes in a directed graph and edges as constraints, where $x \subseteq y$ would be translated to x -> y, the final checker would simply look for a path between $a$ and $b$ in this graph. (Using DFS or BFS per this SO question).

Answer 2

You can identify each set $A$ with a unary predicate $A(x)$. For example, the constraints $A \subseteq B$ and $B \subseteq C$ correspond to the constraints $$ \forall x \, A(x) \to B(x) \\ \forall x \, B(x) \to C(x) $$ Suppose we want to understand whether these constraints imply $A \subseteq C$, that is $$\forall x \, A(x) \to C(x)$$ This holds if for every particular element $x$, $$ (A(x) \to B(x) \land B(x) \to C(x)) \Rightarrow (A(x) \to C(x)) $$ To check whether this is a tautology, we can replace all predicates with Boolean variables: $$ (A \to B \land B \to C) \Rightarrow (A \to C) $$ We have obtained a problem which can be handled by a SAT solver.

In this way you can also express Boolean operations such as union, intersection and complementation.