Solve Sudoku variants with SAT solvers

Sudoku 400x400

under consruction

• https://github.com/hkociemba/sudokuNxM/tree/master/sudokus
• http://forum.enjoysudoku.com/giant-sudoku-s-16x16-25x25-36x36-100x100-t6578-150.html#p269691

Sudoku 144x144

Solved.

git clone https://github.com/shnarazk/sudoku_sat.git
cd sudoku_sat
cargo run --bin sudoku144 --release < sudoku144.txt

• Rust製のSATソルバーで144x144のSudokuを解こう(my blog entry in Japanese)
• #4 (comment)

Sudoku 100x100

• #4
• Reducing the space

Sudoku 64

Solved.

git clone https://github.com/shnarazk/sudoku_sat.git
cd sudoku_sat
cargo run --bin sudoku64 --release

• Rust製のSATソルバーで64x64のSudokuが解けるだろうか(my blog entry in Japanese)

Sudoku 25

Solved.

• Rust製の「SATソルバーで25x25のナンプレが解けるだろうか」(my blog entry in Japanese)

git clone https://github.com/shnarazk/sudoku_sat.git
cd sudoku_sat
cargo run --bin sudoku25 --release

Miracle Sudoku

Solved.

• https://www.youtube.com/watch?v=cvEq_XkQg8U

Approach

1. Preparation

struct Pos { i: isize, j: isize };
struct Cell { pos: Pos, digit: usize, on: bool };

2. Generate Sudoku rules and extra rules

for i in 1..=RANGE {
    for j in 1..=RANGE {
        let p = Pos::at(i, j);
        for target_i in i..=RANGE {
            for target_j in j..=RANGE {
                 let t = Pos::at(target_i, target_j);
                 for d in 1..=RANGE {
                     rules.push(p.state(d, true).requires(t.state(d, false));
                 }
            }
        }
     }
}

3. Convert the rules to a CNF

4. Run SAT solver

Result, the only one result

$ cargo run --release
    Finished release [optimized] target(s) in 0.00s
     Running `target/release/miracle_sudoku`
#rules: 22248
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 

$ 

Stats

$ tokei
-------------------------------------------------------------------------------
 Language            Files        Lines         Code     Comments       Blanks
-------------------------------------------------------------------------------
 Markdown                1           56           56            0            0
 Rust                    5          281          239           30           12
 TOML                    1           11            7            1            3
-------------------------------------------------------------------------------
 Total                   7          348          302           31           15
-------------------------------------------------------------------------------