Matching in general graphs

DefinitionGeneral matching decision problem#✓fully proved

The decision problem that accepts a bitstring \(x\) exactly when \(x\) decodes, under the canonical bitstring encoding, to a triple \((n, E, K)\) of a natural number \(n\), a list \(E\) of pairs of natural numbers and a natural number \(K\) such that every pair \((u, v)\) in \(E\) has \(u < n\), \(v < n\) and \(u \neq v\), and some sublist \(M\) of \(E\) (a subsequence, keeping the order of \(E\)) with no repeated entries and length at least \(K\) has the property that any two different pairs \((u_1, v_1)\) and \((u_2, v_2)\) in \(M\) share no element: \(u_1, v_1 \notin \{u_2, v_2\}\). Bitstrings that do not decode are rejected.

noncomputable def matchingDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := ℕ × List (ℕ × ℕ) × ℕ) x with
  | some i => decide (
      (∀ e ∈ i.2.1, e.1 < i.1 ∧ e.2 < i.1 ∧ e.1 ≠ e.2) ∧
      ∃ matching : List (ℕ × ℕ), matching.Sublist i.2.1 ∧ matching.Nodup ∧
        matching.length ≥ i.2.2 ∧
        ∀ e₁ ∈ matching, ∀ e₂ ∈ matching, e₁ ≠ e₂ →
          e₁.1 ≠ e₂.1 ∧ e₁.1 ≠ e₂.2 ∧ e₁.2 ≠ e₂.1 ∧ e₁.2 ≠ e₂.2)
  | none => false

Uses 9 · 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 · Decision problems

Used byGeneral matching is in P (Edmonds' blossom algorithm)

TheoremGeneral matching is in P (Edmonds' blossom algorithm)#●ready to prove

The general matching decision problem belongs to the complexity class P. This is the problem of deciding, for a vertex count \(n\), a list \(E\) of edges joining distinct vertices below \(n\) and a target \(K\), encoded as a bitstring, whether \(E\) contains at least \(K\) distinct pairwise vertex-disjoint edges.

public theorem_wanted matching_in_p :
    matchingDec ∈ MetaMathlibExt.ComplexityTheory.P

Sources

• J. Edmonds, "Paths, trees, and flowers", Canadian Journal of Mathematics 17 (1965), 449-467.

Uses 4

Statement usesGeneral matching decision problem · Complexity classes · Decision problems · The complexity class P

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.