2009-02-22 竹島の日 [長年日記]
λ. Paradoxで数独を解く
ふと、一階述語論理のモデル発見器であるParadoxを使って、数独を解いてみた。
Paradox
Paradoxは等号付き一階述語論理の有限モデルを探してくれるツールで、一階述語論理の問題を一連のSAT問題に変換して、SATソルバを使うことでモデルを探してくれている。実装にはHaskellが使われていて、SATソルバにはMiniSatが使われている。
入力ファイル sudoku.tptp
% 数の定義 (Paradoxは数をサポートしていないので、単に項として扱う) fof( dom1, axiom, ![X] : (X=1 | X=2 | X=3 | X=4 | X=5 | X=6 | X=7 | X=8 | X=9) ). fof( dom2, axiom, 1!=2 & 1!=3 & 1!=4 & 1!=5 & 1!=6 & 1!=7 & 1!=8 & 1!=9 & 2!=3 & 2!=4 & 2!=5 & 2!=6 & 2!=7 & 2!=8 & 2!=9 & 3!=4 & 3!=5 & 3!=6 & 3!=7 & 3!=8 & 3!=9 & 4!=5 & 4!=6 & 4!=7 & 4!=8 & 4!=9 & 5!=6 & 5!=7 & 5!=8 & 5!=9 & 6!=7 & 6!=8 & 6!=9 & 7!=8 & 7!=9 & 8!=9 ). % 範囲の定義 fof( r1, axiom, ![X] : (r1(X) <=> (X=1 | X=2 | X=3))). fof( r2, axiom, ![X] : (r2(X) <=> (X=4 | X=5 | X=6))). fof( r3, axiom, ![X] : (r3(X) <=> (X=7 | X=8 | X=9))). % 全ての数が全ての行および列に存在する fof( rule1, axiom, ![N,X] : ?[Y] : N=a(X,Y) ). fof( rule2, axiom, ![N,Y] : ?[X] : N=a(X,Y) ). % 全ての数が任意のブロックに存在する fof( rule3, axiom, ![N] : ( (?[X,Y] : (r1(X) & r1(Y) & N=a(X,Y))) & (?[X,Y] : (r1(X) & r2(Y) & N=a(X,Y))) & (?[X,Y] : (r1(X) & r3(Y) & N=a(X,Y))) & (?[X,Y] : (r2(X) & r1(Y) & N=a(X,Y))) & (?[X,Y] : (r2(X) & r2(Y) & N=a(X,Y))) & (?[X,Y] : (r2(X) & r3(Y) & N=a(X,Y))) & (?[X,Y] : (r3(X) & r1(Y) & N=a(X,Y))) & (?[X,Y] : (r3(X) & r2(Y) & N=a(X,Y))) & (?[X,Y] : (r3(X) & r3(Y) & N=a(X,Y))) )). % 既知のマスの定義 fof( given, axiom, a(1,1)=1 & a(1,4)=2 & a(1,7)=3 & a(2,2)=2 & a(2,5)=3 & a(2,8)=4 & a(3,3)=3 & a(3,6)=4 & a(3,9)=5 & a(4,1)=6 & a(4,4)=4 & a(4,7)=5 & a(5,2)=7 & a(5,5)=5 & a(5,8)=6 & a(6,3)=8 & a(6,6)=6 & a(6,9)=7 & a(7,1)=8 & a(7,4)=9 & a(7,7)=7 & a(8,2)=9 & a(8,5)=1 & a(8,8)=8 & a(9,3)=1 & a(9,6)=2 & a(9,9)=4 ).
fofは一階の論理式(first order formula)を追加するためのキーワードで、引数は「名前」「種類」「論理式」という順番になっている。ここでは「種類」としてはaxiomしか用いていないけど、他にもconjectureとかがある。 論理式については、感嘆符(!)が全称量化を表し、疑問符(?)は存在量化を表していることを除けば、普通に読めるのではないかと思う。
実行例
このsudoku.tptpをparadoxに喰わせると、小さなモデルから順に探査していき、領域のサイズが9になったところでモデルが発見される。
% time paradox3 --model sudoku.tptp Paradox, version 3.0, 2008-07-29. +++ PROBLEM: sudoku.tptp Reading 'sudoku.tptp' ... OK +++ SOLVING: sudoku.tptp domain size 1 domain size 2 domain size 3 domain size 4 domain size 5 domain size 6 domain size 7 domain size 8 domain size 9 +++ BEGIN MODEL % domain size is 9 〜中略〜 a(!1,!1) = !1 a(!1,!2) = !4 a(!1,!3) = !5 a(!1,!4) = !2 a(!1,!5) = !8 a(!1,!6) = !9 a(!1,!7) = !3 a(!1,!8) = !7 a(!1,!9) = !6 a(!2,!1) = !7 a(!2,!2) = !2 〜中略〜 +++ END MODEL +++ RESULT: Satisfiable paradox3 --model sudoku.tptp 0.01s user 0.00s system 0% cpu 3.583 total %
これを表の形にすると以下のようになる。とりあえずあってるかな。
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
最適化
論理的には上に書いた制約で十分だけど、このままだと既知のマスが少ないときに解を発見するのに時間がかかってしまう。 これは多分、上の規則だけだと一つの行か列かブロックのマスを全部埋めてからでないと矛盾を発見できず、早い段階で枝刈りを行えていないため。 そこで、各行、各列、各ブロックの中に数字が重複して現れないことを表す公理を追加したら、既知のマスが少ない場合でもあまり時間がかからないようになった。
% 各行、各列、各ブロックの中に数字が重複して現れない fof( rule1b, axiom, ![X,Y,Z] : (a(X,Y)=a(X,Z) => Y=Z) ). fof( rule2b, axiom, ![X,Y,Z] : (a(X,Y)=a(Z,Y) => X=Z) ). fof( rule3b, axiom, ![X,Y,Z,W] : ( ((r1(X) & r1(Y) & r1(Z) & r1(W) & a(X,Y)=a(Z,W)) => (X=Z & Y=W)) & ((r1(X) & r2(Y) & r1(Z) & r2(W) & a(X,Y)=a(Z,W)) => (X=Z & Y=W)) & ((r1(X) & r3(Y) & r1(Z) & r3(W) & a(X,Y)=a(Z,W)) => (X=Z & Y=W)) & ((r2(X) & r1(Y) & r2(Z) & r1(W) & a(X,Y)=a(Z,W)) => (X=Z & Y=W)) & ((r2(X) & r2(Y) & r2(Z) & r2(W) & a(X,Y)=a(Z,W)) => (X=Z & Y=W)) & ((r2(X) & r3(Y) & r2(Z) & r3(W) & a(X,Y)=a(Z,W)) => (X=Z & Y=W)) & ((r3(X) & r1(Y) & r3(Z) & r1(W) & a(X,Y)=a(Z,W)) => (X=Z & Y=W)) & ((r3(X) & r2(Y) & r3(Z) & r2(W) & a(X,Y)=a(Z,W)) => (X=Z & Y=W)) & ((r3(X) & r3(Y) & r3(Z) & r3(W) & a(X,Y)=a(Z,W)) => (X=Z & Y=W)) )).
まとめ
Paradoxには、Alloyのような便利な集合・関係演算や、SMTのような便利なセオリーは無いけれど、こういった組み合わせ的な問題なら特に問題は無いな。速度的にも、直接SATを使うのに比べたら劣るとは思うが、最適化を入れた後は悪くない速度で動いていると思う。 Alloyと比べると、変なクセのない標準的な一階述語論理で書けるのは一応メリットかも。
- 入力ファイル sudoku-paradox.tptp
- ログ sudoku-paradox.txt
