ヒビルテ(2009-08-08)

2009-08-08 [長年日記]

λ. “New Techniques that Improve MACE-style Finite Model Finding” by Koen Claessen and Niklas Sörensson

以前に、一階述語論理のモデル発見器であるParadoxを使って、数独を解いてみたりしたが、Paradoxの実装に使われている性能を改善するためのテクニックを説明した論文。 Paradoxの使っているテクニックだけでなく、その前提となる一階述語論理の有限モデルをSATソルバーを使って解くための基本的な手法についても分かりやすく書かれている。

splitting

splittingというのは、例えば { P(x, y), Q(x, z) } という節を、新しい述語 S を導入して、

{ P(x, y), S(x) }
{ ￢S(x), Q(x, z) }

という節集合に分割することを指す。

splitting をすることによって、個々の節に含まれる変数を減らすことが出来る。節のインスタンス化(= 基礎化(grounding)?)の際に、節の数が変数の数の指数オーダーで膨れ上がるので、節に含まれる変数の数を減らすのは非常に重要。

splittingのためのヒューリスティックは色々あるが、これまでのはあまり良くなかった。そこで、Paradoxで採用しているのは「述語をノード、述語のリテラルが変数を共有するという関係をエッジとするようなグラフを考え、その最小の連結成分をsplittingによって分離する、ということを繰り返す」というもの。

term definition

ひとつの目の新しいテクニックは、節に含まれる変数を減らすための term definition 。

例えば、{ P(f(a, b), f(b, a)) } を普通にフラット化すると、4つの変数を含む節 {a ≠ x, b ≠ y, f(x, y) ≠ z, f(y, x) ≠ w, P(z,w)} になってしまうけど、新しい定数記号t1,t2を導入して

{ t1 = f(a, b) }
{ t2 = f(b, a) }
{ P(t1, t2) }

という節集合に変換しておくと、フラット化したときに、

{ a ≠ x, b ≠ y, f(x, y) ≠ z, t1 = z }
{ a ≠ x, b ≠ y, f(y, x) ≠ z, t2 = z }
{ t1 ≠ x, t2 ≠ y, P(x, y) }

という、各々の節が3変数しか含んでいないような節集合に出来る。

increamental SAT

二つ目の新しいテクニックは、SATソルバーのインクリメンタルな機能の活用。 MACEスタイルの方法では、モデルのサイズnを増やしながら、サイズnのモデルの探索をSAT問題に落として、SAT solver に解かせる。これまではこれを毎回一からSATソルバーにかけていたが、SATソルバーのインクリメンタルな機能を使うことで、サイズnでの探索で得られた情報(特に conflict learning の結果)をSATソルバーがその後の探索で利用でき、探索を効率化出来る。

これをするにはSATへのエンコーディングを少し工夫する必要がある。

static symmetry reduction

三つ目の新しいテクニックは、同型なモデルを排除するような制約を制的に導入すること。 SEMのように自分で探索をする場合には探索を進めながらゴニョゴニョできるけど、SATソルバーを使うので探索を始める前に制約を静的に与えておかなくてはいけないのが難しい。

定数記号 {a_i}_i について考えると、I(a_i)≦i すなわち

{ a₁ = 1 }
{ a₂ = 1, a₂ = 2 }
{ a₃ = 1, a₃ = 2, a₃ = 3 }
…

という節集合によって値域を制限し、さらに 1 < i ∈ D と 1 < d ≦ i について、

{ a_i≠d, a₁ = d-1, a₂ = d-1, …, a_i-1 = d-1 }

という節を導入することで、a_iの値をa₁,…,a_i-1で使われている値か、もしくはa₁,…,a_i-1で使われていない値のうちの最小のものに限定する。

関数記号がある場合についても同様だが、この場合には同型なモデルを完全に排除することは出来ない。

sort inference

四つ目の新しいテクニックはソート(型)の推論。ソートの推論をすることで、ソート単位で symmetry reduction が出来るようになり、より細かい symmetry reduction が出来るようになる。具体的な型推論は、関数(の引数と返り値)と述語(の引数)がすべて異なるソートを持つと仮定して、それから同じ変数が使われているところのソートを同じにしていくという、普通の方法でやっている。