Fifth Annual IEEE Symposium on

Logic in Computer Science (LICS 1990)

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

Authors: Heintze, N. Jaffar, J.


A set constraint is of the form exp1⊇exp2 where exp1 and exp2 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 X1=exp1, . . ., Xn=expn, where the Xi are distinct variables and the expi 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


    author = 	 {Heintze, N. and Jaffar, J.},
    title = 	 {A decision procedure for a class of set constraints},
    booktitle =  {Proceedings of the Fifth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1990},
    year =	 1990,
    editor =	 {John Mitchell},
    month =	 {June}, 
    pages =      {42--51},
    location =   {Philadelphia, PA, USA}, 
    publisher =	 {IEEE Computer Society Press}