Skolemdepth对合金检查公式的影响

Question

有人能解释合金中skolemdepth选项的影响吗？

Answer 1

这会影响您的问题如何编码为SAT实例。

作为一个例子：

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

将得到翻译成

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

（其中，P [A/B]是指B获得与取代的（发出实例的SAT解算器之前）在P）随深度1（即，仅y被skolemized），以及

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

随深度2.

从official documentation：

斯科伦深度：此控制交替 普遍-VS-存在量词时 产生斯科伦功能，我们将允许的最大深度。如果一个公式超过这个深度，我们将 不生成一个skolem函数。