Algorithm for finding smallest set and instanciation for a given constraint system
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.)