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
次回は、数値を求めるパズルではなくて、他の可能性をさぐってみます。
