Sudoku

This tutorial will demonstrate how to solve a Sudoku puzzle by encoding its rules into propositional logic, which is a good example of a non-trivial logic problem.

Setup

julia> using PAndQ, PrettyTables

Creating a Grid

Sudoku is traditionally played on a 9x9 grid.

julia> lines = collect(0:3:9);
julia> grid = zeros(Int, 9, 9);
julia> print_grid(grid) = pretty_table(
           map(cell -> cell == 0 ? "⋅" : string(cell), grid);
           vlines = lines, hlines = lines, show_header = false
       );
julia> print_grid(grid)┌─────────┬─────────┬─────────┐
│ ⋅  ⋅  ⋅ │ ⋅  ⋅  ⋅ │ ⋅  ⋅  ⋅ │
│ ⋅  ⋅  ⋅ │ ⋅  ⋅  ⋅ │ ⋅  ⋅  ⋅ │
│ ⋅  ⋅  ⋅ │ ⋅  ⋅  ⋅ │ ⋅  ⋅  ⋅ │
├─────────┼─────────┼─────────┤
│ ⋅  ⋅  ⋅ │ ⋅  ⋅  ⋅ │ ⋅  ⋅  ⋅ │
│ ⋅  ⋅  ⋅ │ ⋅  ⋅  ⋅ │ ⋅  ⋅  ⋅ │
│ ⋅  ⋅  ⋅ │ ⋅  ⋅  ⋅ │ ⋅  ⋅  ⋅ │
├─────────┼─────────┼─────────┤
│ ⋅  ⋅  ⋅ │ ⋅  ⋅  ⋅ │ ⋅  ⋅  ⋅ │
│ ⋅  ⋅  ⋅ │ ⋅  ⋅  ⋅ │ ⋅  ⋅  ⋅ │
│ ⋅  ⋅  ⋅ │ ⋅  ⋅  ⋅ │ ⋅  ⋅  ⋅ │
└─────────┴─────────┴─────────┘

The grid is currently empty. Placing random numbers in some of the cells has a very high probability of generating an unsolvable board. Knowing which numbers to place in each cell requires the same functionality that it takes to solve the board in the first place. Encoding the rules of Sudoku into a proposition means that any solution to that proposition can be decoded into a solution of Sudoku.

Given the predicate p(row, column, number) is true when the given row and column of the grid contains the given number:

julia> p(row, column, number) = @atomize $((row, column) => number);

1. Each row contains each number from 1 to 9. This proposition can be read as "for each row and for each number, one of the cells in that row contains that number".

\[\bigwedge\limits_{i = 1}^9 \bigwedge\limits_{n = 1}^9 \bigvee\limits_{j = 1}^9 P(i, j, n) \\\]

julia> one = fold((∧) => 1:9, (∧) => 1:9, (∨) => 1:9) do i, n, j
           p(i, j, n)
       end;

2. Each column contains each number from 1 to 9. This proposition can be read as "for each column and for each number, one of the cells in that column contains that number".

\[\bigwedge\limits_{j = 1}^9 \bigwedge\limits_{n = 1}^9 \bigvee\limits_{i = 1}^9 P(i, j, n) \\\]

julia> two = fold((∧) => 1:9, (∧) => 1:9, (∨) => 1:9) do j, n, i
           p(i, j, n)
       end;

3. Each 3x3 subgrid contains each number from 1 to 9. This proposition can be read as "for each 3x3 subgrid and for each number, one of the cells in that subgrid contains that number".

\[\bigwedge\limits_{r = 0}^2 \bigwedge\limits_{c = 0}^2 \bigwedge\limits_{n = 1}^9 \bigvee\limits_{i = 1}^3 \bigvee\limits_{j = 1}^3 P(3r + i, 3c + j, n) \\\]

julia> three = fold(
           (∧) => 0:2, (∧) => 0:2, (∧) => 1:9, (∨) => 1:3, (∨) => 1:3
       ) do r, c, n, i, j
           p(3r + i, 3c + j, n)
       end;

4. Each cell contains a single number. This proposition can be read as "for each cell and for each pair of unique numbers, that cell does not contain both numbers".

\[\bigwedge\limits_{i = 1}^9 \bigwedge\limits_{j = 1}^9 \bigwedge\limits_{n = 1}^8 \bigwedge\limits_{m = n + 1}^9 ¬P(i, j, n) ∨ ¬P(i, j, m)\]

julia> four = fold((∧) => 1:9, (∧) => 1:9, (∧) => 1:8) do i, j, n
           fold((∧) => n + 1:9) do m
               ¬p(i, j, n) ∨ ¬p(i, j, m)
           end
       end;

The conjunction of these rules represent the encoding.

julia> rules = ⋀((one, two, three, four));

Note

See also @atomize, fold, conjunction, and, and or.

Finding a Solution

Given a proposition, valuations that result in a true interpretation can be found using the solutions function. Since the encoding does not specify any initial values of the cells, there will be many possible solutions to the proposition. Each solution contains 729 assignments of a constant to a Bool, which makes sense because the 9x9 grid has 81 cells and each cell contains one of 9 possible numbers.

