Algorithm for finding smallest set and instanciation for a given constraint system

I have a system of constraints described by a set of clauses of the form $x_1 \neq x_2 \lor \dots \lor x_{i-1} \neq x_i$, for instance:

x1 != x2
x3 != x4 or x5 != x6


and I need to find the smallest set $A$ such that $x_1, \dots x_n \in A$, and of course an instanciation of those variables.

Note that I'm not working with numbers, so I don't have any other sorts of inequalities (like $x_i \leq x_j$, etc.), only $x_i \neq x_j$.

Has this problem a name ? Is there a specific algorithm for this problem ?

I was planning to use a SMT solver for this, replacing $A$ by $\mathbb{N}$ and adding the constraint $\forall i, x_i \leq k$ while minimizing $k$. This works fine but I feel like it's a bit too much.

• Graph coloring is a special case of your problem: Every variable $x_i$ corresponds to a vertex of the graph, and an edge between two vertices means that the two variables must take different values. – Gamow May 22 '18 at 13:31
• @Gamow I thought abouth that, but how do you model $x_3 \neq x_4 \lor x_5 \neq x_6$ ? If a put an edge between $x_3,x_4$ and an other one between $x_5,x_6$, I'll have $x_3 \neq x_4 \land x_5 \neq x_6$, right? – Jingbee May 22 '18 at 13:55
Your problem is at least as hard as SAT: given a CNF formula $\varphi$ on variables $x_1,\dots,x_n$, add variables $x_{\bot},x_{\top}$ and the clause $x_{\bot} \ne x_{\top}$, and translate each occurrence of the literal $x_i$ in $\varphi$ to $x_i \ne x_\bot$ and each occurrence of the literal $\overline{x_i}$ to $x_i \ne x_\top$. In this way each clause of $\varphi$ can be translated into a constraint of your form. Then $\varphi$ is satisfiable iff the resulting set of constraints can be satisfied by a set $A$ of size 2 (i.e., $|A|=2$). Therefore, if we could solve your problem, we could solve SAT. So your problem is at least as hard as SAT.
This does leave some room for cleverness in how you encode your problem as a SAT instance. You could encode each $x_i$ either with a one-hot encoding (using $nk$ bits), or in binary (with $n\lceil \lg k \rceil$ bits), or by encoding which pairs of $x$'s are equal (with ${n \choose 2}$ bits, i.e., a boolean variable for each $i,j$ encoding whether $x_i = x_j$, with transitivity constraints enforced). Which you choose is likely to affect the running time in practice. I suggest experimenting a bit with different possible ways of encoding your problem as SAT to see what seems to work best for the types of problems you are dealing with. (I don't particularly expect a SMT solver to do any better than a SAT solver here, but you could try it.)