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

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

スリザーリンクとは?

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

スリザーリンクソルバー

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

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

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

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

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

他のパズルは?

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

解けそうなもの:

  • ひとりにしてくれ
  • へやわけ
  • ましゅ

解けなそうなもの:

  • ぬりかべ
  • フィルオミノ

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

ソース

参考