Is unification over regular expression equations doable? By way of example, suppose I know that $X + a = b + Y$ where $X$ and $Y$ are variables standing for regular expressions, then $(X, Y) = (b, a)$ is a solution to this set of equations.

Generalizing over all such equations, is there a computable (decidable) procedure for calculating the regular expressions which the variables must stand for in order for the equation to be solvable? Is there some kind of uniqueness, e.g. of minimal solutions?

In case the alphabet size matters: you can represent $\{1, \ldots, n\}$ in unary using just two symbols, so I assume the answer for $k$- and $m$-symbol alphabets are the same when $k \geq 2 \land m \geq 2$, in which case I care primarily for alphabets of size $\geq 2$—the reason I stress the word "assume" is that I know some properties of regular languages don't hold for regular expression equations (when suitably translated).

The application I have in mind is miniKanren-style logic programming.

Since families of sets closed under union form a semilattice, and the family of regular languages is one such closed family, programming with regular languages seems straightforward. For example, let each logic variable $V$ represent some indeterminate language $L$. For each $V$ store a pair of bounds $(sub, disj)$ expressing the knowledge $sub \subseteq L \land (L \cap disj) = \emptyset$, i.e. store two sets of strings for which the membership-ness is known. Grow them in the variable unification part and fail when $sub \cap disj \not= \emptyset$.

It would be nice to add logic over regular expressions and not just regular languages.  No obvious approach occurs to me, and I suspect it's a whole other ballgame.
I'm fairly sure this is possible. This seems to me as a special case of set constraints over tree languages: we can view regular expressions as a restriction of regular tree languages where each node has 0 or 1 children. These can handle union, concatenation, and recursion (star), and you can solve for variables like you describe.

They're decidable, even when we allow negation. You can see a great survey here:  https://theory.stanford.edu/~aiken/publications/papers/ppcp94.pdf In general, Alexander Aiken has a lot of great papers on set constraints.

You might find more of what you're looking for with "word constraints" or "set constraints over words". The complexity situation isn't great for trees, but it might be better for words.