julia> first_solution(p) = collect(first(solutions(p)));
julia> solution = first_solution(rules)729-element Vector{Pair{PAndQ.Constant, Bool}}:
 PAndQ.Constant((1, 9) => 1) => 1
 PAndQ.Constant((1, 8) => 1) => 0
 PAndQ.Constant((1, 7) => 1) => 0
 PAndQ.Constant((1, 6) => 1) => 0
 PAndQ.Constant((1, 5) => 1) => 0
 PAndQ.Constant((1, 4) => 1) => 0
 PAndQ.Constant((1, 3) => 1) => 0
 PAndQ.Constant((1, 2) => 1) => 0
 PAndQ.Constant((1, 1) => 1) => 0
 PAndQ.Constant((1, 9) => 2) => 0
                             ⋮
 PAndQ.Constant((9, 9) => 9) => 0
 PAndQ.Constant((9, 8) => 9) => 0
 PAndQ.Constant((9, 7) => 9) => 0
 PAndQ.Constant((9, 6) => 9) => 0
 PAndQ.Constant((9, 5) => 9) => 0
 PAndQ.Constant((9, 4) => 9) => 0
 PAndQ.Constant((9, 3) => 9) => 0
 PAndQ.Constant((9, 2) => 9) => 0
 PAndQ.Constant((9, 1) => 9) => 1

The assignments from a constant to true correspond to cells that contain the given numbers. There are 81 such constants, with each value corresponding to a cell in the grid.

julia> extract(solution) = map(something ∘ value ∘ first, filter(last, solution));
julia> cells = extract(solution)81-element Vector{Pair{Tuple{Int64, Int64}, Int64}}:
 (1, 9) => 1
 (1, 3) => 2
 (1, 7) => 3
 (1, 2) => 4
 (1, 8) => 5
 (1, 1) => 6
 (1, 5) => 7
 (1, 4) => 8
 (1, 6) => 9
 (2, 2) => 1
        ⋮
 (9, 8) => 1
 (9, 9) => 2
 (9, 6) => 3
 (9, 5) => 4
 (9, 4) => 5
 (9, 3) => 6
 (9, 7) => 7
 (9, 2) => 8
 (9, 1) => 9

Each cell is a Pair in the form (row, column) => number, which maps from the row and column of the grid to its corresponding number.

julia> function decode!(grid, cells)
           for ((row, column), value) in cells
               grid[row, column] = value
           end
       
           grid
       end;
julia> print_grid(decode!(grid, cells))┌─────────┬─────────┬─────────┐
│ 6  4  2 │ 8  7  9 │ 3  5  1 │
│ 5  1  8 │ 4  3  2 │ 9  7  6 │
│ 7  9  3 │ 1  6  5 │ 2  4  8 │
├─────────┼─────────┼─────────┤
│ 4  2  9 │ 3  5  8 │ 1  6  7 │
│ 1  3  5 │ 7  2  6 │ 4  8  9 │
│ 8  6  7 │ 9  1  4 │ 5  2  3 │
├─────────┼─────────┼─────────┤
│ 2  5  1 │ 6  9  7 │ 8  3  4 │
│ 3  7  4 │ 2  8  1 │ 6  9  5 │
│ 9  8  6 │ 5  4  3 │ 7  1  2 │
└─────────┴─────────┴─────────┘

Creating a Puzzle

Now that a solution has been found, it can be used to create a puzzle by removing some of the known values.

julia> print_grid(grid .*= rand(Bool, 9, 9))┌─────────┬─────────┬─────────┐
│ ⋅  4  ⋅ │ 8  7  ⋅ │ ⋅  ⋅  1 │
│ ⋅  ⋅  8 │ ⋅  ⋅  2 │ ⋅  ⋅  ⋅ │
│ ⋅  ⋅  3 │ ⋅  ⋅  ⋅ │ ⋅  4  ⋅ │
├─────────┼─────────┼─────────┤
│ 4  2  ⋅ │ 3  ⋅  8 │ 1  6  ⋅ │
│ 1  3  ⋅ │ ⋅  ⋅  6 │ ⋅  ⋅  ⋅ │
│ ⋅  6  ⋅ │ ⋅  1  ⋅ │ ⋅  2  3 │
├─────────┼─────────┼─────────┤
│ ⋅  ⋅  1 │ 6  9  ⋅ │ 8  ⋅  ⋅ │
│ 3  ⋅  ⋅ │ 2  ⋅  ⋅ │ 6  9  ⋅ │
│ 9  8  6 │ ⋅  4  ⋅ │ ⋅  1  2 │
└─────────┴─────────┴─────────┘

Since the rules represent an empty Sudoku grid, finding a solution to this puzzle means encoding the initial values as additional rules and finding a solution to the combined ruleset. If a grid has no solutions, then it contains a contradiction to the rules.

julia> print_grid(decode!(grid, extract(first_solution(rules ∧ ⋀(map(
           i -> p(i.I..., grid[i]), filter(i -> grid[i] != 0, CartesianIndices(grid))))))))┌─────────┬─────────┬─────────┐
│ 6  4  2 │ 8  7  9 │ 3  5  1 │
│ 5  1  8 │ 4  3  2 │ 9  7  6 │
│ 7  9  3 │ 1  6  5 │ 2  4  8 │
├─────────┼─────────┼─────────┤
│ 4  2  9 │ 3  5  8 │ 1  6  7 │
│ 1  3  5 │ 7  2  6 │ 4  8  9 │
│ 8  6  7 │ 9  1  4 │ 5  2  3 │
├─────────┼─────────┼─────────┤
│ 2  5  1 │ 6  9  7 │ 8  3  4 │
│ 3  7  4 │ 2  8  1 │ 6  9  5 │
│ 9  8  6 │ 5  4  3 │ 7  1  2 │
└─────────┴─────────┴─────────┘

Sudoku

Setup

Creating a Grid

Encoding the Rules

Finding a Solution

Creating a Puzzle