07
04
CBMCを使って数独パズルを解く その3
2010.07.04(17:41)
数独の答えはほんとうに1つなんでしょうか? まあまともに出題されている問題であれば、出題から解いてゆけば解答は一意に決まるんでしょうね。
それを確かめるソースコードを書いてみました。
2つの結果を比較する compare()
配列に対して出題をセットする shutudai()
これらを使った main()
を用意しました。まずこのプログラムが合っていることを確認するために、
mainの一番最後に、
解が求まって かつ その解が適当に作った配列と違っている という assert
を書いて実行してみます。解は1つはあるはずです。
出題は前回のと違ってちょっと難しいのにしてみました。
解がもとまり、適当な解もそれと同じものにすれば、反例になりました。
次に、
2つ解が求まって かつ それらが一致している という assert
を書いて実行してみます。
反例が見つかれば、解が少なくとも2つあることになります。
その結果は、
503秒かかって、反例が見つからないことが証明されてしました。
この問題には解は1つしかないようです。
あまり面白くないので、問題のほうを変更して、値が設定してあるマスを
半分にしてみました。条件をゆるめると可能性が増えるので計算時間はよりかかるはず。
497秒かかって、反例が1つ見つかりました。
最初に埋めるマスを減らせば、解が2つ見つかることがあることはわかりました。
何かあやしい問題があったら、このソースコードを使ってチェックしてみようと思います。
ソースコード
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);
}
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
次回は、数値を求めるパズルではなくて、他の可能性をさぐってみます。