Rustとkaniで数独を解く
κeenです。Twitterで面白そうなネタをみかけたのでやってみます。
元ネタはこちらの記事です。
分かる人向けに説明すると、モデルチェッカってSMT載ってるしコードで数独の制約を表現して反例出力させられるよねって内容です。それをRustでやってみます。
背景 - kaniについて
以前記事に書いたこともあるのですが、kaniはRustのモデル検査器です。Rustのプログラム受け取って未定義動作が起きないかやpanicが起きないかなどを検査してくれます。特に、panicが起きないか検査できるということはテストのように assert!(expr) を使ってある事柄が成り立つか成り立たないかを調べてくれます。このとき、kaniが成り立つと言えば必ず成り立つし、成り立たないと言えば少なくとも1つは反例となる入力があることが保証されます。
さらにまだ不安定なオプションですが、成り立たない場合にはその反例を出力することもできます。
kaniを使って数独を解かせる
kaniの反例を出力するオプションを使って数独を解かせることができます。 ある数独パズルが与えられたときに、Rustで「このパズルに正解はない」と宣言してそれをkaniに検査させます。するとkaniは「いや、このパズルに正解はあるよ。反例としてこういう埋め方したらちゃんと正解になってるよ」と解答を持ってきてくれる訳です。
やってみましょう。まずはプロジェクトを用意します。
$ cargo new kani-sudoku
$ cd kani-sudoku
9x9の数値が与えられたときに、それが数独の条件を満たしているかチェックする check 関数を定義してみます。
fn find(n: i32, a: i32, b: i32, c: i32, d: i32, e: i32, f: i32, g: i32, h: i32, i: i32) -> bool {
// aからiまでに nがあることを確認する
(n == a)
|| (n == b)
|| (n == c)
|| (n == d)
|| (n == e)
|| (n == f)
|| (n == g)
|| (n == h)
|| (n == i)
}
fn find9(a: i32, b: i32, c: i32, d: i32, e: i32, f: i32, g: i32, h: i32, i: i32) -> bool {
// aからiまでに 1から9までのすべてがあることを確認する
find(1, a, b, c, d, e, f, g, h, i)
&& find(2, a, b, c, d, e, f, g, h, i)
&& find(2, a, b, c, d, e, f, g, h, i)
&& find(3, a, b, c, d, e, f, g, h, i)
&& find(4, a, b, c, d, e, f, g, h, i)
&& find(5, a, b, c, d, e, f, g, h, i)
&& find(6, a, b, c, d, e, f, g, h, i)
&& find(7, a, b, c, d, e, f, g, h, i)
&& find(8, a, b, c, d, e, f, g, h, i)
&& find(9, a, b, c, d, e, f, g, h, i)
}
#[rustfmt::skip]
fn check(a: [[i32; 9]; 9]) -> bool {
// 数独の条件を満たしていることを確認する。
// ヨコ
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]) &&
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]) &&
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]) &&
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]) &&
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]) &&
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]) &&
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]) &&
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]) &&
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]) &&
// タテ
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]) &&
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]) &&
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]) &&
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]) &&
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]) &&
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]) &&
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]) &&
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]) &&
// マス
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]) &&
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]) &&
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]) &&
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]) &&
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]) &&
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]) &&
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]) &&
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]) &&
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])
}
この関数に空欄を適当に埋めたパズルを与えると、パズルに正解がなければ空欄にどんな数値を入れても false になりますし、正解があるならなら1つは true となる空欄の埋め方があります。
そこでkaniの機能を使って空欄のあるパズルを用意して、 assert!(!check(puzzle)); のように宣言すると「このpuzzleはどのような埋め方をしても正解にならない」という意味になり、kaniが反例を探してくれます。
空欄のあるパズルは以下のように作ります。パズルは [[i32; 9]; 9] のデータとし、数値が入ってるマスは普通に数値を入れます。空欄になっているマスには kani::any() を入れます。
// kani::anyに短い名前をつけておく
let g: fn() -> i32 = kani::any;
let puzzle: [[i32; 9]; 9] = [
[g(), g(), g(), 3, g(), g(), g(), 9, g()],
[g(), 4, g(), g(), g(), g(), g(), g(), 2],
[ 1, g(), g(), g(), 8, g(), 5, g(), g()],
[g(), g(), 8, g(), g(), 9, g(), g(), 7],
[g(), 2, g(), g(), g(), g(), g(), 3, g()],
[ 4, g(), g(), 7, g(), g(), 1, g(), g()],
[g(), g(), 3, g(), 5, g(), g(), g(), 6],
[ 5, g(), g(), g(), g(), g(), g(), 8, g()],
[g(), 9, g(), g(), g(), 1, g(), g(), g()],
];
kani::any() はその型の値ならなんでもOKという宣言です。kani側の裁量で好きな値を埋められます。数独は本来は1から9までしか入りませんが、 check 関数に1から9以外の値を入れても問題なく動くので支障はないでしょう。
ということで proof 関数を以下のように定義しましょう。
#[cfg(kani)]
#[kani::proof]
#[rustfmt::skip]
fn proof() {
let g: fn() -> i32 = kani::any;
let puzzle: [[i32; 9]; 9] = [
[g(), g(), g(), 3, g(), g(), g(), 9, g()],
[g(), 4, g(), g(), g(), g(), g(), g(), 2],
[ 1, g(), g(), g(), 8, g(), 5, g(), g()],
[g(), g(), 8, g(), g(), 9, g(), g(), 7],
[g(), 2, g(), g(), g(), g(), g(), 3, g()],
[ 4, g(), g(), 7, g(), g(), 1, g(), g()],
[g(), g(), 3, g(), 5, g(), g(), g(), 6],
[ 5, g(), g(), g(), g(), g(), g(), 8, g()],
[g(), 9, g(), g(), g(), 1, g(), g(), g()],
];
assert!(!check(puzzle));
}
これであとはkaniに解かせるだけです。反例を表示させるために concrete-playback オプションを使います。
ちょっと長いですが、以下のような出力が得られます。
$ cargo kani --fail-fast -Zconcrete-playback --concrete-playback print
Kani Rust Verifier 0.67.0 (cargo plugin)
Compiling kani-sudoku v0.1.0 (/home/shun/Rust/kani-sudoku)
Finished `dev` profile [unoptimized + debuginfo] target(s) in 0.19s
Checking harness proof...
CBMC 6.8.0 (cbmc-6.8.0)
CBMC version 6.8.0 (cbmc-6.8.0) 64-bit x86_64 linux
...skip...
SUMMARY:
** 1 of 1055 failed
Failed Checks: assertion failed: !check(masu)
File: "src/main.rs", line 79, in proof
VERIFICATION:- FAILED
Verification Time: 82.52442s
Concrete playback unit test for `proof`:
```
/// Test generated for harness `proof`
///
/// Check for `assertion`: "assertion failed: !check(masu)"
#[test]
fn kani_concrete_playback_proof_17227887837670858443() {
let concrete_vals: Vec<Vec<u8>> = vec![
// 8
vec![8, 0, 0, 0],
// 5
vec![5, 0, 0, 0],
// 2
vec![2, 0, 0, 0],
// 4
vec![4, 0, 0, 0],
// 7
vec![7, 0, 0, 0],
// 6
vec![6, 0, 0, 0],
// 1
vec![1, 0, 0, 0],
// 3
vec![3, 0, 0, 0],
// 6
vec![6, 0, 0, 0],
// 1
vec![1, 0, 0, 0],
// 9
vec![9, 0, 0, 0],
// 5
vec![5, 0, 0, 0],
// 8
vec![8, 0, 0, 0],
// 7
vec![7, 0, 0, 0],
// 7
vec![7, 0, 0, 0],
// 9
vec![9, 0, 0, 0],
// 6
vec![6, 0, 0, 0],
// 2
vec![2, 0, 0, 0],
// 4
vec![4, 0, 0, 0],
// 3
vec![3, 0, 0, 0],
// 6
vec![6, 0, 0, 0],
// 1
vec![1, 0, 0, 0],
// 4
vec![4, 0, 0, 0],
// 3
vec![3, 0, 0, 0],
// 2
vec![2, 0, 0, 0],
// 5
vec![5, 0, 0, 0],
// 9
vec![9, 0, 0, 0],
// 7
vec![7, 0, 0, 0],
// 5
vec![5, 0, 0, 0],
// 1
vec![1, 0, 0, 0],
// 6
vec![6, 0, 0, 0],
// 4
vec![4, 0, 0, 0],
// 8
vec![8, 0, 0, 0],
// 3
vec![3, 0, 0, 0],
// 5
vec![5, 0, 0, 0],
// 2
vec![2, 0, 0, 0],
// 8
vec![8, 0, 0, 0],
// 6
vec![6, 0, 0, 0],
// 9
vec![9, 0, 0, 0],
// 2
vec![2, 0, 0, 0],
// 8
vec![8, 0, 0, 0],
// 9
vec![9, 0, 0, 0],
// 4
vec![4, 0, 0, 0],
// 7
vec![7, 0, 0, 0],
// 1
vec![1, 0, 0, 0],
// 6
vec![6, 0, 0, 0],
// 1
vec![1, 0, 0, 0],
// 2
vec![2, 0, 0, 0],
// 7
vec![7, 0, 0, 0],
// 3
vec![3, 0, 0, 0],
// 9
vec![9, 0, 0, 0],
// 4
vec![4, 0, 0, 0],
// 7
vec![7, 0, 0, 0],
// 4
vec![4, 0, 0, 0],
// 8
vec![8, 0, 0, 0],
// 6
vec![6, 0, 0, 0],
// 3
vec![3, 0, 0, 0],
// 2
vec![2, 0, 0, 0],
// 5
vec![5, 0, 0, 0],
];
kani::concrete_playback_run(concrete_vals, proof);
}
```
INFO: To automatically add the concrete playback unit test(s) to the src code, run Kani with `--concrete-playback=inplace`.
Manual Harness Summary:
Verification failed for - proof
Complete - 0 successfully verified harnesses, 1 failures, 1 total.
末尾の方にユニットテストが生成されました。このテストに入っている数値を前から順番に kani::any の部分を置き換えるようにして埋めると反例になっている(=数独を解いた結果になる)はずです。
本当に解けているか検査してみましょう。check 関数に全マス埋めたデータを渡してあげれば検算してくれます。
fn main() {
// 元のパズルに加えてanyの部分を手動で埋めたもの
let puzzle: [[i32; 9]; 9] = [
[8, 5, 2, 3, 4, 7, 6, 9, 1],
[3, 4, 6, 1, 9, 5, 8, 7, 2],
[1, 7, 9, 6, 8, 2, 5, 4, 3],
[6, 1, 8, 4, 3, 9, 2, 5, 7],
[9, 2, 7, 5, 1, 6, 4, 3, 8],
[4, 3, 5, 7, 2, 8, 1, 6, 9],
[2, 8, 3, 9, 5, 4, 7, 1, 6],
[5, 6, 1, 2, 7, 3, 9, 8, 4],
[7, 9, 4, 8, 6, 1, 3, 2, 5],
];
assert!(check(puzzle));
}
これを走らせてパニックにならなければOKです。
$ cargo run
Compiling kani-sudoku v0.1.0 (/home/shun/Rust/kani-sudoku)
Finished `dev` profile [unoptimized + debuginfo] target(s) in 0.11s
Running `target/debug/kani-sudoku`
無事正常終了したので解けているようです。
まとめ
Rustのモデル検査ツールであるkaniを使って数独を解かせてみました。シンプルにRustのコードでSMTに解かせる制約を表現できるという小ネタとしても面白いですが、モデル検査ツールがこういった制約の元に色々探索して望ましい結果になるかをみてくれるツールというのが実感しやすい例でもあるんじゃないでしょうか。
今回のコードを以下に置いておきます。展開して参照して下さい。
今回のコード
fn find(n: i32, a: i32, b: i32, c: i32, d: i32, e: i32, f: i32, g: i32, h: i32, i: i32) -> bool {
// aからiまでに nがあることを確認する
(n == a)
|| (n == b)
|| (n == c)
|| (n == d)
|| (n == e)
|| (n == f)
|| (n == g)
|| (n == h)
|| (n == i)
}
fn find9(a: i32, b: i32, c: i32, d: i32, e: i32, f: i32, g: i32, h: i32, i: i32) -> bool {
// aからiまでに 1から9までのすべてがあることを確認する
find(1, a, b, c, d, e, f, g, h, i)
&& find(2, a, b, c, d, e, f, g, h, i)
&& find(2, a, b, c, d, e, f, g, h, i)
&& find(3, a, b, c, d, e, f, g, h, i)
&& find(4, a, b, c, d, e, f, g, h, i)
* && find(5, a, b, c, d, e, f, g, h, i)
&& find(6, a, b, c, d, e, f, g, h, i)
&& find(7, a, b, c, d, e, f, g, h, i)
&& find(8, a, b, c, d, e, f, g, h, i)
&& find(9, a, b, c, d, e, f, g, h, i)
}
#[rustfmt::skip]
fn check(a: [[i32; 9]; 9]) -> bool {
// 数独の条件を満たしていることを確認する。
// ヨコ
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]) &&
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]) &&
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]) &&
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]) &&
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]) &&
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]) &&
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]) &&
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]) &&
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]) &&
// タテ
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]) &&
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]) &&
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]) &&
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]) &&
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]) &&
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]) &&
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]) &&
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]) &&
// マス
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]) &&
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]) &&
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]) &&
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]) &&
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]) &&
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]) &&
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]) &&
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]) &&
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])
}
#[cfg(kani)]
#[kani::proof]
#[rustfmt::skip]
fn proof() {
let g: fn() -> i32 = kani::any;
let puzzle: [[i32; 9]; 9] = [
[g(), g(), g(), 3, g(), g(), g(), 9, g()],
[g(), 4, g(), g(), g(), g(), g(), g(), 2],
[ 1, g(), g(), g(), 8, g(), 5, g(), g()],
[g(), g(), 8, g(), g(), 9, g(), g(), 7],
[g(), 2, g(), g(), g(), g(), g(), 3, g()],
[ 4, g(), g(), 7, g(), g(), 1, g(), g()],
[g(), g(), 3, g(), 5, g(), g(), g(), 6],
[ 5, g(), g(), g(), g(), g(), g(), 8, g()],
[g(), 9, g(), g(), g(), 1, g(), g(), g()],
];
assert!(!check(puzzle));
}
fn main() {
let puzzle: [[i32; 9]; 9] = [
[8, 5, 2, 3, 4, 7, 6, 9, 1],
[3, 4, 6, 1, 9, 5, 8, 7, 2],
[1, 7, 9, 6, 8, 2, 5, 4, 3],
[6, 1, 8, 4, 3, 9, 2, 5, 7],
[9, 2, 7, 5, 1, 6, 4, 3, 8],
[4, 3, 5, 7, 2, 8, 1, 6, 9],
[2, 8, 3, 9, 5, 4, 7, 1, 6],
[5, 6, 1, 2, 7, 3, 9, 8, 4],
[7, 9, 4, 8, 6, 1, 3, 2, 5],
];
assert!(check(puzzle));
}
余談
ところで、ちょっと例に出したコードが野暮ったいと思いませんでしたか？ .contains() とか .all() とかを使えばもっとスマートに書けそうです。ところがこれらの関数を呼ぶとコントロールフローが複雑になって検査にものすごく時間がかかりました。途中で止めてしまったので正確には分かりませんが、数百倍くらい遅くなっているようでした。厳しいですね。