Fine-grained control over Skolemization

Forking off discussion about Skolemization from this thread about using disjoint “some” quantification:

There’s a separate issue here that’s caused by our inability to control Skolemization at a fine grain. Suppose you have two predicates, maybe something like:

sig Node {edges: set Node}

pred containsK3 {
some disj x1, x2, x3: Node |
x1->x2 + x1->x3 + x2->x1 + x2->x3 +
x3->x2 + x3->x1 in edges

pred someSeparatedNodes {
some disj x1, x2: Node |
x1 not in x2.^edges and
x2 not in x1.^edges

run {containsK3 and someSeparatedNodes}
for exactly 5 Node

Now the variables in both predicates get Skolemized.

This is great for debugging – I can see where a complete subgraph is and find two nodes that are mutually unreachable. But the more of these predicates I have, the more the Skolem variables start to overwhelm the instance content and the more I rely on symmetry-breaking.

So I went in search for a way to control what gets Skolemized in Alloy, beyond the Skolem depth setting (which is global and doesn’t allow a setting of -1 to disable Skolemization entirely). Amusingly, I can manually control Skolemization by careful use of superfluous disjunction. This prevents all Skolemization:

run {(containsK3 and someSeparatedNodes) or Node != Node}
for exactly 5 Node

and this prevents Skolemization of the 2 variables in someSeparatedNodes:

run {(containsK3 and (someSeparatedNodes or Node != Node))}
for exactly 5 Node

So, that’s a useful trick, although it feels a little clumsy.

1 Like

I’d personally strongly appreciate an essay on what Skolemization is and why it matters. I know it’s talked about a bit in Software Abstractions but that didn’t leave me feeling prepared for understanding this issue.


Strongly agree with @hwayne . Is there a recommended introductory text somewhere?