Sudoku

AbbreviationSudoku instances#✓fully proved

A Sudoku instance is a pair \((n, G)\) of a natural number \(n\), the block size, and a grid \(G\) given as a finite list of rows, each row a finite list of natural numbers; an entry \(0\) stands for a blank cell.

abbrev SudokuInstance := ℕ × List (List ℕ)

Used by 3

Used bySUDOKU as a decision problem · Feasible Sudoku instances · Well-formed Sudoku instances

DefinitionWell-formed Sudoku instances#✓fully proved

A Sudoku instance \((n, G)\), with block size \(n\) and grid \(G\) a list of rows of natural numbers, is well formed when \(n > 0\), \(G\) has exactly \(n^2\) rows, every row of \(G\) has exactly \(n^2\) entries, and every entry of \(G\) is at most \(n^2\).

def WellFormed (i : SudokuInstance) : Prop :=
  0 < i.1 ∧ i.2.length = i.1 * i.1 ∧ (∀ row ∈ i.2, row.length = i.1 * i.1) ∧
    ∀ row ∈ i.2, ∀ x ∈ row, x ≤ i.1 * i.1

Uses 1 · Used by 1

Statement usesSudoku instances

Used bySUDOKU as a decision problem

DefinitionFeasible Sudoku instances#✓fully proved

A Sudoku instance \((n, G)\), with block size \(n\) and grid \(G\) a list of rows of natural numbers, is feasible when there is a grid \(C\) of natural numbers with exactly \(n^2\) rows, each of exactly \(n^2\) entries, such that, indexing rows and columns from \(0\): for all \(r, c < n^2\) the entry \(G_{rc}\) is \(0\) or equals \(C_{rc}\), where an entry missing from \(G\) counts as \(0\); every row of \(C\) and every column of \(C\) lists each of \(1, \dots, n^2\) exactly once; and for all \(b, b' < n\) the \(n^2\) entries \(C_{bn + i,\, b'n + j}\) with \(i, j < n\) list each of \(1, \dots, n^2\) exactly once.

MetaMathlibExt.Complexity.NPComplete.Sudoku.SudokuFeasible · 16 lines

def SudokuFeasible
    (i : SudokuInstance) : Prop :=
  ∃ completion : List (List ℕ), completion.length = i.1 * i.1 ∧
    (∀ row ∈ completion, row.length = i.1 * i.1) ∧
    (∀ r < i.1 * i.1, ∀ c < i.1 * i.1, (i.2.getD r []).getD c 0 = 0 ∨
      (i.2.getD r []).getD c 0 = (completion.getD r []).getD c 0) ∧
    (∀ r < i.1 * i.1,
      (completion.getD r []).Perm ((List.range (i.1 * i.1)).map (· + 1))) ∧
    (∀ c < i.1 * i.1,
      ((List.range (i.1 * i.1)).map
        (fun r => (completion.getD r []).getD c 0)).Perm
        ((List.range (i.1 * i.1)).map (· + 1))) ∧
    ∀ br < i.1, ∀ bc < i.1,
      ((List.range (i.1 * i.1)).map (fun t =>
        (completion.getD (br * i.1 + t / i.1) []).getD (bc * i.1 + t % i.1) 0)).Perm
        ((List.range (i.1 * i.1)).map (· + 1))

Uses 1 · Used by 1

Statement usesSudoku instances

Used bySUDOKU as a decision problem

DefinitionSUDOKU as a decision problem#✓fully proved

The decision problem SUDOKU accepts a bitstring \(x\) exactly when \(x\) decodes, under the canonical bitstring encoding of pairs of a natural number and a finite list of finite lists of natural numbers, to a Sudoku instance that is well formed and feasible. It rejects every bitstring that does not decode to an instance.

noncomputable def sudokuDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := SudokuInstance) x with
  | some i => decide (WellFormed i ∧ SudokuFeasible i)
  | none => false

Uses 12 · Used by 1

Statement usesBitstring encodings · Decoding function of a bitstring encoding · Decoding inverts bitstring encoding · Encoding function of a bitstring encoding · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Parsing a list of booleans into self-delimiting blocks · Bounded parsing of self-delimiting blocks · Feasible Sudoku instances · Sudoku instances · Well-formed Sudoku instances · Decision problems

Used bySUDOKU is NP-complete

TheoremSUDOKU is NP-complete#●ready to prove

The decision problem SUDOKU lies in NP, and every decision problem in NP has a polynomial-time many-one reduction to SUDOKU.

public theorem_wanted sudoku_npComplete :
    sudokuDec ∈ MetaMathlibExt.ComplexityTheory.NP ∧
      ∀ L : MetaMathlibExt.ComplexityTheory.DecisionProblem,
        L ∈ MetaMathlibExt.ComplexityTheory.NP →
          Cslib.CookLevin.PolyManyOneRed L sudokuDec

Sources

• T. Yato and T. Seta, "Complexity and completeness of finding another solution and its application to puzzles" (2003).

Uses 5

Statement usesPolynomial-time many-one reduction · SUDOKU as a decision problem · Complexity classes · Decision problems · The complexity class NP

4 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.