Exact cover by 3-sets

AbbreviationInstances of EXACT COVER BY 3-SETS#✓fully proved

An instance of EXACT COVER BY 3-SETS is a pair \((q, C)\) of a natural number \(q\) and a finite list \(C\) of finite lists of natural numbers. The intended universe is \(\{0, \dots, 3q - 1\}\) and the entries of \(C\) are the candidate three-element subsets; that each entry lists three distinct elements of the universe is required by well-formedness, not by the type of instances.

abbrev ExactCoverBy3SetsInstance := ℕ × List (List ℕ)

Used by 3

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

DefinitionWell-formed EXACT COVER BY 3-SETS instances#✓fully proved

An instance \((q, C)\) of EXACT COVER BY 3-SETS is well formed when every entry of \(C\) is a list of exactly three pairwise distinct natural numbers, each less than \(3q\).

def WellFormed (i : ExactCoverBy3SetsInstance) : Prop :=
  ∀ s ∈ i.2, s.length = 3 ∧ s.Nodup ∧ ∀ x ∈ s, x < 3 * i.1

Uses 1 · Used by 1

Statement usesInstances of EXACT COVER BY 3-SETS

Used byEXACT COVER BY 3-SETS as a decision problem

DefinitionFeasible EXACT COVER BY 3-SETS instances#✓fully proved

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

def ExactCoverBy3SetsFeasible
    (i : ExactCoverBy3SetsInstance) : Prop :=
  ∃ sub : List (List ℕ), sub.Sublist i.2 ∧
    ∀ x < 3 * i.1, ∃! s ∈ sub, x ∈ s

Uses 1 · Used by 1

Statement usesInstances of EXACT COVER BY 3-SETS

Used byEXACT COVER BY 3-SETS as a decision problem

DefinitionEXACT COVER BY 3-SETS as a decision problem#✓fully proved

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

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

Used byEXACT COVER BY 3-SETS is NP-complete

TheoremEXACT COVER BY 3-SETS is NP-complete#●ready to prove

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

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

Sources

• M. R. Garey and D. S. Johnson, Computers and Intractability (1979), EXACT COVER BY 3-SETS.

Uses 5

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