合金のチェック式にskolemdepthの影響

Question

誰かが合金のskolemdepthオプションの影響を説明できますか？

Answer 1

これは、問題がどのようにSATインスタンスとしてエンコードされるかに影響します。例として

：P [A/B] Bを意味するが、で置換されています

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

は（SATソルバにインスタンスを発行する前）に変換さになるだろう

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

（深さ1）P（すなわちYのみがskolemizedされる）、および深さ2

と

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

に

official documentationから：

スコーレムの深さ：これは はスコーレム関数を生成するときに我々が許可されます ユニバーサル-VS-存在記号を交互に最大の深さを制御します。数式がこの深さを超えると、 はスカラー関数を生成しません。