Rigid E-unification is the problem of unifying two expressions modulo a set
of equations, with the assumption that every variable denotes
exactly one term (rigid semantics). This form of unification
was originally developed as an approach to integrate equational
reasoning in tableau-like proof procedures, and studied extensively
in the late 80s and 90s. However, the fact that simultaneous
rigid E-unification is undecidable has limited the practical relevance of
the method, and to the best of our knowledge there is no
tableau-based theorem prover that uses rigid E-unification. We recently
introduced a new decidable variant of (simultaneous) rigid E-unification, bounded
rigid E-unification (BREU), in which variables only represent terms from
finite domains, and used it to define a first-order logic
calculus. In this paper, we study the problem of computing solutions
of (individual or simultaneous) BREU problems. Two new unification
procedures for BREU are introduced, and compared theoretically and
experimentally.