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!

  • $\begingroup$ 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$. $\endgroup$ Commented May 7, 2020 at 14:45
  • $\begingroup$ @YuvalFilmus I'm not entirely sure how that helps me, since I don't have elements to work with. $\endgroup$
    – Felipe
    Commented May 7, 2020 at 15:17
  • $\begingroup$ Will leave this open for a bit since I find the max/min algebra idea intriguing $\endgroup$
    – Felipe
    Commented May 7, 2020 at 15:28
  • $\begingroup$ You don't need elements. $\endgroup$ Commented May 7, 2020 at 15:45

2 Answers 2


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.

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


Your Answer

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

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