# Algebra for min/max bounds

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!

• There's no need for SMT, since your constraints are Boolean. Think of each set $A$ as a unary predicate $A(x)$. If you consider any element $x$, then you can just substitute the truth value of $A(x)$ to get a Boolean variant $A$. – Yuval Filmus May 7 '20 at 14:45
• @YuvalFilmus I'm not entirely sure how that helps me, since I don't have elements to work with. – Felipe May 7 '20 at 15:17
• Will leave this open for a bit since I find the max/min algebra idea intriguing – Felipe May 7 '20 at 15:28
• You don't need elements. – Yuval Filmus May 7 '20 at 15:45

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).
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.