ペントミノパズルをSATソルバで解く

#puzzle

以前ペントミノパズルをコンピュータで解こうとしたがSATソルバで解かせることには失敗したため、深さ優先探索とDancing Links法で解いてみた。それを再度SATソルバで試してみる。

SATソルバでの解き方

SATソルバは自分でパズルの解法を書くのではなく、論理式を組み立てるだけで解くことができるという汎用的な手法。もうちょっと詳しいことは昔の記事を読んでもらうとして、ペントミノパズルをどうやって解くか考える。

ペントミノパズルを解くために論理式の変数がなにを表すかを決める必要がある。以前と同じく「各ピースの反転・回転ごと・盤面の各位置に配置される」とする。変数は例えば6x10の盤面の場合、全部で2,056個になる（X最適化前）。

パズルは矩形の盤面に12種類のピースを詰め込む、ということなので以前考えたのと同様に、

という制約になる。ただこれだけだと以前に失敗したのと同じで現実的な時間では解けない。 SATソルバが条件を絞り込めなくて非常に時間がかかってしまう。

どうしたもんかと思ったが、

という追加の制約を加えることでだいぶ高速化できる。

ルール的にはAとBだけで成り立つと思うんだけど、「盤面がピースで埋め尽くせる」というのがSATソルバにとっては自明じゃない、ということで明示的に与える必要があるのかもしれない
逆にルールBを除外してAとCだけでも有効だけど、Bがあった上でCを「1つだけ存在」ではなく「少なくとも1つは」にする（ピース同士の交差の除外はBで行う）のが一番効果的だった
- Cのピース交差の除外では同じピース・回転反転・位置のペアでも複数回列挙されてしまうから、性能が劣化するのだと予想

SATでは論理式を乗法標準形(Conjunctive Normal Form (CNF)、orでつないだ命題を、andでつないだもの)で表すという制限があるけど、

「少なくとも１つ」At Least One(ALO)：単なるor v1 || v2 || ...
「たかだか１つ」At Most One(AMO)：否定のorのand (!v1 || !v2) && (!v1 || !v3) && (!v2 || !v3) ... どのペアも両者が成り立つことはない
「必ず１つだけ存在する」Exactly One：ALO && AMO

パズルを解くにはこの3つでなんとかなる気がしてきた。

ペントミノパズルには複数の解が存在するが、SATソルバは制約を満たす組み合わせを1つ見つけるだけなので、別の解を探すには対策が必要になる。解が見つかったら、「その解を除く」という制約、つまり「解で真となった変数のうちどれか1つは偽となる組み合わせ」という制約を追加して、再度ソルバにかける。

また盤面に対して上下または左右対称、正方形8x8の盤面の場合には回転対称の解も除外するため、それらの制約も追加する。

深さ優先探索で解いた時にも使った盤面対称解の絞り込み、Ｘピースによる解の重複排除、Xを盤面の1/4の範囲のみに制限するという手法を適用してみる。盤面が正方形の場合には「x>y」も除外することで回転対称解も絞り込める。

深さ優先探索のときのように「先に配置しておく」というようなことはできないが、それでもかなり効果がある。

これによって対称解をあらかじめ省けるが、盤面の幅や高さが奇数の場合や、正方形の場合の対角線対称の重複解が列挙されてしまうので、対称解の制約追加は残している。

盤面のサイズ6x10と8x8、ソルバをSAT・深さ優先探索(DFS)・Dancing Links(DLX)で計測（単位：ミリ秒、低い方がよい）

盤面	SAT	DFS	DLX
6x10	1,152,311.6	156.0	4,414.3
8x8	37,679.5	64.6	373.4

SAT版は20分くらいかかるという桁違いの遅さだけど、まあ汎用的なソルバで一応待てる時間で解けるようになって結果としては満足。