いろんな方法で数独解いてみる(ASP, Prolog編)

前回の続きです。ルールの定義とかはここにあります。

ここからは、表現力の高い言語を扱うので、pythonに頼らないようにします。

ASP

ASP(解集合プログラミング)は一階述語論理を解くプログラムです。ただし、一階述語論理はホーン節で表される必要があります。

A \leftarrow A_1\wedge A_2\wedge \dots\wedge A_n

実際は、プログラムがしやすいように、述語だけではなく、四則演算や比較演算子、range関数(のようなもの)などが使えます。
ここではclingoというASPソルバーを利用します。

前提

assignという述語は「行x列yのセルの値がn」の時にassign(x,y,n)が真になるような述語です。

{assign(X, Y, N) : N=1..9} = 1 :- X=0..8, Y=0..8.

数学的に書き換えるとこんな感じです

|\{\text{assign}(X, Y, N)\mid N\in\{1,\dots,9\}\}| = 1\leftarrow X\in\{0,\dots,8\}, Y\in\{0,\dots,8\}.

日本語にすれば、「X, Yが0から8の整数であるとき、assign(X, Y, N)を満たす1から9の整数Nはただ一つある」ということですね。
つまりこの定義は、ルール１を満たします。

(じゃあ、XやYが範囲外であったら$\{\text{assign}(X, Y, N)\mid N\in\{1,\dots,9\}\}$はなんでもいいのか、というとそうではありません。ASPでは閉世界仮説というものがあり、これは「真であると演繹されないのであれば、偽である」という仮説のもとで解を求めるものです。ここで言えば、XやYが範囲外であれば、$\text{assign}(X, Y, N)$を演繹する論理式は存在しないので、明示しなくても偽となります。)

ルール2,3(一つの行(列)に同じ数字は一つ)

次のように表されます。

N1 != N2 :- assign(X1, Y, N1), assign(X2, Y, N2), X1 != X2.

論理式だと

N_1 \neq N_2 \leftarrow \text{assign}(X_1, Y, N_1) \wedge \text{assign}(X_2, Y, N_2)\wedge (X_1 \neq X_2).

日本語にすると、「同じ列Yで、X1とX2が異なる行であり、assign(X1, Y, N1)とassign(X2, Y, N2)が真ならば、N1とN2は異なる値である」という意味になります。

行についても同様です

N1 != N2 :- assign(X, Y1, N1), assign(X, Y2, N2), Y1 != Y2.

ルール4(一つのブロックに同じ数字は一つ)

まず、ブロックを定義します。block(X, Y, P, Q)はブロックの行P列Qに行x列yのセルが属する時真になる述語です。

block(X, Y, P, Q) :- P=0..2, Q=0..2, X=0..8, Y=0..8,
  P * 3 <= X, X < P * 3 + 3, Q * 3 <= Y, Y < Q * 3 + 3.

\begin{align}
\text{block}(X, Y, P, Q) \leftarrow &P, Q\in \{0,1,2\}\wedge X, Y \in\{0,\dots,8\}\wedge \\
& (3P \leq X < 3P + 3) \wedge (3Q \leq Y < 3Q + 3).
\end{align}

これを利用すれば、あとはルール2,3と同様です

N1 != N2 :- assign(X1, Y1, N1), assign(X2, Y2, N2), 
  block(X1, Y1, P, Q), block(X2, Y2, P, Q), X1 != X2.
N1 != N2 :- assign(X1, Y1, N1), assign(X2, Y2, N2),
  block(X1, Y1, P, Q), block(X2, Y2, P, Q), Y1 != Y2.

ルール5(入力を満たす)

これは次のように書けば良いです。

assign(0,3,4).
assign(0,5,2).
    :
    :

Prolog

