Solving systems of set constraints with negated subset relationships

We present a decision procedure, based on tree automata techniques, for satisfiability of systems of set constraints including negated subset relationships. This result extends all previous works on set constraints solving and solves a problem which was left open by L. Bachmair et al. (1993). We prove in a constructive way that a non empty set of solutions always contains a regular solution, that is a tuple of regular tree languages. Moreover, we think that the new class of tree automata described here could be interesting in its own