07

04

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

2010.07.04(00:34)

前回のソースコードに問題をいれます。
ニコリ公式パズルガイド「数独」-WEBニコリ
http://www.nikoli.co.jp/ja/puzzles/sudoku/
の最初の問題にします。

数字が埋まっているところをいれてみると、9 x 9 の配列はこうなっています。



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



mainを書き換えて、値がはいっているところだけいれて、
そのあとで、数独の条件を満たしていることを assumeします。


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

masu[0][2] = 6; masu[0][8] = 1;
masu[1][1] = 7; masu[1][4] = 6; masu[1][7] = 5;
masu[2][0] = 8; masu[2][3] = 1; masu[2][5] = 3; masu[2][6] = 2;

masu[3][2] = 5; masu[3][4] = 4; masu[3][6] = 8;
masu[4][1] = 4; masu[4][3] = 7; masu[4][5] = 2; masu[4][7] = 9;
masu[5][2] = 8; masu[5][4] = 1; masu[5][6] = 7;

masu[6][2] = 1; masu[6][3] = 2; masu[6][5] = 5; masu[6][8] = 3;
masu[7][1] = 6; masu[7][4] = 7; masu[7][7] = 8;
masu[8][0] = 2; masu[8][6] = 4;

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


これを実行すると、


D:\CBMC>cbmc sudoku.c
file sudoku.c: Parsing
sudoku.c
Converting
Type-checking sudoku
tmp.stdin5752.c
Generating GOTO Program
Function Pointer Removal
Starting Bounded Model Checking
size of program expression: 13428 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
178752 variables, 721900 clauses
Verified 78097 original clauses.
SAT checker: negated claim is SATISFIABLE, i.e., does not hold
Runtime decision procedure: 70.531s
Building error trace

Counterexample:

... 略 ...

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

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

VERIFICATION FAILED



制約を加えると選択肢が狭まるので
今回は 70秒で答えが求まりました。
問題と求まった答えを並べてみます。


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

求まった答え
{ 5, 3, 6, 8, 2, 7, 9, 4, 1 },
{ 1, 7, 2, 9, 6, 4, 3, 5, 8 },
{ 8, 9, 4, 1, 5, 3, 2, 6, 7 },
{ 7, 1, 5, 3, 4, 9, 8, 2, 6 },
{ 6, 4, 3, 7, 8, 2, 1, 9, 5 },
{ 9, 2, 8, 5, 1, 6, 7, 3, 4 },
{ 4, 8, 1, 2, 9, 5, 6, 7, 3 },
{ 3, 6, 9, 4, 7, 1, 5, 8, 2 },
{ 2, 5, 7, 6, 3, 8, 4, 1, 9 }


きちんと解けていますね。

ソースコード
sudoku2.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リンクの表示