3-dimensional matching

Abbreviation3-dimensional matching instances#✓fully proved

An instance of 3-DIMENSIONAL MATCHING is a pair \((n, T)\) of a natural number \(n\), the part size, and a finite list \(T\) of triples of natural numbers.

abbrev ThreeDimensionalMatchingInstance := ℕ × List (ℕ × ℕ × ℕ)

Used by 3

Used by3-DIMENSIONAL MATCHING as a decision problem · Feasible 3-dimensional matching instances · Well-formed 3-dimensional matching instances

DefinitionWell-formed 3-dimensional matching instances#✓fully proved

A 3-dimensional matching instance \((n, T)\) is well formed when each of the three coordinates of every triple in \(T\) is less than \(n\).

def WellFormed (i : ThreeDimensionalMatchingInstance) : Prop :=
  ∀ t ∈ i.2, t.1 < i.1 ∧ t.2.1 < i.1 ∧ t.2.2 < i.1

Uses 1 · Used by 1

Statement uses3-dimensional matching instances

Used by3-DIMENSIONAL MATCHING as a decision problem

DefinitionFeasible 3-dimensional matching instances#✓fully proved

A 3-dimensional matching instance \((n, T)\) is feasible, or has a perfect matching, when there is a list \(M\) of length \(n\), obtained from the list of triples \(T\) by deleting some of its entries, such that for each of the three coordinate positions, every natural number \(a < n\) occurs in that position in exactly one triple of \(M\).

def ThreeDimensionalMatchingFeasible
    (i : ThreeDimensionalMatchingInstance) : Prop :=
  ∃ matching : List (ℕ × ℕ × ℕ), matching.Sublist i.2 ∧ matching.length = i.1 ∧
    (∀ a < i.1, ∃! t ∈ matching, t.1 = a) ∧
    (∀ b < i.1, ∃! t ∈ matching, t.2.1 = b) ∧
    ∀ c < i.1, ∃! t ∈ matching, t.2.2 = c

Uses 1 · Used by 1

Statement uses3-dimensional matching instances

Used by3-DIMENSIONAL MATCHING as a decision problem

Definition3-DIMENSIONAL MATCHING as a decision problem#✓fully proved

The decision problem 3-DIMENSIONAL MATCHING accepts a bitstring \(x\) exactly when \(x\) decodes, under the canonical bitstring encoding, to a 3-dimensional matching instance \((n, T)\) that is well formed (every coordinate of every triple in \(T\) is less than \(n\)) and feasible (it has a perfect matching). Bitstrings that do not decode to an instance are rejected.

noncomputable def threeDimensionalMatchingDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := ThreeDimensionalMatchingInstance) x with
  | some i => decide (WellFormed i ∧ ThreeDimensionalMatchingFeasible 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 3-dimensional matching instances · 3-dimensional matching instances · Well-formed 3-dimensional matching instances · Decision problems

Used by3-DIMENSIONAL MATCHING is NP-complete

Theorem3-DIMENSIONAL MATCHING is NP-complete#●ready to prove

The decision problem 3-DIMENSIONAL MATCHING on bitstrings is in NP, and every decision problem in NP reduces to it by a polynomial-time many-one reduction.

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

Sources

• M. R. Garey and D. S. Johnson, Computers and Intractability (1979), 3-DIMENSIONAL MATCHING; R. M. Karp, "Reducibility among combinatorial problems" (1972).

Uses 5

Statement usesPolynomial-time many-one reduction · 3-DIMENSIONAL MATCHING 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.