--
--
スポンサーサイト
--.--.--(--:--)
上記の広告は１ヶ月以上更新のないブログに表示されています。
新しい記事を書く事で広告が消せます。
新しい記事を書く事で広告が消せます。
カテゴリ：有界モデル検査技術 CBMC の記事一覧
- スポンサーサイト
- CBMCを使って数独パズルを解く その３
- CBMCを使って数独パズルを解く その２
- CBMCを使って数独パズルを解く その１
- 有界モデル検査技術 CBMC その2
- 有界モデル検査技術 CBMC その1
07
04
CBMCを使って数独パズルを解く その３
2010.07.04(17:41)
数独の答えはほんとうに１つなんでしょうか？ まあまともに出題されている問題であれば、出題から解いてゆけば解答は一意に決まるんでしょうね。
それを確かめるソースコードを書いてみました。
２つの結果を比較する compare()
配列に対して出題をセットする shutudai()
これらを使った main()
を用意しました。まずこのプログラムが合っていることを確認するために、
mainの一番最後に、
解が求まって かつ その解が適当に作った配列と違っている という assert
を書いて実行してみます。解は１つはあるはずです。
出題は前回のと違ってちょっと難しいのにしてみました。
解がもとまり、適当な解もそれと同じものにすれば、反例になりました。
次に、
２つ解が求まって かつ それらが一致している という assert
を書いて実行してみます。
反例が見つかれば、解が少なくとも２つあることになります。
その結果は、
503秒かかって、反例が見つからないことが証明されてしました。
この問題には解は１つしかないようです。
あまり面白くないので、問題のほうを変更して、値が設定してあるマスを
半分にしてみました。条件をゆるめると可能性が増えるので計算時間はよりかかるはず。
497秒かかって、反例が１つ見つかりました。
最初に埋めるマスを減らせば、解が２つ見つかることがあることはわかりました。
何かあやしい問題があったら、このソースコードを使ってチェックしてみようと思います。
ソースコード
sudoku4.c
次回は、数値を求めるパズルではなくて、他の可能性をさぐってみます。
それを確かめるソースコードを書いてみました。
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);
}
２つの結果を比較する compare()
配列に対して出題をセットする shutudai()
これらを使った main()
を用意しました。まずこのプログラムが合っていることを確認するために、
mainの一番最後に、
解が求まって かつ その解が適当に作った配列と違っている という assert
を書いて実行してみます。解は１つはあるはずです。
出題は前回のと違ってちょっと難しいのにしてみました。
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 }
解がもとまり、適当な解もそれと同じものにすれば、反例になりました。
次に、
２つ解が求まって かつ それらが一致している という assert
を書いて実行してみます。
反例が見つかれば、解が少なくとも２つあることになります。
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秒かかって、反例が見つからないことが証明されてしました。
この問題には解は１つしかないようです。
あまり面白くないので、問題のほうを変更して、値が設定してあるマスを
半分にしてみました。条件をゆるめると可能性が増えるので計算時間はよりかかるはず。
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秒かかって、反例が１つ見つかりました。
最初に埋めるマスを減らせば、解が２つ見つかることがあることはわかりました。
何かあやしい問題があったら、このソースコードを使ってチェックしてみようと思います。
ソースコード
sudoku4.c
次回は、数値を求めるパズルではなくて、他の可能性をさぐってみます。
スポンサーサイト
07
04
CBMCを使って数独パズルを解く その２
2010.07.04(00:34)
前回のソースコードに問題をいれます。
ニコリ公式パズルガイド「数独」-WEBニコリ
http://www.nikoli.co.jp/ja/puzzles/sudoku/
の最初の問題にします。
数字が埋まっているところをいれてみると、9 x 9 の配列はこうなっています。
mainを書き換えて、値がはいっているところだけいれて、
そのあとで、数独の条件を満たしていることを assumeします。
これを実行すると、
制約を加えると選択肢が狭まるので
今回は 70秒で答えが求まりました。
問題と求まった答えを並べてみます。
きちんと解けていますね。
ソースコード
sudoku2.c
ニコリ公式パズルガイド「数独」-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
07
04
CBMCを使って数独パズルを解く その１
2010.07.04(00:33)
今度はCBMCを使って、数独パズルの問題を解いてみます。まずソースコードです。
masu[9][9] に何も値をセットしていません。
そのあと assume して数独の条件を満たしていると仮定し、
配列から配列への代入をして、値を画面表示させ、
最後にそんなものはありえないと assert します。
CBMCは assertが成り立たない反例を探します。
つまり 数独パズルを解いてくれます。
結局このプログラムは、何でもいいので何か１つ数独の条件を満たすものを求める、
というプログラムです。これを走らせると、
104秒かかって、”適当”な答えが１つ求まりました。
ソースコード
sudoku1.c
その２へ続く
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が成り立たない反例を探します。
つまり 数独パズルを解いてくれます。
結局このプログラムは、何でもいいので何か１つ数独の条件を満たすものを求める、
というプログラムです。これを走らせると、
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秒かかって、”適当”な答えが１つ求まりました。
ソースコード
sudoku1.c
その２へ続く
06
15
有界モデル検査技術 CBMC その2
2010.06.15(20:55)
CBMCを使って、まほうじんを解いてみましょう。
assert(0)が実行されたとき、まほうじんが解けています。
これをCBMCにかけると、 assert(0)が失敗するような、数字の組み合わせを見つけてくれます。
6 1 8
7 5 3
2 9 4
確かに3x3のまほうじんが解けています。プログラムを修正し、先頭のほうに、
__CPROVER_assume(masu[4] != 5);
を追加します。つまりちょうど真ん中が 5ではないと条件を追加してみます。
反例を見つけることができませんでした。3x3のまほうじんでは、真ん中は必ず 5 になることがわかりました。
先頭で定義されているNUMを4にすると4x4のまほうじんが、5にすると5x5のまほうじんが解けます。
3と4は一瞬で解けますが、5はかなり時間がかかります。PCの性能によりますが私のPCの場合、141秒ぐらいかかりました。画面が何も変わらないのでじっと待ちます。
このようにして、プログラムがそこを通過するときに、失敗するようなassertをいれておけば、プログラムがそこを通過する条件がないか総当たりで調べてくれます。
たとえば、ある関数を、引き数がNULLでは絶対に呼んでほしくないときに、NULLで呼び出してくる場所を総当たりで調べてくれる、という使い方ができます。
CBMCは、モデル検査に使うツールなのですが、このように、C言語で使え、モデル全部ができあがっていなくても、1関数だけでも使い道があるところがすばらしいです。
続く。
#define NUM 3
int solve(void) {
// マス目の数
int masu[NUM*NUM];
// マス目の数の合計 縦 NUM個、横 NUM個、斜め 2個
int sum[NUM*2+2];
int ans[NUM*NUM];
int check;
int i, j;
int sum_index;
// すべてのマスの値は、0より大きく、マス目の数より小さい
for(i = 0; i < NUM*NUM; i++){
__CPROVER_assume(masu[i] > 0 && masu[i] < NUM*NUM+1);
}
// すべてのマスの値は異なる
for(i = 0; i < NUM*NUM; i++){
for(j = i+1; j < NUM*NUM; j++){
__CPROVER_assume(masu[i] != masu[j]);
}
}
// 縦横の合計
for(i = 0; i < NUM; i++){
sum[i] = 0;
sum[NUM + i] = 0;
for(j = 0; j < NUM; j++){
sum[i] += masu[i*NUM+j];
sum[NUM + i] += masu[i+NUM*j];
}
}
// 斜めの合計
sum[NUM*2 + 0] = 0:
sum[NUM*2 + 1] = 0;
for(j = 0; j < NUM; j++){
sum[NUM*2 + 0] += masu[0 +(NUM+1)*j];
sum[NUM*2 + 1] += masu[(NUM-1)+(NUM-1)*j];
}
// 合計がすべて一致すると assertで落とす
check = 1;
for(i = 0; i < NUM*2+2-1; i++){
check &= (sum[i] == sum[i+1]);
}
if(check){
ans = masu; // 代入文
assert(0);
}
}
assert(0)が実行されたとき、まほうじんが解けています。
これをCBMCにかけると、 assert(0)が失敗するような、数字の組み合わせを見つけてくれます。
D:\CBMC>cbmc mahoujin.c --function solve
... 中略 ...
State 354 file mahoujin.c line 49 function solve thread 0
----------------------------------------------------
mahoujin::solve::1::ans={ 6, 1, 8, 7, 5, 3, 2, 9, 4 }
Violated property:
file mahoujin.c line 50 function solve
assertion
FALSE
VERIFICATION FAILED
6 1 8
7 5 3
2 9 4
確かに3x3のまほうじんが解けています。プログラムを修正し、先頭のほうに、
__CPROVER_assume(masu[4] != 5);
を追加します。つまりちょうど真ん中が 5ではないと条件を追加してみます。
... 中略 ...
Runtime decision procedure: 0.312s
VERIFICATION SUCCESSFUL
反例を見つけることができませんでした。3x3のまほうじんでは、真ん中は必ず 5 になることがわかりました。
先頭で定義されているNUMを4にすると4x4のまほうじんが、5にすると5x5のまほうじんが解けます。
4の場合
...
Runtime decision procedure: 3.5s
...
State 808 file mahoujin.c line 49 function solve thread 0
----------------------------------------------------
mahoujin::solve::1::ans={ 4, 7, 10, 13, 14, 16, 1, 3, 5, 9, 8, 12, 11, 2, 15, 6}
5の場合
...
Runtime decision procedure: 141.032s
...
State 1674 file mahoujin.c line 49 function solve thread 0
----------------------------------------------------
mahoujin::solve::1::ans={ 6, 22, 10, 19, 8, 3, 18, 12, 23, 9, 24, 13, 16, 5, 7 , 15, 1, 25, 4, 20, 17, 11, 2, 14, 21 }
3と4は一瞬で解けますが、5はかなり時間がかかります。PCの性能によりますが私のPCの場合、141秒ぐらいかかりました。画面が何も変わらないのでじっと待ちます。
このようにして、プログラムがそこを通過するときに、失敗するようなassertをいれておけば、プログラムがそこを通過する条件がないか総当たりで調べてくれます。
たとえば、ある関数を、引き数がNULLでは絶対に呼んでほしくないときに、NULLで呼び出してくる場所を総当たりで調べてくれる、という使い方ができます。
CBMCは、モデル検査に使うツールなのですが、このように、C言語で使え、モデル全部ができあがっていなくても、1関数だけでも使い道があるところがすばらしいです。
続く。
06
15
有界モデル検査技術 CBMC その1
2010.06.15(10:12)
CBMC (Bounded Model Checking for C/C++)
http://www.cprover.org/cbmc/
は、米国CMUで開発された有界モデル検査技術です。
有界モデル検査とは何なのか説明をとばして、いきなり使ってみることにします。
インストール方法
http://www.cprover.org/cbmc/
の中頃にある、
CBMC for Windows: cbmc-3-6-win.zip Unzip the archive before running. You will need CL (comes with Microsoft Visual Studio) in your PATH for preprocessing.
をダウンロードしてきて解凍する。
D:\CBMC に解凍したとします。
使い方
Microsoft Visual Studio 2008 の場合で説明します。
Microsoft Visual Studio 2008 - Visual Studio Tools - Visual Stdio 2008 コマンドプロンプトを起動
その中で、D:\CBMC に移動して、
D:\CBMC>cbmc --version
3.6
さてプログラムを解析してゆきましょう。最初のプログラムです。
なんとも奇妙なCプルグラムですが、以下のように読みます。
(i+j) が10でないことは常に成立する。
おかしいですね。1と9、5と5などで成立しないことは明らかです。
CBMCは、assertが失敗する条件が作れないか徹底的に探してくれます。
CBMCは、プログラムが完全にできあがっていなくても解析してくれます。
コマンドラインから以下のように入力すると、
-function foo は、fooという名前の関数をスタートポイントにして解析する、という指定です。
デフォルトは int main(int argc,char**argv); をスタートポイントにして調べます。
大切なのは最後の5行です。
VERIFICATION FAILED と出て、assertが失敗する例 (反例といいます)が存在することが報告されています。
反例が見つかったときの、i とjの値が知りたいので、プログラムを少し修正します。
iをiに、jをjに、つまり自分自身に値を代入しています。それ自体に意味はないのですが、CBMCは、代入文を実行するときに、その値をトレースして表示 してくれます。
反例として、5と5が見つかりました。このように、CBMCは、プログラムは実行しないのですが、反例を見つけることができます。
さらにプログラムを修正します。
__CPROVER_assume() というのは、プログラムがここを通過するときに、この条件は成立していると見なす、
というふうに読みます。CPROVERの前のアンダースコアは2つ、後のアンダースコアは1つです
__CPROVER_assume(i < 2);
__CPROVER_assume(j > 8);
となっているので、プログラムがここを通過するときに iは2より小さくて、jは8より大きいと見なす、
となります。__CPROVER_assumeのことを、関数fooの事前条件、assertのほうを事後条件と呼びます。
これで実行すると、今度は反例が 1,9 になりました。事前条件を満たしている反例として、1,9 を選んでくれたわけです。
このようにして、事前条件を満たし、事後条件を満たさない値を見つけることができます。
このようなしくみを使って、
assert(問題が解けない)
という書き方をすると、それの反例を総当たりで探し出し、問題が解ける例を探すことができます。
CBMC は、値が代入されると、トレースにその値を表示しますが、printfを使う方法もあります。
このように、<stdio.h>をインクルードして、printf 文を普通に書いておくと、
プログラム自身は実行しないのですが、 printf など標準出力に出力するような文は実行してくれて、
と値を確認することができます。上記のどちらかを使えば、反例の値を知ることができます。
この総当たりのしくみを使って、問題を解いてみましょう。
その２へ
http://www.cprover.org/cbmc/
は、米国CMUで開発された有界モデル検査技術です。
有界モデル検査とは何なのか説明をとばして、いきなり使ってみることにします。
インストール方法
http://www.cprover.org/cbmc/
の中頃にある、
CBMC for Windows: cbmc-3-6-win.zip Unzip the archive before running. You will need CL (comes with Microsoft Visual Studio) in your PATH for preprocessing.
をダウンロードしてきて解凍する。
D:\CBMC に解凍したとします。
使い方
Microsoft Visual Studio 2008 の場合で説明します。
Microsoft Visual Studio 2008 - Visual Studio Tools - Visual Stdio 2008 コマンドプロンプトを起動
その中で、D:\CBMC に移動して、
D:\CBMC>cbmc --version
3.6
さてプログラムを解析してゆきましょう。最初のプログラムです。
int foo(int i,int j) {
assert ((i+j) != 10);
}なんとも奇妙なCプルグラムですが、以下のように読みます。
(i+j) が10でないことは常に成立する。
おかしいですね。1と9、5と5などで成立しないことは明らかです。
CBMCは、assertが失敗する条件が作れないか徹底的に探してくれます。
CBMCは、プログラムが完全にできあがっていなくても解析してくれます。
コマンドラインから以下のように入力すると、
D:\CBMC>cbmc file1.c --function foo
file file1.c: Parsing
file1.c Converting
Type-checking file1
Generating GOTO Program
Function Pointer Removal
Starting Bounded Model Checking
size of program expression: 11 assignments
simple slicing removed 0 assignments
Generated 1 VCC(s), 1 remaining after simplification
Passing problem to propositional reduction
Running propositional reduction
Solving with MiniSAT2 without simplifier
281 variables, 730 clauses
Verified 608 original clauses.
SAT checker: negated claim is SATISFIABLE, i.e., does not hold
Runtime decision procedure: 0s
Building error trace
Counterexample:
State 1 fileline 12 thread 0
----------------------------------------------------
__CPROVER_alloc=(assignment removed)
State 2 fileline 13 thread 0
----------------------------------------------------
__CPROVER_alloc_size=(assignment removed)
State 3 fileline 14 thread 0
----------------------------------------------------
__func__=(assignment removed)
State 4 fileline 20 thread 0
----------------------------------------------------
__CPROVER_rounding_mode=0 (00000000000000000000000000000000)
Violated property:
file file1.c line 4 function foo
assertion
FALSE
VERIFICATION FAILED
-function foo は、fooという名前の関数をスタートポイントにして解析する、という指定です。
デフォルトは int main(int argc,char**argv); をスタートポイントにして調べます。
大切なのは最後の5行です。
VERIFICATION FAILED と出て、assertが失敗する例 (反例といいます)が存在することが報告されています。
反例が見つかったときの、i とjの値が知りたいので、プログラムを少し修正します。
void foo(int i,int j)
{
if ((i + j) == 10) {
i = i;
j = j;
assert(0);
}
}
iをiに、jをjに、つまり自分自身に値を代入しています。それ自体に意味はないのですが、CBMCは、代入文を実行するときに、その値をトレースして表示 してくれます。
State 9 file file1.c line 4 function foo thread 0
----------------------------------------------------
file1::foo::i=5 (00000000000000000000000000000101)
State 10 file file1.c line 5 function foo thread 0
----------------------------------------------------
file1::foo::j=5 (00000000000000000000000000000101)
Violated property:
file file1.c line 6 function foo
assertion
FALSE
VERIFICATION FAILED
反例として、5と5が見つかりました。このように、CBMCは、プログラムは実行しないのですが、反例を見つけることができます。
さらにプログラムを修正します。
void foo(int i,int j)
{
__CPROVER_assume(i < 2);
__CPROVER_assume(j > 8);
if ((i + j) == 10) {
i = i;
j = j;
assert(0):
}
}
__CPROVER_assume() というのは、プログラムがここを通過するときに、この条件は成立していると見なす、
というふうに読みます。CPROVERの前のアンダースコアは2つ、後のアンダースコアは1つです
__CPROVER_assume(i < 2);
__CPROVER_assume(j > 8);
となっているので、プログラムがここを通過するときに iは2より小さくて、jは8より大きいと見なす、
となります。__CPROVER_assumeのことを、関数fooの事前条件、assertのほうを事後条件と呼びます。
State 11 file file1.c line 6 function foo thread 0
----------------------------------------------------
file1::foo::i=1 (00000000000000000000000000000001)
State 12 file file1.c line 7 function foo thread 0
----------------------------------------------------
file1::foo::j=9 (00000000000000000000000000001001)
Violated property:
file file1.c line 8 function foo
assertion
FALSE
VERIFICATION FAILED
これで実行すると、今度は反例が 1,9 になりました。事前条件を満たしている反例として、1,9 を選んでくれたわけです。
このようにして、事前条件を満たし、事後条件を満たさない値を見つけることができます。
このようなしくみを使って、
assert(問題が解けない)
という書き方をすると、それの反例を総当たりで探し出し、問題が解ける例を探すことができます。
CBMC は、値が代入されると、トレースにその値を表示しますが、printfを使う方法もあります。
#include <stdio.h>
int foo(int i,int j){
__CPROVER_assume(i < 2);
__CPROVER_assume(j > 8);
if ((i+j) == 10) {
printf("counterexample %d %d\n",i,j);
assert(0);
}
}
このように、<stdio.h>をインクルードして、printf 文を普通に書いておくと、
プログラム自身は実行しないのですが、 printf など標準出力に出力するような文は実行してくれて、
counterexample 1 9
Violated property:
file file1.c line 7 function foo
assertion
FALSE
VERIFICATION FAILED
と値を確認することができます。上記のどちらかを使えば、反例の値を知ることができます。
この総当たりのしくみを使って、問題を解いてみましょう。
その２へ