ここのコピペ(若干改定）

:- use_module(library(clpfd)).
sudoku(Rows) :-
        length(Rows, 9), 
        maplist(same_length(Rows), Rows),
        append(Rows, Vs), Vs ins 1..9,
        maplist(all_distinct, Rows),
        transpose(Rows, Columns),
        maplist(all_distinct, Columns),
        Rows = [As,Bs,Cs,Ds,Es,Fs,Gs,Hs,Is],
        blocks(As, Bs, Cs),
        blocks(Ds, Es, Fs),
        blocks(Gs, Hs, Is).

blocks([], [], []).
blocks(X, Y, Z) :-
        X = [N1,N2,N3|Ns1],
        Y = [N4,N5,N6|Ns2],
        Z = [N7,N8,N9|Ns3],
        all_distinct([N1,N2,N3,N4,N5,N6,N7,N8,N9]),
        blocks(Ns1, Ns2, Ns3).

問題の入力は

problem([[_,_,_,_,_,_,_,_,_],
         [_,_,_,_,_,3,_,8,5],
         [_,_,1,_,2,_,_,_,_],
         [_,_,_,5,_,7,_,_,_],
         [_,_,4,_,_,_,1,_,_],
         [_,9,_,_,_,_,_,_,_],
         [5,_,_,_,_,_,_,7,3],
         [_,_,2,_,1,_,_,_,_],
         [_,_,_,_,4,_,_,_,9]]).

質問は

?- problem(Rows), sudoku(Rows), maplist(portray_clause, Rows).

超シンプルですね。日本語に直すとこんな感じです。

• Rowsが次を全て満たすとき、Rowsは有効な数独である
  • Rowsは長さ9のリスト(ルール1）
  • Rowsのリストの中身は全て長さ9のリスト(ルール1）
  • Rowsのリストのリストの中身は、1から9の数字(ルール1）
  • Rowsのそれぞれのリストについて、中身が全て異なる（ルール2）
  • ColumnsはRowsを転置したやつ
  • Columnsのそれぞれのリストについて、中身が全て異なる（ルール3）
  • Rowsは[As,Bs,Cs,Ds,Es,Fs,Gs,Hs,Is]と一致する
  • block(As,Bs,Cs)が真である（ルール4）
  • block(Ds,Es,Fs)が真である（ルール4）
  • block(Gs,Hs,Is)が真である（ルール4）
• blockは次のいずれかの条件を満たすとき真である
  • block([], [], [])である。
  • blocks(X, Y, Z)が次を満たす。
    • Xの最初の3つの要素をそれぞれN1, N2, N3とし、残りの要素をNs1とする。
    • Yの最初の3つの要素をそれぞれN4, N5, N6とし、残りの要素をNs2とする。
    • Zの最初の3つの要素をそれぞれN7, N8, N9とし、残りの要素をNs3とする。
    • N1 ~ N9が全て異なる
    • block(Ns1, Ns2, Ns3)を満たす。

problemにあるアンダーバーは、「何にも縛られない変数」という意味です。また、質問のportray_clauseはきれいにプリントしてくれる述語になります

自前アルゴリズム

時間ないのでやめました٩( ᐛ )و(☝︎ ՞ਊ ՞)☝︎( ͡° ͜ʖ ͡°)

比較

言語	宣言的(*1)	探索アルゴリズム(*2)	コードの読みやすさ	条件の追加のしやすさ(*3)
SAT	○	◎	x	x
CSP	○	◎	△	△
ASP	○	◎	○	◎
Prolog	○	○	○	◎
手続き型	言語による(Cならx)	自前で書けば◎	簡単な探索なら◎、効率の良い探索ならx	△

• (*1) 宣言型(Declarative)プログラミング はプログラムが満たすべき性質を宣言することで、それを満たす計算を行ってくれるプログラミングパラダイムのことです。これは、手続きを記述する命令型プログラミング(C, Pythonなど)と、関数の性質を記述する関数型プログラミング(Lisp, Haskell)とは異なるものです（Prologは比較的にマルチパラダイムに近いですが）
• (*2) 当たり前ですが、SAT、CSP、ASPはそれぞれ効率の良い探索方法が研究されており、手続き型では自前で実装しなければならない単位伝搬などのアルゴリズムを勝手に行ってくれます。Prologについてはどのような探索が行われるかよくわかりませんが、元のページ曰く探索を行わずとも（つまり単位伝搬だけで）解が求まるそうなので、効率の良いことは間違いなさそうです。
• (*3)宣言型(Declarative)プログラミングの良さの一つが、新しい条件を加えやすいということです。例えば、ASPでは、対角線上の数値も重複を許さないという条件を加えるには以下のコードを好きなところに加えれば良いんです

N1 != N2 :- assign(X1, X1, N1), assign(X2, X2, N2), X1 != X2.
N1 != N2 :- assign(X1, 9-X1, N1), assign(X2, 9-X2, N2), X1 != X2, X1 != 9-X2.

まとめ

PrologはPepperでも使われるくらいのイケイケなAIの分野です...とはなかなか言えないくらい機械学習の影に潜んでしまっていますが、使える場面があるのは確かです。フルスタックプログラマーを自称したいならここにある言語全部使えるようになっておきましょう(暴論）