for a SAT solver developer

25日のHacker Newsで初めて知ったMiracle Sudoku。ビデオの横に書いてあることから判断するに

• Normal Sudoku rules apply.
• ナイトまたはキングが1hopで行ける場所には同じ数は置けない: Any two cells separated by a knight's move or a king's move (in chess) cannot contain the same digit.
• 近接した4近傍には連続する数列は置けない: Any two orthogonally adjacent cells cannot contain consecutive digits.

さあSATソルバの出番。

2020-05-30 mokumoku

場所とセルの状態をそれぞれ構造体Pos, Cellで表現すると

• fn state(Pos, digit: usize, bool) -> Cell　で状態を生成
• fn requires(Cell, Cell) -> [i32; 2] で制約節を生成
• fn valid(Pos) -> Option<Pos> で妥当なセル座標に限定

といった補助関数を用意すれば後は簡単。

ナイトまたはキングが1hopで行ける場所には同じ数は置けない

まず、移動可能なベクターを用意。

    let knights_moves = [
        Pos::at(-2, 1),
        Pos::at(-1, 2),
        Pos::at(1, 2),
        Pos::at(2, 1),
        Pos::at(2, -1),
        Pos::at(1, -2),
        Pos::at(-1, -2),
        Pos::at(-2, -1),
    ];

全ての位置で移動して、妥当な場所なら全ての数字に対して禁止ルールを追加。

    let mut rules = Vec::new();
    for i in 1..=RANGE {
        for j in 1..=RANGE {
            let p = Pos::at(i, j);
            for m in moves.iter() {
                if let Some(t) = (p + *m).valid() {
                    for d in 1..=RANGE as usize {
                        rules.push(p.state(d, true).requires(t.state(d, false)));
                    }
                }
            }
        }
    }

キングについても同様。

近接した4近傍には連続する数列は置けない

ほぼ同じ考えでいける。連続した数列なのでそこだけ変更。

    let dirs = [
        Pos::at(-1, 0), // North
        Pos::at(0, 1),  // East
        Pos::at(1, 0),  // South
        Pos::at(0, -1), // West
    ];
    let mut rules = Vec::new();
    for i in 1..=RANGE {
        for j in 1..=RANGE {
            let p = Pos::at(i, j);
            for m in dirs.iter() {
                if let Some(t) = (p + *m).valid() {
                    for d in 1..RANGE as usize {
                        rules.push(p.state(d, true).requires(t.state(d + 1, false)));
                    }
                }
            }
        }
    }

SATソルバを呼び出す

rulesがVec<Vec<i32>>の形なので、後はSplrを呼び出すだけ。

    let rules: Vec<Vec<i32> = make_rules();
    let mut solver = Solver::try_from((Config::default(), rules.as_ref())).expect("panic");
    // 初期状態
    solver.add_assignment(Pos::at(5, 3).state(1, true).as_lit()).expect("panic");
    solver.add_assignment(Pos::at(6, 7).state(2, true).as_lit()).expect("panic");
    for ans in solver.iter() {
        // 正リテラルだけ抽出
        let picked = ans.iter().filter(|l| 0 < **l).collect::<Vec<&i32>>();
        println!(-);
    }

できたプログラムはこちら。

座標やリテラルは1で始まる一方で、Vec は0で始まるといったあたりでいつものようにバグを発生させてしまった けど、200行程度でできました。

実行結果

得られる出力は以下の通り。

4 8 3 7 2 6 1 5 9 
7 2 6 1 5 9 4 8 3 
1 5 9 4 8 3 7 2 6 
8 3 7 2 6 1 5 9 4 
2 6 1 5 9 4 8 3 7 
5 9 4 8 3 7 2 6 1 
3 7 2 6 1 5 9 4 8 
6 1 5 9 4 8 3 7 2 
9 4 8 3 7 2 6 1 5 

となって、ビデオの解が唯一解であることも判明しました。

2020-08-24

Rust-jp slackでの近隣を辿るイテレータというアイデアがよさそうだったので乗り換えました。

    let mut rules = Vec::new();
    for i in 1..=RANGE {
        for j in 1..=RANGE {
            let p = Pos::at(i, j);
-            for m in moves.iter() {
-                if let Some(t) = (p + *m).valid() {
-                    for d in 1..=RANGE as usize {
-                        rules.push(p.state(d, true).requires(t.state(d, false)));
-                    }
+            for q in p.neighbors(&moves) {
+                for d in 1..=RANGE as usize {
+                    rules.push(p.state(d, true).requires(q.state(d, false)));
                 }
             }
        }
    }