## Paper: A decision procedure for a class of set constraints (at LICS 1990)

**Nevin Heintze Joxan Jaffar**

### Abstract

A set constraint is of the form exp_{1}⊇exp_{2 } where exp_{1} and exp_{2} 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_{1}=exp_{1}, . . ., 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

### BibTeX

@InProceedings{HeintzeJaffar-Adecisionproceduref, author = {Nevin Heintze and Joxan Jaffar}, title = {A decision procedure for a class of set constraints}, booktitle = {Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science (LICS 1990)}, year = {1990}, month = {June}, pages = {42--51}, location = {Philadelphia, PA, USA}, publisher = {IEEE Computer Society Press} }