Systems of set constraints with negative constraints are NEXPTIME-complete

A system of set constraints is a system of expressions E⊆F where E and F describe sets of ground terms over a ranked alphabet. Aiken et al. (1993) classified the complexity of such systems. In A. aiken et al. (1993), it was shown that if negative constraints Enot⊆F were allowed, then the problem as decidable. This was done by reduction to a Diophantine problem, the nonlinear reachability problem, which was shown to be decidable. We show that nonlinear reachability is NP-complete. By bounding the reduction of A. aiken et al. (1993), we conclude that systems of set constraints allowing negative constraints are NEXPTIME-complete