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)
┌─────────┬─────────┬─────────┐ │ ⋅ ⋅ ⋅ │ ⋅ ⋅ ⋅ │ ⋅ ⋅ ⋅ │ │ ⋅ ⋅ ⋅ │ ⋅ ⋅ ⋅ │ ⋅ ⋅ ⋅ │ │ ⋅ ⋅ ⋅ │ ⋅ ⋅ ⋅ │ ⋅ ⋅ ⋅ │ ├─────────┼─────────┼─────────┤ │ ⋅ ⋅ ⋅ │ ⋅ ⋅ ⋅ │ ⋅ ⋅ ⋅ │ │ ⋅ ⋅ ⋅ │ ⋅ ⋅ ⋅ │ ⋅ ⋅ ⋅ │ │ ⋅ ⋅ ⋅ │ ⋅ ⋅ ⋅ │ ⋅ ⋅ ⋅ │ ├─────────┼─────────┼─────────┤ │ ⋅ ⋅ ⋅ │ ⋅ ⋅ ⋅ │ ⋅ ⋅ ⋅ │ │ ⋅ ⋅ ⋅ │ ⋅ ⋅ ⋅ │ ⋅ ⋅ ⋅ │ │ ⋅ ⋅ ⋅ │ ⋅ ⋅ ⋅ │ ⋅ ⋅ ⋅ │ └─────────┴─────────┴─────────┘
Encoding the Rules
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);
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{PAndQ.AbstractSyntaxTree}: $((9, 9)=>9) $((9, 9)=>8) $((9, 9)=>7) $((9, 9)=>6) $((9, 9)=>5) $((9, 9)=>4) $((9, 9)=>3) $((9, 9)=>2) $((9, 9)=>1) $((9, 8)=>9) ⋮ $((1, 1)=>9) $((1, 1)=>8) $((1, 1)=>7) $((1, 1)=>6) $((1, 1)=>5) $((1, 1)=>4) $((1, 1)=>3) $((1, 1)=>2) $((1, 1)=>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)
ERROR: MethodError: no method matching lastindex(::PAndQ.AbstractSyntaxTree) Closest candidates are: lastindex(::Any, ::Any) @ Base abstractarray.jl:427 lastindex(::Base.JuliaSyntax.SourceFile) @ Base /cache/build/builder-amdci4-0/julialang/julia-release-1-dot-10/base/JuliaSyntax/src/source_files.jl:132 lastindex(::Base64.Buffer) @ Base64 /opt/hostedtoolcache/julia/1.10.4/x64/share/julia/stdlib/v1.10/Base64/src/buffer.jl:19 ...
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), number) in cells grid[row, column] = number end grid end;
julia> print_grid(decode!(grid, cells))
ERROR: UndefVarError: `cells` not defined
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))
┌─────────┬─────────┬─────────┐ │ ⋅ ⋅ ⋅ │ ⋅ ⋅ ⋅ │ ⋅ ⋅ ⋅ │ │ ⋅ ⋅ ⋅ │ ⋅ ⋅ ⋅ │ ⋅ ⋅ ⋅ │ │ ⋅ ⋅ ⋅ │ ⋅ ⋅ ⋅ │ ⋅ ⋅ ⋅ │ ├─────────┼─────────┼─────────┤ │ ⋅ ⋅ ⋅ │ ⋅ ⋅ ⋅ │ ⋅ ⋅ ⋅ │ │ ⋅ ⋅ ⋅ │ ⋅ ⋅ ⋅ │ ⋅ ⋅ ⋅ │ │ ⋅ ⋅ ⋅ │ ⋅ ⋅ ⋅ │ ⋅ ⋅ ⋅ │ ├─────────┼─────────┼─────────┤ │ ⋅ ⋅ ⋅ │ ⋅ ⋅ ⋅ │ ⋅ ⋅ ⋅ │ │ ⋅ ⋅ ⋅ │ ⋅ ⋅ ⋅ │ ⋅ ⋅ ⋅ │ │ ⋅ ⋅ ⋅ │ ⋅ ⋅ ⋅ │ ⋅ ⋅ ⋅ │ └─────────┴─────────┴─────────┘
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))))))))
ERROR: MethodError: Cannot `convert` an object of type Vector{PAndQ.AbstractSyntaxTree} to an object of type PAndQ.AbstractSyntaxTree Closest candidates are: convert(::Type{PAndQ.AbstractSyntaxTree}, ::PAndQ.Interface.Operator) @ PAndQ ~/work/PAndQ.jl/PAndQ.jl/src/semantics.jl:372 convert(::Type{PAndQ.AbstractSyntaxTree}, ::Symbol) @ PAndQ ~/work/PAndQ.jl/PAndQ.jl/src/semantics.jl:373 convert(::Type{PAndQ.AbstractSyntaxTree}, ::Some) @ PAndQ ~/work/PAndQ.jl/PAndQ.jl/src/semantics.jl:374 ...