Minimum fill-in

AbbreviationInstances of MINIMUM FILL-IN#✓fully proved

An instance of MINIMUM FILL-IN is a triple \((n, E, K)\) consisting of a natural number \(n\) (the number of vertices), a list \(E\) of pairs of natural numbers (the edge list) and a natural number \(K\) (the bound).

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

Used by 4

Used byGraph augmented by added edges · The MINIMUM FILL-IN (CHORDAL COMPLETION) problem · Feasible MINIMUM FILL-IN instances · Well-formed MINIMUM FILL-IN instances

DefinitionGraph augmented by added edges#✓fully proved

For an instance \((n, E, K)\) of MINIMUM FILL-IN and a list \(A\) of pairs of natural numbers, the augmented graph is the graph of the edge list \(E\) followed by \(A\) on \(n\) vertices: the simple graph on \(\{0, \dots, n - 1\}\) in which distinct vertices \(i\) and \(j\) are adjacent when \((i, j)\) or \((j, i)\) belongs to \(E\) or to \(A\).

def GraphAug (i : MinimumFillInInstance) (added : List (ℕ × ℕ)) : SimpleGraph (Fin i.1) :=
  Cslib.Complexity.Karp.edgeGraph i.1 (i.2.1 ++ added)

Uses 2 · Used by 1

Statement usesGraph of an edge list · Instances of MINIMUM FILL-IN

Used byFeasible MINIMUM FILL-IN instances

DefinitionWell-formed MINIMUM FILL-IN instances#✓fully proved

An instance \((n, E, K)\) of MINIMUM FILL-IN is well formed when the list \(E\) has no repeated entries and every pair \((u, v)\) in \(E\) satisfies \(u < n\), \(v < n\) and \(u \ne v\), and its reverse \((v, u)\) does not belong to \(E\).

def WellFormed (i : MinimumFillInInstance) : 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 usesInstances of MINIMUM FILL-IN

Used byThe MINIMUM FILL-IN (CHORDAL COMPLETION) problem

DefinitionFeasible MINIMUM FILL-IN instances#✓fully proved

An instance \((n, E, K)\) of MINIMUM FILL-IN is feasible when there are an ordering \(\sigma\) of the vertices \(0, \dots, n - 1\) (a list that contains each of them exactly once) and a list \(A\) of pairs of natural numbers, with no repeated entries and at most \(K\) entries, such that every pair \((u, v)\) in \(A\) satisfies \(u < n\), \(v < n\) and \(u \ne v\), neither \((u, v)\) nor \((v, u)\) belongs to \(E\), and \((v, u)\) does not belong to \(A\), and such that, in the graph augmented by \(A\), any two distinct vertices \(a\) and \(b\) that are both adjacent to a vertex \(v\) and both come after \(v\) in \(\sigma\) are adjacent to each other.

The ordering \(\sigma\) is thus a perfect elimination ordering of the augmented graph, so adding the at most \(K\) edges of \(A\) to the graph makes it chordal.

def MinimumFillInFeasible
    (i : MinimumFillInInstance) : Prop :=
  ∃ ord : List (Fin i.1), ord.Perm (List.finRange i.1) ∧
    ∃ added : List (ℕ × ℕ), added.Nodup ∧ added.length ≤ i.2.2 ∧
      (∀ e ∈ added, e.1 < i.1 ∧ e.2 < i.1 ∧ e.1 ≠ e.2 ∧ (e.2, e.1) ∉ added ∧
        (e.2, e.1) ∉ i.2.1 ∧ e ∉ i.2.1) ∧
      ∀ v a b : Fin i.1, a ≠ b → ord.idxOf v < ord.idxOf a →
        ord.idxOf v < ord.idxOf b → (GraphAug i added).Adj v a →
        (GraphAug i added).Adj v b → (GraphAug i added).Adj a b

Uses 2 · Used by 1

Statement usesGraph augmented by added edges · Instances of MINIMUM FILL-IN

Used byThe MINIMUM FILL-IN (CHORDAL COMPLETION) problem

DefinitionThe MINIMUM FILL-IN (CHORDAL COMPLETION) problem#✓fully proved

The decision problem MINIMUM FILL-IN accepts a bitstring \(x\) exactly when \(x\) decodes, under the canonical bitstring encoding, to an instance \((n, E, K)\) of MINIMUM FILL-IN that is well formed and feasible.

noncomputable def minimumFillInDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := MinimumFillInInstance) x with
  | some i => decide (WellFormed i ∧ MinimumFillInFeasible 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 MINIMUM FILL-IN instances · Instances of MINIMUM FILL-IN · Well-formed MINIMUM FILL-IN instances · Decision problems

Used byMINIMUM FILL-IN (CHORDAL COMPLETION) is NP-complete

TheoremMINIMUM FILL-IN (CHORDAL COMPLETION) is NP-complete#●ready to prove

The decision problem MINIMUM FILL-IN lies in NP, and every decision problem in NP has a polynomial-time many-one reduction to MINIMUM FILL-IN.

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

Sources

• M. R. Garey and D. S. Johnson, Computers and Intractability (1979), MINIMUM FILL-IN; M. Yannakakis, "Computing the minimum fill-in is NP-complete" (1981).

Uses 5

Statement usesPolynomial-time many-one reduction · The MINIMUM FILL-IN (CHORDAL COMPLETION) problem · Complexity classes · Decision problems · The complexity class NP

5 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.