Latin square completion

AbbreviationLatin square completion instances#✓fully proved

An instance of LATIN SQUARE COMPLETION is a pair \((n, G)\) of a natural number \(n\), the intended size, and a list \(G\) of lists of natural numbers, read as the rows of a partial grid in which the entry \(0\) marks a blank cell.

abbrev LatinSquareCompletionInstance := ℕ × List (List ℕ)

Used by 3

Used byLATIN SQUARE COMPLETION as a decision problem · Completable partial Latin squares · Well-formed Latin square completion instances

DefinitionWell-formed Latin square completion instances#✓fully proved

An instance \((n, G)\) of LATIN SQUARE COMPLETION is well formed when \(n > 0\), \(G\) has exactly \(n\) rows, every row of \(G\) has length \(n\), and every entry of \(G\) is at most \(n\).

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

Uses 1 · Used by 1

Statement usesLatin square completion instances

Used byLATIN SQUARE COMPLETION as a decision problem

DefinitionCompletable partial Latin squares#✓fully proved

An instance \((n, G)\) of LATIN SQUARE COMPLETION is feasible when there is a grid \(C\) consisting of \(n\) rows of length \(n\) such that for all \(r, c < n\) the entry \(G_{rc}\) is either \(0\) or equal to \(C_{rc}\), every row of \(C\) is a permutation of \(1, \dots, n\), and every column of \(C\) is a permutation of \(1, \dots, n\). Here \(G_{rc}\) is taken to be \(0\) when \(G\) has no entry in row \(r\) and column \(c\).

def LatinSquareCompletionFeasible
    (i : LatinSquareCompletionInstance) : Prop :=
  ∃ completion : List (List ℕ), completion.length = i.1 ∧
    (∀ row ∈ completion, row.length = i.1) ∧
    (∀ r < i.1, ∀ c < 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, (completion.getD r []).Perm ((List.range i.1).map (· + 1))) ∧
    ∀ c < i.1, ((List.range i.1).map
      (fun r => (completion.getD r []).getD c 0)).Perm ((List.range i.1).map (· + 1))

Uses 1 · Used by 1

Statement usesLatin square completion instances

Used byLATIN SQUARE COMPLETION as a decision problem

DefinitionLATIN SQUARE COMPLETION as a decision problem#✓fully proved

The decision problem LATIN SQUARE COMPLETION accepts a bitstring \(x\) exactly when \(x\) decodes, under the canonical bitstring encoding of pairs of a natural number and a list of lists of natural numbers, to an instance \((n, G)\) that is well formed (\(n > 0\) and \(G\) consists of \(n\) rows of length \(n\) with entries at most \(n\)) and feasible (\(G\) can be completed to an \(n \times n\) grid whose rows and columns are permutations of \(1, \dots, n\) and which agrees with \(G\) on its nonzero entries). Bitstrings that do not decode, or that decode to a malformed instance, are rejected.

noncomputable def latinSquareCompletionDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := LatinSquareCompletionInstance) x with
  | some i => decide (WellFormed i ∧ LatinSquareCompletionFeasible 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 · Completable partial Latin squares · Latin square completion instances · Well-formed Latin square completion instances · Decision problems

Used byLATIN SQUARE COMPLETION is NP-complete

TheoremLATIN SQUARE COMPLETION is NP-complete#●ready to prove

The decision problem LATIN SQUARE COMPLETION on bitstrings lies in NP, and every decision problem in NP reduces to it by a polynomial-time many-one reduction.

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

Sources

• C. J. Colbourn, "The complexity of completing partial Latin squares" (1984).

Uses 5

Statement usesPolynomial-time many-one reduction · LATIN SQUARE COMPLETION 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.