07

04

CBMCを使って数独パズルを解く その3

2010.07.04(17:41)

数独の答えはほんとうに1つなんでしょうか? まあまともに出題されている問題であれば、出題から解いてゆけば解答は一意に決まるんでしょうね。

それを確かめるソースコードを書いてみました。



int compare(int a[9][9],int b[9][9]) {
for (int i = 0; i < 9; i++) {
for (int j = 0; j < 9; j++) {
if (a[i][j] != b[i][j]) {
return 0;
}
}
}
return 1;
}

void shutudai(int masu[9][9])
{
masu[0][2] = 2; masu[0][4] = 9; masu[0][5] = 3; masu[0][7] = 8;
masu[1][1] = 7; masu[1][2] = 4; masu[1][5] = 6;
masu[2][3] = 4; masu[2][7] = 5;
masu[3][7] = 2;
masu[4][2] = 1; masu[4][3] = 3; masu[4][5] = 8; masu[4][6] = 5;
masu[5][1] = 9;
masu[6][1] = 6; masu[6][5] = 4;
masu[7][3] = 9; masu[7][6] = 8; masu[7][7] = 7;
masu[8][1] = 5; masu[8][3] = 8; masu[8][4] = 7; masu[8][6] = 2;
}

int main(int argc, char **argv) {
int first[9][9];
int second[9][9];
int temp[9][9];

shutudai(first);
shutudai(second);
__CPROVER_assume(check(first) == 1);
//__CPROVER_assume(check(second) == 1);
temp = first;
temp = second;
assert(compare(first,second) == 0);
}



2つの結果を比較する compare()
配列に対して出題をセットする shutudai()
これらを使った main()
を用意しました。まずこのプログラムが合っていることを確認するために、
mainの一番最後に、
解が求まって かつ その解が適当に作った配列と違っている という assert
を書いて実行してみます。解は1つはあるはずです。

出題は前回のと違ってちょっと難しいのにしてみました。



State 5778 file sudoku.c line 102 function main thread 0
----------------------------------------------------
sudoku::main::1::temp={ { 5, 1, 2, 7, 9, 3, 4, 8, 6 }, { 9, 7, 4, 5, 8, 6, 1, 3, 2 }, { 3, 8, 6, 4, 1, 2, 7, 5, 9 }, { 7, 3, 5, 1, 4, 9, 6, 2, 8 }, { 6, 4, 1, 3, 2, 8, 5, 9, 7 }, { 2, 9, 8, 6, 5, 7, 3, 4, 1 }, { 8, 6, 7, 2, 3, 4, 9, 1, 5 }, { 1, 2, 3, 9, 6, 5, 8, 7, 4 }, { 4, 5, 9, 8, 7, 1, 2, 6, 3 } }

State 5779 file sudoku.c line 103 function main thread 0
----------------------------------------------------
sudoku::main::1::temp={ { 5, 1, 2, 7, 9, 3, 4, 8, 6 }, { 9, 7, 4, 5, 8, 6, 1, 3, 2 }, { 3, 8, 6, 4, 1, 2, 7, 5, 9 }, { 7, 3, 5, 1, 4, 9, 6, 2, 8 }, { 6, 4, 1, 3, 2, 8, 5, 9, 7 }, { 2, 9, 8, 6, 5, 7, 3, 4, 1 }, { 8, 6, 7, 2, 3, 4, 9, 1, 5 }, { 1, 2, 3, 9, 6, 5, 8, 7, 4 }, { 4, 5, 9, 8, 7, 1, 2, 6, 3 } }

{ 5, 1, 2, 7, 9, 3, 4, 8, 6 },
{ 9, 7, 4, 8, 5, 6, 2, 1, 3 },
{ 3, 6, 8, 4, 1, 2, 7, 5, 9 },
{ 7, 5, 3, 9, 6, 4, 8, 2, 1 },
{ 6, 4, 1, 3, 2, 8, 5, 9, 7 },
{ 2, 8, 9, 5, 7, 1, 6, 3, 4 },
{ 4, 2, 5, 1, 3, 7, 9, 6, 8 },
{ 1, 9, 7, 6, 8, 5, 3, 4, 2 },
{ 8, 3, 6, 2, 4, 9, 1, 7, 5 }



解がもとまり、適当な解もそれと同じものにすれば、反例になりました。

次に、
2つ解が求まって かつ それらが一致している という assert
を書いて実行してみます。

反例が見つかれば、解が少なくとも2つあることになります。



int main(int argc, char **argv) {
int first[9][9];
int second[9][9];
int temp[9][9];

shutudai(first);
shutudai(second);
__CPROVER_assume(check(first) == 1);
__CPROVER_assume(check(second) == 1);
temp = first;
temp = second;
assert(compare(first,second) == 1);
}



その結果は、


size of program expression: 28202 assignments
simple slicing removed 1 assignments
Generated 1 VCC(s), 1 remaining after simplification
Passing problem to propositional reduction
Running propositional reduction
Solving with MiniSAT2 without simplifier
398350 variables, 1580586 clauses
SAT checker: negated claim is UNSATISFIABLE, i.e., holds
Runtime decision procedure: 503.766s
VERIFICATION SUCCESSFUL


503秒かかって、反例が見つからないことが証明されてしました。
この問題には解は1つしかないようです。

あまり面白くないので、問題のほうを変更して、値が設定してあるマスを
半分にしてみました。条件をゆるめると可能性が増えるので計算時間はよりかかるはず。


