skolemdepth 对检查公式的影响 Alloy
Influence of skolemdepth on checking formulas in Alloy
有人可以解释 Alloy 中 skolemdepth 选项的影响吗？
这会影响您的问题如何编码为 SAT 实例。
举个例子：
∀x.∃y.∀z.∃w. P
将被转换为（在将实例发布到 SAT 求解器之前）
∀x.∀z.∃w. P[f(x)/y]
（其中 P[a/b] 表示 b 被 P 中的 a 替换）深度为 1（即只有 y 被 skolemized），并且 to
∀x.∀z. P[f(x)/y, g(x,z)/w]
深度为 2。
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.
有人可以解释 Alloy 中 skolemdepth 选项的影响吗？
这会影响您的问题如何编码为 SAT 实例。
举个例子：
∀x.∃y.∀z.∃w. P
将被转换为（在将实例发布到 SAT 求解器之前）
∀x.∀z.∃w. P[f(x)/y]
（其中 P[a/b] 表示 b 被 P 中的 a 替换）深度为 1（即只有 y 被 skolemized），并且 to
∀x.∀z. P[f(x)/y, g(x,z)/w]
深度为 2。
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.