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.

Thanks for your help!
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.

Consequently, solving your problem by bit-blasting to SAT is a reasonable way to solve your problem.  I don't think you should expect a much better algorithm.

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