ACM Transactions on Programming Languages and Systems, Volume 20, No. 2, March 1998, pp. 302-343.
Download the PostScript.
A new method for finding relational models is presented. It exploits the permutation invariance of models-if two interpretations are isomorphic, then neither is a model or both are-by partitioning the space into equivalence classes of symmetrical interpretations. Representatives of these classes are constructed incrementally by using the symmetry of the partial interpretation to limit the enumeration of new relation values. The notion of symmetry depends on the type structure of the formula; by picking the weakest typing, larger equivalence classes (and thus fewer representatives) are obtained. A more refined notion of symmetry that exploits the meaning of the relational operators is also described. The method typically leads to exponential reductions, often of 6 orders of magnitude, making the automatic analysis of relational specifications possible for the first time.