Maximum induced matching

AbbreviationMaximum-induced-matching instances#✓fully proved

A maximum-induced-matching instance is a triple \((n, E, K)\) of a natural number \(n\) (the vertex count), a list \(E\) of pairs of natural numbers (the edges) and a natural number \(K\) (the bound).

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

Used by 3

Used byThe MAXIMUM INDUCED MATCHING decision problem · Feasible maximum-induced-matching instances · Well-formed maximum-induced-matching instances

DefinitionWell-formed maximum-induced-matching instances#✓fully proved

A maximum-induced-matching instance \((n, E, K)\) is well formed when the edge list \(E\) has no repeated entries and every pair \((u, v)\) in \(E\) satisfies \(u < n\), \(v < n\) and \(u \ne v\), with the reverse pair \((v, u)\) not in \(E\).

def WellFormed (i : MaximumInducedMatchingInstance) : Prop :=
  i.2.1.Nodup ∧ ∀ e ∈ i.2.1, e.1 < i.1 ∧ e.2 < i.1 ∧ e.1 ≠ e.2 ∧ (e.2, e.1) ∉ i.2.1

Uses 1 · Used by 1

Statement usesMaximum-induced-matching instances

Used byThe MAXIMUM INDUCED MATCHING decision problem

DefinitionFeasible maximum-induced-matching instances#✓fully proved

A maximum-induced-matching instance \((n, E, K)\), with vertex count \(n\), edge list \(E\) of pairs of natural numbers and bound \(K\), is feasible when there is a sublist \(M\) of \(E\) of length at least \(K\) such that any two distinct pairs in \(M\) share no endpoint, and no pair in \(E\) joins an endpoint of one pair in \(M\) to an endpoint of a different pair in \(M\).

def MaximumInducedMatchingFeasible
    (i : MaximumInducedMatchingInstance) : Prop :=
  ∃ M : List (ℕ × ℕ), M.Sublist i.2.1 ∧ i.2.2 ≤ M.length ∧
    (∀ e1 ∈ M, ∀ e2 ∈ M, e1 ≠ e2 →
      e1.1 ≠ e2.1 ∧ e1.1 ≠ e2.2 ∧ e1.2 ≠ e2.1 ∧ e1.2 ≠ e2.2) ∧
    ∀ e ∈ i.2.1, ∀ e1 ∈ M, ∀ e2 ∈ M, e1 ≠ e2 →
      ¬ ((e.1 = e1.1 ∨ e.1 = e1.2) ∧ (e.2 = e2.1 ∨ e.2 = e2.2) ∨
        (e.2 = e1.1 ∨ e.2 = e1.2) ∧ (e.1 = e2.1 ∨ e.1 = e2.2))

Uses 1 · Used by 1

Statement usesMaximum-induced-matching instances

Used byThe MAXIMUM INDUCED MATCHING decision problem

DefinitionThe MAXIMUM INDUCED MATCHING decision problem#✓fully proved

MAXIMUM INDUCED MATCHING is the decision problem that accepts a bitstring \(x\) exactly when \(x\) decodes, under the canonical bitstring encoding, to a maximum-induced-matching instance \((n, E, K)\) that is well formed and feasible: the edge list \(E\) has no repeated entries, every pair \((u, v)\) in \(E\) satisfies \(u < n\), \(v < n\) and \(u \ne v\) with \((v, u)\) not in \(E\), and some sublist \(M\) of \(E\) of length at least \(K\) is an induced matching, meaning that any two distinct pairs in \(M\) share no endpoint and no pair in \(E\) joins an endpoint of one pair in \(M\) to an endpoint of a different pair in \(M\). Bitstrings that do not decode are rejected.

noncomputable def maximumInducedMatchingDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := MaximumInducedMatchingInstance) x with
  | some i => decide (WellFormed i ∧ MaximumInducedMatchingFeasible 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 maximum-induced-matching instances · Maximum-induced-matching instances · Well-formed maximum-induced-matching instances · Decision problems

Used byMAXIMUM INDUCED MATCHING is NP-complete

TheoremMAXIMUM INDUCED MATCHING is NP-complete#●ready to prove

The MAXIMUM INDUCED MATCHING decision problem belongs to NP, and every decision problem in NP reduces to it by a polynomial-time many-one reduction.

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

Sources

• L. J. Stockmeyer and V. V. Vazirani, "NP-completeness of some generalizations of the maximum matching problem", Information Processing Letters 15 (1982), 14-19; K. Cameron, "Induced matchings", Discrete Applied Mathematics 24 (1989), 97-102 (NP-completeness for bipartite graphs, polynomial for chordal graphs).

Uses 5

Statement usesPolynomial-time many-one reduction · The MAXIMUM INDUCED MATCHING 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.