スリザーリンクをSATソルバーで解く

#puzzle

おととい、昨日に引き続き、今度はスリザーリンクのソルバーを作ってみた。

スリザーリンクもまたニコリの定番ペンシルパズルで、格子状の盤面に線を引いて１つのループを作るというルール。数字（０〜３）のあるマスは、接する線４本のうちの何本に線が引かれるかを示している。

ナンバーリンクソルバーと同様に、格子を結ぶ線を引くか引かないかの真偽値を変数にする。

そして線は途切れないので、それぞれの頂点につながる線の４本中２本に線が引かれる、または１本も引かれない、という条件になる。

全体でループがひとつながりになっているかどうかの判定は、SATソルバー内で判定する方法が思いつかなかった。なので solve で得られた解を判定して、２つ以上だったらその解は無効にして再度調べることにした。

solve で得られた解の getFormulaメソッドを forbidすることでその解を無効にすることもできるが、それだと全体がその状態となるのを除外するだけなのであまり絞り込まれず試行回数が増えてしまう。

そうではなく複数できたループごとに forbid してやると、現実的な時間で解を求めることができる。

メジャーなペンシルパズルのソルバーが作れたので、他のパズルもSATソルバーで解けるかどうか考えてみた。

解けそうなもの：

解けなそうなもの：

マスごとや行・列・指定の領域ごとなどといった決まった範囲で判定すればよいルールは解きやすそうに思うが、ぬりかべやフィルオミノなどのマスのつながりを調べる必要があるパズルはどうやってSATのルールに起こしたらいいのか、ちょっと見当がつかない。