Exact cover

AbbreviationInstances of EXACT COVER#✓fully proved

An instance of EXACT COVER is a pair \((n, C)\) of a natural number \(n\), the size of the universe \(\{0, \dots, n - 1\}\), and a finite list \(C\) of finite lists of natural numbers, the candidate subsets. That each entry of \(C\) lists distinct elements of the universe is required by well-formedness, not by the type of instances.

abbrev ExactCoverInstance := ℕ × List (List ℕ)

Used by 3

Used byEXACT COVER as a decision problem · Feasible EXACT COVER instances · Well-formed EXACT COVER instances

DefinitionWell-formed EXACT COVER instances#✓fully proved

An instance \((n, C)\) of EXACT COVER is well formed when every entry of \(C\) is a list of pairwise distinct natural numbers, each less than \(n\).

def WellFormed (i : ExactCoverInstance) : Prop :=
  ∀ s ∈ i.2, s.Nodup ∧ ∀ x ∈ s, x < i.1

Uses 1 · Used by 1

Statement usesInstances of EXACT COVER

Used byEXACT COVER as a decision problem

DefinitionFeasible EXACT COVER instances#✓fully proved

An instance \((n, C)\) of EXACT COVER is feasible when \(C\) has a sublist \(S\), obtained by deleting some entries of \(C\), such that for every natural number \(x < n\) there is exactly one list that occurs in \(S\) and contains \(x\).

def ExactCoverFeasible
    (i : ExactCoverInstance) : Prop :=
  ∃ sub : List (List ℕ), sub.Sublist i.2 ∧
    ∀ x < i.1, ∃! s ∈ sub, x ∈ s

Uses 1 · Used by 1

Statement usesInstances of EXACT COVER

Used byEXACT COVER as a decision problem

DefinitionEXACT COVER as a decision problem#✓fully proved

The decision problem EXACT COVER 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 of EXACT COVER that is well formed and feasible; bitstrings that do not decode are rejected.

noncomputable def exactCoverDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := ExactCoverInstance) x with
  | some i => decide (WellFormed i ∧ ExactCoverFeasible 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 EXACT COVER instances · Instances of EXACT COVER · Well-formed EXACT COVER instances · Decision problems

Used byEXACT COVER is NP-complete

TheoremEXACT COVER is NP-complete#●ready to prove

The decision problem EXACT COVER is in NP, and every decision problem in NP has a polynomial-time many-one reduction to it.

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

Sources

• M. R. Garey and D. S. Johnson, Computers and Intractability (1979), EXACT COVER; R. M. Karp, "Reducibility among combinatorial problems" (1972).

Uses 5

Statement usesPolynomial-time many-one reduction · EXACT COVER 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.