2009-04-21 [長年日記]
λ. ASPで数独を解く
こないだはIDPで数独を解くというのを書いたが、今度は解集合プログラミング(Answer Set Programming, ASP)のソルバに解かせてみることにした。
ASPとは
ASPソルバは、これまでに使ってきたParadox等と同様のモデル探索器(model finder)なんだけど、Paradox等が普通の一階述語論理に基づいていたのに対して、ASPは論理プログラミングの考え方に基づいている点が少し異なる。
論理プログラミングの考え方に基づいているので、モデルとして考えているのは最小エルブランモデルや安定モデル(stable model)の一般化である解集合に限られているし、また否定に関しても古典論理の否定(classical negation, strong negation)とは別に「デフォルトの否定(default negation)」(= 「失敗による否定(negation as failure)」)を持っている。
そのため、到達可能性などを記述できたり、知識表現を行いやすかったりするのではないかと思う。 Prolog等で論理プログラミングに親しんでいる人にとっては、一階述語論理に基づいたモデル探査機よりASPのソルバの方が、親しみやすいだろう。
今回使ったソルバ
今回はPotasscoで配布されているものを使ってみた。
Potassco, the Potsdam Answer Set Solving Collection, bundles tools for Answer Set Programming developed at the University of Potsdam, among them, the answer set solver clasp, the grounder Gringo, and their combinations Clingo and iClingo.
こないだのIDPもそうだったけど、Potasscoでもグラウンダとソルバは別々になってるのね。
問題の記述
人工知能学会誌 Vol. 23 No. 5 (2008年9月) の「論理コンピューティング」(佐藤健, Marina De Vos)にちょうど数独の例が載っていて、それをほぼそのまま用いることが出来た。
sudoku-clingo.lp:
% 位置は1から9まで
position(1..9).
% 値も1から9まで
value(1..9).
% 各X,Yについて、state(X,Y,N)を満たすNがただひとつ存在
1 {state(X,Y,N) : value(N)} 1 :- position(X), position(Y).
% ある行の中の異なる場所に同じ数字があったら矛盾
:- state(XA,Y,N), state(XB,Y,N),
position(XA), position(XB), position(Y), value(N),
XA!=XB.
% ある列の中の異なる場所に同じ数字があったら矛盾
:- state(X,YA,N), state(X,YB,N),
position(X), position(YA), position(YB), value(N),
YA!=YB.
% 範囲の定義
subRange(X,1) :- position(X), 1<=X, X<=3.
subRange(X,2) :- position(X), 4<=X, X<=6.
subRange(X,3) :- position(X), 7<=X, X<=9.
% (XA,YA)と(XB,YB)が同じボックスの中にある
sameSubSquare(XA,YA,XB,YB) :-
subRange(XA,XR), subRange(XB,XR),
subRange(YA,YR), subRange(YB,YR).
% 同じボックスの中の異なる場所に同じ数字があったら矛盾
:- state(XA,YA,N), state(XB,YB,N),
sameSubSquare(XA,YA,XB,YB), value(N), XA!=XB, YA!=YB.
% 数字の既知の配置
state(1,1,1). state(1,4,2). state(1,7,3).
state(2,2,2). state(2,5,3). state(2,8,4).
state(3,3,3). state(3,6,4). state(3,0,5).
state(4,1,6). state(4,4,4). state(4,7,5).
state(5,2,7). state(5,5,5). state(5,8,6).
state(6,3,8). state(6,6,6). state(6,0,7).
state(7,1,8). state(7,4,0). state(7,7,7).
state(8,2,0). state(8,5,1). state(8,8,8).
state(0,3,1). state(0,6,2). state(0,0,4).
ちなみに、この数字の既知の配置は以下のようなものになっている。
1 |6 |8 2 | 7 | 9 3| 8| 1 ---+---+--- 2 |4 |9 3 | 5 | 1 4| 6| 2 ---+---+--- 3 |5 |7 4 | 6 | 8 5| 7| 4
実行結果
clingo sudoku-clingo.lp として実行したら、sudoku-clingo.txtのような出力が出てきた。これを見ると「Answer: 1」に続くアトムの列が解になっており、その中に「state(1,1,1) state(1,4,2) state(1,7,3), …」の部分が、実際の割り当てを現しているようだ。
それを表の形にすると以下のようになる。
179|632|845 428|175|693 563|948|271 ---+---+--- 257|413|968 836|259|417 914|786|352 ---+---+--- 381|594|726 742|361|589 695|827|134
