Influence of skolemdepth on checking formulas in Alloy

Question

Could someone explain the influence of skolemdepth option in Alloy?

Answer 1

This affects how is your problem encoded as a SAT instance.

As an example:

∀x.∃y.∀z.∃w. P

would get translated to (before issuing the instance to the SAT solver)

∀x.∀z.∃w. P[f(x)/y]

(where P[a/b] means b gets substituted with a in P) with depth 1 (i.e. only y is skolemized), and to

∀x.∀z. P[f(x)/y, g(x,z)/w]

with depth 2.

From official documentation:

Skolem Depth: This controls the maximum depth of alternating universal-vs-existential quantifier that we will permit when generating a skolem function. If a formula exceeds this depth, we will not generate a skolem function for it.