Xmas Contest 2017 I問題 SAT Puzzle 解説

問題 | 解説まとめ

まずはコードです。
このコードでやっていることを解説します。

まず、各マスには「黒」または「白」ではなく、「黒」または「(1,1)~(4,4)」を割り当てることにします。
ただし、(j,k)は「j番目の白マスグループのk番目のマス」を表すものとします。
これを実現するには、黒を割り当てることを表す x[1]~x[36] の他に、マス
i に (j,k) を割り当てることを表す変数 x'[i][j][k] を用意し、条件を節として書き連ねていきます。
書かなければいけない条件は以下の通りです。

  • 各マスは「黒」または「(1,1)~(4,4)」のいずれかちょうど1つに割り当てなければならない。
  • 「(1,1)~(4,4)」が割り当てられるマスはそれぞれちょうど1つずつでなければならない。
  • 「(j,1)~(j,4)」は連結でなければならない。
  • 「(j,k)~(j',k')」(j≠j')は隣接してはいけない。

1つ目と2つ目

1つ目の条件では、各 i について x[i] と x'[i][1~4][1~4] のうちちょうど1つが真であれば良く、
2つ目の条件では、各 j,k の組について x'[1~36][j][k] のうちちょうど1つが真であれば良いです。
いずれにおいても「いくつかの変数のうちちょうど1つが真」というのを表現できればいいです。
これは、例えば a,b,c の3つの変数のうちちょうど1つのときは、

  • (a V b V c)(少なくとも1つは真)
  • (-a V -b)^(-b V -c)^(-c V -a)(どの2つを取ってきてもどちらかは偽=多くとも真は1つ以下)

と表現できます。

3つ目

「連結」という条件をそのまま扱うのは難しいため、「うまく有向辺をはると根付き木ができる」という条件として実装します。
このとき、辺は小→大へのみ張れることとし、根は1番になるようにするとします。
つまり、k=2~4について、隣接のいずれかに1~k-1のいずれかがあれば良いことになります。
これを節で表すと、

  • (x'[i][j][k] → V(x'[i'][j][k'] | i' ∈ iの隣接, 1 ≦ k' < k))

A→Bは「AならばB」の意味で、(A,B)が(真,偽)のときのみ偽となります。
これをCNFに直すと、

  • (-x'[i][j][k] V (V(x'[i'][j][k'] | i' ∈ iの隣接, 1 ≦ k' < k)))

となります。(数式が見にくいのでソースコードも参考に・・・)

4つ目

隣接するマスが別グループであってはならないという条件。
ドモルガンでandの否定を否定のorに変換するのはSATの基本。

  • (-x'[i][j][k] V -x[i'][j'][k']) (i' ∈ iの隣接, j ≠ j')

これで満点が取れます。

パズルをSATで解く話は昔、準急がJOIの春合宿の講義でしていて、すごく面白かったので自分でも遊んでみてたりしました。(なのに準急がこれ解けなかったのは意外だった)
楽しいので、他のパズルのソルバも書いて遊んでみてください。
初心者向けなのは数独かなぁ。
僕は美術館とひとりにしてくれを昔書きました。
僕のコードはここにあります。(honeyはこの問題の元になったハニーアイランドというパズルで、これは普通に枝刈り探索のコードです)(number_linkはgraphillionで書きました)
github.com