Why does the name of a signature impact the number of variables?

Questions
1

I was looking at StackOverflow for unanswered Alloy questions, and stumbled on this one, from 7 years ago.

They give this example:

sig E {}
sig G {}
sig D extends G {
  x: E
}
sig F1 extends G {
  x: G
}
sig F2 extends G {
  x: G
}
sig F3 extends G {
  x: G
}
sig F4 extends G {
  x: G
}
run {} for 3

And note that if D is simply renamed H, Alloy produces a different number of variables.

I tested the example with Analyzer 6.1.0 and it is still the case: for “D” it produces 571 vars, 911 clauses; for “H” we get 579 vars, 925 clauses.

Any ideas why?

2

From the question:

I’m convinced this has to do with the alphabetical order of the names of the signatures. If you choose any name lower than E , you get 486 variables, and with any name higher than H you get 494 variables.

I have tried these on Alloy Analyzer 6.2.0 20241017 SNAPSHOT, with some CJK symbols too:

A: 571
D: 571
H: 579
I: 579
Z: 579
AZ: 571
ZA: 579
火: 579
金: 579
A金: 571
あ: 579
3

Hi! Interesting question. The only thing I could think of that could be affected by relation names was the symmetry breaking predicate (SBP) that is generated by Kodkod to discard identical instances from being generated. I did some digging around, and that is exactly the case, although the explanation gets a bit intricate.

TLDR: The SBP orders relations by name and there’s a limit on its size.

Details: For each pair of permutable atoms, the SBP creates a lexicographic order over all relevant tuples of a model, roughly stating which symmetries are “broken first”. Kodkod gives priority to lower arity relations, but then has no other criteria to distinguish relations, and just uses their names. So, when breaking the symmetry between atoms G$0 and G$1, your first model uses order D E F1 .. F4 G D.x F1.x .. F4.x, while the second uses E F1 .. F4 G H F1.x .. F4.x H.x. In principle, this would result in similar SBPs and number of clauses/variables, except that Kodkod imposes a limit on the size of the SBP (20 tuples by default). This is why only complex models exhibit the strange behaviour: the last relation of that order cannot fit in the SBP, so either F4.x or H.x are ignored. And since F4.x contains more tuples with G$0/G$1 than H.x, the first SBP has fewer clauses.

3 Likes