スリザーリンクをSATソルバーで解いてみた．
まずは，minisat-2.2.0を使用．以下の制約を与えた．
- 問題升の辺の数
- 各頂点につき，辺の数は0または2
- 辺にランクを与える．問題で1以上の値が与えられている升をひとつ任意に固定し，この升の周囲の辺をすべてランク0とする．他の辺は，隣接辺のどれかが自分よりもランクが低い
ランクに整数が出てくる．「2進エンコーディング」とした．つまり，各辺edgeと整数nに対し，「edgeのランクの2進表記の第n桁の値が1」という命題に変数を割り当てた．「順序エンコーディング」(rank(edge) < n という命題に変数を割り当てる) も考えたが，出てくる制約が大小比較だけなので，2進エンコーディングの方が変数の数が少ない分有利，と判断した．実験して比較すれば良いのだけれど．
動作させてみたが，結構時間がかかる．問題サイズが10×10だと1-2秒で返ってくるが，45×31だと，2分弱かかる．もちろん問題にも依存するだろうから，もっと計らなくてはいけないが．
そこで，今度は次の方針にしてみた: 制約1,2のみでSATソルバーで解かせ，出てきたものを輪に分解し，各々の輪について，そのどれかの辺はOFFでなければならない，という制約を追加して再びSATソルバーにかける．これを輪の数が1になるまで繰り返す，
この場合，(k+1)回目の制約条件はk回目のそれに対する追加なのだから，k回目の計算過程 (学習節とか) を覚えていて，k+1回目の計算で利用してほしい．でないと，毎回同じ計算を繰り返すことになって遅くなってしまう．いわゆるインクリメンタルな解法である．どうも，minisatは，インクリメンタルに行おうとすると，APIを使ったプログラムを書かなくてはならず，外側から起動するのではだめなようである．
そこで，Z3を使うことにした．Z3ならば整数の演算ができるので，辺の型はBoolのままだけれど，制約1,2の表現を「trueは1, falseは0として，和がn」として書いてみた．するとあまり速くない．上のminisat版と同じくらいかかる．制約1,2を元と同じようにBool式だけで書いてやったら，速くなった．45×31が，30秒強である．
keyword: slither link SAT solver incremental