A decision procedure for a class of set constraints

A set constraint is of the form exp₁⊇exp₂ where exp₁ and exp₂ are set expressions constructed using variables, function symbols, projection symbols, and the set union, intersection, and complement symbols. While the satisfiability problem for such constraints is open, restricted classes have been useful in program analysis. The main result is a decision procedure for definite set constraints which are of the restricted form a⊇exp, where a contains only constants, variables, and function symbols, and exp is a positive set expression (that is, it does not contain the complement symbol). A conjunction of such constraints, whenever satisfiable, has a least model and the algorithm will output an explicit representation of this model. An additional feature of the algorithm is that it deals with another important class of set constraints. These are the solved form set constraints which have the form X₁=exp₁, . . ., X_n=exp_n, where the X_i are distinct variables and the exp_i are positive set expressions. A solved form constraint is always satisfiable and possesses a least and a greatest model. The algorithm can output explicit representations of both