void shutudai(int masu[9][9])
{
masu[0][2] = 2; masu[0][4] = 9; masu[0][5] = 3; masu[0][7] = 8;
masu[1][1] = 7; masu[1][2] = 4; masu[1][5] = 6;
masu[2][3] = 4; masu[2][7] = 5;
masu[3][7] = 2;
masu[4][2] = 1; masu[4][3] = 3; masu[4][5] = 8; masu[4][6] = 5;
/*
masu[5][1] = 9;
masu[6][1] = 6; masu[6][5] = 4;
masu[7][3] = 9; masu[7][6] = 8; masu[7][7] = 7;
masu[8][1] = 5; masu[8][3] = 8; masu[8][4] = 7; masu[8][6] = 2;
*/
}

size of program expression: 28182 assignments
simple slicing removed 1 assignments
Generated 1 VCC(s), 1 remaining after simplification
Passing problem to propositional reduction
Running propositional reduction
Solving with MiniSAT2 without simplifier
399890 variables, 1607071 clauses
SAT checker: negated claim is SATISFIABLE, i.e., does not hold
Runtime decision procedure: 497.547s
Building error trace

Counterexample:

State 11469 file sudoku.c line 104 function main thread 0
----------------------------------------------------
sudoku::main::1::temp={ { 6, 5, 2, 1, 9, 3, 7, 8, 4 }, { 9, 7, 4, 5, 8, 6, 1, 3, 2 }, { 8, 1, 3, 4, 7, 2, 6, 5, 9 }, { 5, 3, 8, 6, 1, 4, 9, 2, 7 }, { 7, 9, 1, 3, 2, 8, 5, 4, 6 }, { 4, 2, 6, 9, 5, 7, 8, 1, 3 }, { 3, 8, 5, 7, 4, 9, 2, 6, 1 }, { 2, 4, 7, 8, 6, 1, 3, 9, 5 }, { 1, 6, 9, 2, 3, 5, 4, 7, 8 } }

State 11470 file sudoku.c line 105 function main thread 0
----------------------------------------------------
sudoku::main::1::temp={ { 5, 1, 2, 7, 9, 3, 4, 8, 6 }, { 9, 7, 4, 8, 5, 6, 2, 1, 3 }, { 3, 6, 8, 4, 1, 2, 7, 5, 9 }, { 7, 5, 3, 9, 6, 4, 8, 2, 1 }, { 6, 4, 1, 3, 2, 8, 5, 9, 7 }, { 2, 8, 9, 5, 7, 1, 6, 3, 4 }, { 4, 2, 5, 1, 3, 7, 9, 6, 8 }, { 1, 9, 7, 6, 8, 5, 3, 4, 2 }, { 8, 3, 6, 2, 4, 9, 1, 7, 5 } }

{ 6, 5, 2, 1, 9, 3, 7, 8, 4 },
{ 9, 7, 4, 5, 8, 6, 1, 3, 2 },
{ 8, 1, 3, 4, 7, 2, 6, 5, 9 },
{ 5, 3, 8, 6, 1, 4, 9, 2, 7 },
{ 7, 9, 1, 3, 2, 8, 5, 4, 6 },
{ 4, 2, 6, 9, 5, 7, 8, 1, 3 },
{ 3, 8, 5, 7, 4, 9, 2, 6, 1 },
{ 2, 4, 7, 8, 6, 1, 3, 9, 5 },
{ 1, 6, 9, 2, 3, 5, 4, 7, 8 }

{ 5, 1, 2, 7, 9, 3, 4, 8, 6 },
{ 9, 7, 4, 8, 5, 6, 2, 1, 3 },
{ 3, 6, 8, 4, 1, 2, 7, 5, 9 },
{ 7, 5, 3, 9, 6, 4, 8, 2, 1 },
{ 6, 4, 1, 3, 2, 8, 5, 9, 7 },
{ 2, 8, 9, 5, 7, 1, 6, 3, 4 },
{ 4, 2, 5, 1, 3, 7, 9, 6, 8 },
{ 1, 9, 7, 6, 8, 5, 3, 4, 2 },
{ 8, 3, 6, 2, 4, 9, 1, 7, 5 }



497秒かかって、反例が1つ見つかりました。
最初に埋めるマスを減らせば、解が2つ見つかることがあることはわかりました。

何かあやしい問題があったら、このソースコードを使ってチェックしてみようと思います。

ソースコード
sudoku4.c

次回は、数値を求めるパズルではなくて、他の可能性をさぐってみます。

コメントの投稿

非公開コメント

プロフィール

島敏博

Shima Toshihiro 島敏博
信州アルプスハイランド在住。HaskellとElixirが好き。組み込みソフトウェアアーキテクト、C++プログラマ、山歩き、美術館巡り、和食食べ歩き、日本赤十字社救急法指導員、インデックス投資、クラシック音楽、SESSAME会員、状態マシン設計、モデル駆動開発、ソフトウェアプロダクトライン、Rubyist、実践ビジネス英語

■ ツイッター
http://twitter.com/saltheads
■ Facebook
http://www.facebook.com/saltheads
■ Qiita
http://qiita.com/saltheads

印刷する場合は、ブラウザの印刷メニューではなく、このページの上から3cmくらいの青いところにある、「印刷」を押してみてください。少しうまく印刷できます。まだ完全ではないのですが、これで勘弁してください。


カテゴリ
最新記事
月別アーカイブ
最新コメント
検索フォーム
リンク
sessame
RSSリンクの表示