07

04

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

2010.07.04(00:33)

今度はCBMCを使って、数独パズルの問題を解いてみます。まずソースコードです。


int find(int n,int a,int b,int c,int d,int e,int f,int g,int h,int i)
{
// aからiまでに nがあることを確認する
if ((n == a)||(n == b)||(n == c)
||(n == d)||(n == e)||(n == f)
||(n == g)||(n == h)||(n == i)) {
return 1;
}
// not found
return 0;
}

int find9(int a,int b,int c,int d,int e,int f,int g,int h,int i)
{
// aからiまでに 1から9までのすべてがあることを確認する
if ((find(1,a,b,c,d,e,f,g,h,i)==0)
||(find(2,a,b,c,d,e,f,g,h,i)==0)
||(find(3,a,b,c,d,e,f,g,h,i)==0)
||(find(4,a,b,c,d,e,f,g,h,i)==0)
||(find(5,a,b,c,d,e,f,g,h,i)==0)
||(find(6,a,b,c,d,e,f,g,h,i)==0)
||(find(7,a,b,c,d,e,f,g,h,i)==0)
||(find(8,a,b,c,d,e,f,g,h,i)==0)
||(find(9,a,b,c,d,e,f,g,h,i)==0)
||(find(1,a,b,c,d,e,f,g,h,i)==0)) {
return 0;
}
return 1;
}

int check(int a[9][9]) {
// 数独の条件を満たしていることを確認する。
if ( (find9(a[0][0],a[0][1],a[0][2],a[0][3],a[0][4],a[0][5],a[0][6],a[0][7],a[0][8])==0)
||(find9(a[1][0],a[1][1],a[1][2],a[1][3],a[1][4],a[1][5],a[1][6],a[1][7],a[1][8])==0)
||(find9(a[2][0],a[2][1],a[2][2],a[2][3],a[2][4],a[2][5],a[2][6],a[2][7],a[2][8])==0)
||(find9(a[3][0],a[3][1],a[3][2],a[3][3],a[3][4],a[3][5],a[3][6],a[3][7],a[3][8])==0)
||(find9(a[4][0],a[4][1],a[4][2],a[4][3],a[4][4],a[4][5],a[4][6],a[4][7],a[4][8])==0)
||(find9(a[5][0],a[5][1],a[5][2],a[5][3],a[5][4],a[5][5],a[5][6],a[5][7],a[5][8])==0)
||(find9(a[6][0],a[6][1],a[6][2],a[6][3],a[6][4],a[6][5],a[6][6],a[6][7],a[6][8])==0)
||(find9(a[7][0],a[7][1],a[7][2],a[7][3],a[7][4],a[7][5],a[7][6],a[7][7],a[7][8])==0)
||(find9(a[8][0],a[8][1],a[8][2],a[8][3],a[8][4],a[8][5],a[8][6],a[8][7],a[8][8])==0)
||(find9(a[9][0],a[9][1],a[9][2],a[9][3],a[9][4],a[9][5],a[9][6],a[9][7],a[9][8])==0)

||(find9(a[0][1],a[1][1],a[2][1],a[3][1],a[4][1],a[5][1],a[6][1],a[7][1],a[8][1])==0)
||(find9(a[0][2],a[1][2],a[2][2],a[3][2],a[4][2],a[5][2],a[6][2],a[7][2],a[8][2])==0)
||(find9(a[0][3],a[1][3],a[2][3],a[3][3],a[4][3],a[5][3],a[6][3],a[7][3],a[8][3])==0)
||(find9(a[0][4],a[1][4],a[2][4],a[3][4],a[4][4],a[5][4],a[6][4],a[7][4],a[8][4])==0)
||(find9(a[0][5],a[1][5],a[2][5],a[3][5],a[4][5],a[5][5],a[6][5],a[7][5],a[8][5])==0)
||(find9(a[0][6],a[1][6],a[2][6],a[3][6],a[4][6],a[5][6],a[6][6],a[7][6],a[8][6])==0)
||(find9(a[0][7],a[1][7],a[2][7],a[3][7],a[4][7],a[5][7],a[6][7],a[7][7],a[8][7])==0)
||(find9(a[0][8],a[1][8],a[2][8],a[3][8],a[4][8],a[5][8],a[6][8],a[7][8],a[8][8])==0)
||(find9(a[0][9],a[1][9],a[2][9],a[3][9],a[4][9],a[5][9],a[6][9],a[7][9],a[8][9])==0)

||(find9(a[0][0],a[0][1],a[0][2],a[1][0],a[1][1],a[1][2],a[2][0],a[2][1],a[2][2])==0)
||(find9(a[3][0],a[3][1],a[3][2],a[4][0],a[4][1],a[4][2],a[5][0],a[5][1],a[5][2])==0)
||(find9(a[6][0],a[6][1],a[6][2],a[7][0],a[7][1],a[7][2],a[8][0],a[8][1],a[8][2])==0)
||(find9(a[0][3],a[0][4],a[0][5],a[1][3],a[1][4],a[1][5],a[2][3],a[2][4],a[2][5])==0)
||(find9(a[3][3],a[3][4],a[3][5],a[4][3],a[4][4],a[4][5],a[5][3],a[5][4],a[5][5])==0)
||(find9(a[6][3],a[6][4],a[6][5],a[7][3],a[7][4],a[7][5],a[8][3],a[8][4],a[8][5])==0)
||(find9(a[0][6],a[0][7],a[0][8],a[1][6],a[1][7],a[1][8],a[2][6],a[2][7],a[2][8])==0)
||(find9(a[3][6],a[3][7],a[3][8],a[4][6],a[4][7],a[4][8],a[5][6],a[5][7],a[5][8])==0)
||(find9(a[6][6],a[6][7],a[6][8],a[7][6],a[7][7],a[7][8],a[8][6],a[8][7],a[8][8])==0)) {
return 0;
}
return 1;
}

int main(int argc, char **argv) {
int masu[9][9];
int ans[9][9];

__CPROVER_assume(check(masu) == 1);
ans = masu;
assert(0);
}


masu[9][9] に何も値をセットしていません。
そのあと assume して数独の条件を満たしていると仮定し、
配列から配列への代入をして、値を画面表示させ、
最後にそんなものはありえないと assert します。

CBMCは assertが成り立たない反例を探します。
つまり 数独パズルを解いてくれます。

結局このプログラムは、何でもいいので何か1つ数独の条件を満たすものを求める、
というプログラムです。これを走らせると、


180392 variables, 757716 clauses
Verified 119293 original clauses.
SAT checker: negated claim is SATISFIABLE, i.e., does not hold
Runtime decision procedure: 104.813s

sudoku::main::1::ans={ { 5, 9, 8, 1, 3, 4, 2, 7, 6 }, { 1, 4, 2, 7, 9, 6, 5, 3
, 8 }, { 7, 6, 3, 5, 2, 8, 9, 1, 4 }, { 3, 8, 5, 6, 7, 9, 4, 2, 1 }, { 6, 1, 7,
4, 5, 2, 3, 8, 9 }, { 4, 2, 9, 8, 1, 3, 6, 5, 7 }, { 9, 7, 6, 3, 8, 5, 1, 4, 2 }
, { 8, 5, 4, 2, 6, 1, 7, 9, 3 }, { 2, 3, 1, 9, 4, 7, 8, 6, 5 } }

Violated property:
file sudoku.c line 76 function main
assertion
FALSE

VERIFICATION FAILED


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


104秒かかって、”適当”な答えが1つ求まりました。

ソースコード
sudoku1.c

その2へ続く

コメントの投稿

非公開コメント

プロフィール

島敏博

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リンクの表示