読者です 読者をやめる 読者になる 読者になる

SAT solverでパズルを解いた話

programming パズル

SAT solverで「数独」「美術館」「ひとりにしてくれ」を解きました。

Githubにあげました。

めっちゃ楽しかったので準急に多謝だー。(JOI春合宿で講義をしてくれた)

準備

SAT solverをインストールしましょう。

僕はminisatにしました。(なんか入れるのに苦労したけど)

SATを知らない人は適当に調べましょう。

流れとしては、

  • パズルを連言標準形(CNF)の論理式にして
  • SAT solverに投げて
  • ビジュアライズする

って感じです。

数独

多分一番簡単です。

「x1,x2,...,x9 のうち、ちょうど1つだけがtrue」

という式が書ければ勝ちです。これは、

  • x1 or x2 or ... or x9 (1つ以上であるという制約)
  • 全てのi,jのペアについて、!xi or !xj (2つ以上ないという制約)

で実現できます。

あとは、X_i,j,k(i行目j列目がkであるならtrue)という変数を使って

  • 行にちょうど1つだけkがある
  • 列にちょうど1つだけkがある
  • 3x3のグループにちょうど1つだけkがある
  • 各マスにはちょうど1つだけ数が割り当てられている

という条件を書いてやればいいです。

美術館

これも基本的

変数は、X_i,j = i行目j列目に明かりを置くならtrue です。

  • 照らしあってはいけない
  • 照らされていないマスがあってはいけない
  • 黒マスに明かりがあってはいけない
  • 周りに 0 個ある
  • 周りに 1 個ある
  • 周りに 3 個ある
  • 周りに 4 個ある

は簡単(実際にプログラムとして書くのはちょっと面倒だけど)で、問題は

  • 周りに 2 個ある

です。これは、

  • どの3個を取り出してorを取ってもtrue
  • どの3個を取り出して否定のorを取ってもtrue

の2つの条件にすると楽に書けます。

ちなみに、フィールドの周囲に番兵を置くとかなり実装が楽になります。

ひとりにしてくれ

  • 各列に同じ数が2つ以上残ってはならない
  • 黒マスが隣り合ってはならない

は簡単。

  • 白マスは連結でなければならない

ひぇーっ!?こんなのできるんでしょうか?

かなりのパズルが連結性判定を必要とするので、これができないとなかなか厳しいです。

連結性判定は、いろいろな方法がありそうですが、僕が今回採用したのはBFSっぽい方法です。

イメージとしては、

  • 適当に根を決めてBFSをするときの、各ステップでのvisitedの配列を変数にする。

という感じ。式を書く方針はこんな感じ。

  • Y_i,j : i行目、j列目を黒く塗るならtrue
  • X_i,j,k : i行目、j列目、BFSのkステップ目
  • X_i,j,0 たちのうち、1つだけがtrue
  • BFSの総ステップ数を T とすると、白マスの X_i,j,T は全部true
  • 黒マスの X_i,j,k は全部false
  • X_i,j,k+1 がtrueなら、X_ai,aj,kのうちいずれかはtrue((ai,aj)は(i,j)に隣接するマス)

※「A ならば B」は 「!A or B」と変換できます

変数も節もO(マスの個数^2)個でいい感じです。

ちなみに、17x17のを1つやらせてみたら20秒で答えが出ました。感動!