Let $S_1,\dots,S_n$ be variables representing unknown sets. A set expression has the form $S_i$, $\overline{E}$ (the complement of $E$), or $E \cap E'$, where $E,E'$ are set expressions. A constraint has the form $E = \emptyset$ or $E \ne \emptyset$, where $E$ is a set expression. Given a conjunction of constraints, the problem is to determine whether they are satisfiable, i.e., whether there is an assignment from variables to sets that makes all of the constraints hold.

Conjecture: if there exists a satisfying assignment, then there is a satisfying assignment where all sets are subsets of a universe $U$ with $k$ elements, where $k$ is the number of constraints of the form $E \ne \emptyset$.

Is this conjecture true?

I suspect it is, but I can't seems to prove it. I can prove it if there is no complement operator, but my proof strategy seems to go awry if there are complements. (Proof strategy: suppose the constraints are $E_1 \ne \emptyset$, .., $E_k \ne \emptyset$, and suppose we have any satisfying assignment. Let $x$ be the smallest element of $E_1 \cup \dots \cup E_k$, where $x_i$ is an element of $E_i$; then add $x$ to $U$, discard $E_i$, and repeat. Once this is finished, replacing each set $S_i$ with $S_i \cap U$ still leaves all constraints satisfied.) If this conjecture is true, it is a sort of "small-world theorem", which says that a not-too-large universe suffices for checking satisfiability. These kinds of theorems are helpful for improving the performance of constraint-solving algorithms.