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函數。