SAT攻撃で「タルスキの高校代数問題」の最小反例モデルを解明

SATソルバーの論文は大好きだ。補助変数のテクニックはいつ見ても面白い。なぜなら、それが一箇所にまとめてリストアップされることは滅多にないからだ。例えばここでは、{f(x,y,z)==g(x,y,z)}と言う代わりに、著者らは変数グループa_w:=(f(x,y,z)=w||g(x,y,z)=w)を作り、それに「高々1個」制約を適用している。両方の関数が全体で1つの結果しか持てないなら、等しくないことはあり得ない。これは反復するためのインデックスを追加するが、f()とg()の内部サブ式を分離し、(この問題では)2つのインデックスを削除して、節のn乗全体を落とすことになる。

---

私が理解できないのは、彼らがタルスキの問題そのものを探しているのではなく、その特定の解(与えられたものから導かれない1つの恒等式)を探していることだ。私はウィルキーとは別の方法で期待を裏切る算術モデルを探すだろう。