Perfect graphs

DefinitionPerfect graph#✓fully proved

A finite simple graph \(G\) is perfect if, for every set \(S\) of its vertices, the induced subgraph \(G[S]\) has chromatic number equal to its clique number, the largest size of a clique in \(G[S]\).

def IsPerfect {V : Type*} [Fintype V] (G : SimpleGraph V) : Prop :=
  ∀ (s : Set V), (G.induce s).chromaticNumber = ((G.induce s).cliqueNum : ℕ∞)

Used by 4

Used byLovász's weak perfect graph theorem · Weak perfect graph theorem · The perfect-graph decision problem · Perfect graphs satisfy condition (P)

DefinitionGasparian's condition (P)#✓fully proved

A finite simple graph \(G\) satisfies condition (P) if, for every set \(S\) of its vertices, the induced subgraph \(G[S]\), with independence number \(\alpha(G[S])\) and clique number \(\omega(G[S])\), satisfies \(|S| \le \alpha(G[S]) \cdot \omega(G[S])\).

def PerfIneq {V : Type*} [Fintype V] (G : SimpleGraph V) : Prop :=
  ∀ s : Finset V, s.card ≤ (G.induce (↑s : Set V)).indepNum * (G.induce (↑s : Set V)).cliqueNum

Used by 2

Used byWeak perfect graph theorem · Perfect graphs satisfy condition (P)

TheoremPerfect graphs satisfy condition (P)#✓fully proved

Every finite perfect graph \(G\) satisfies Gasparian's condition (P): for every set \(S\) of its vertices, the induced subgraph \(G[S]\), with independence number \(\alpha(G[S])\) and clique number \(\omega(G[S])\), satisfies \(|S| \le \alpha(G[S]) \cdot \omega(G[S])\).

Indeed, \(G[S]\) has a coloring with \(\omega(G[S])\) colors, and each color class is an independent set, so it has at most \(\alpha(G[S])\) vertices.

theorem perfect_implies_ineq {V : Type*} [Fintype V]
    (G : SimpleGraph V) (hG : IsPerfect G) : PerfIneq G

Uses 2 · Used by 1

Statement usesPerfect graph · Gasparian's condition (P)

Used byWeak perfect graph theorem

TheoremWeak perfect graph theorem#✓fully proved

A finite simple graph \(G\) is perfect if and only if its complement \(\overline{G}\) is perfect.

theorem lovasz_weak_perfect_graph_general
    {V : Type*} [Fintype V]
    (G : SimpleGraph V) : IsPerfect G ↔ IsPerfect Gᶜ

Uses 3 · Used by 1

Statement usesPerfect graph

Proof usesGasparian's condition (P) · Perfect graphs satisfy condition (P)

Used byLovász's weak perfect graph theorem

TheoremLovász's weak perfect graph theorem#✓fully proved

A finite simple graph \(G\) is perfect if and only if its complement \(\overline{G}\) is perfect.

theorem lovasz_weak_perfect_graph
    {V : Type*} [Fintype V] [DecidableEq V]
    (G : SimpleGraph V) : IsPerfect G ↔ IsPerfect Gᶜ

Sources

• L. Lovasz, "Normal hypergraphs and the perfect graph conjecture", Discrete Math. 2 (1972), 253-267, DOI 10.1016/0012-365X(72)90006-4.

Uses 2

Statement usesPerfect graph

Proof usesWeak perfect graph theorem

StructureAdjacency-matrix graph instance#✓fully proved

An instance consists of a natural number \(n\) and a Boolean \(n \times n\) matrix \(A\) with rows and columns indexed by \(\{0, \dots, n-1\}\), read as the adjacency matrix of a graph on the vertices \(0, \dots, n-1\). The matrix is arbitrary; symmetry and the absence of loops are imposed separately by the validity condition.

structure PerfectGraphInstance where
  n : Nat
  adj : Fin n → Fin n → Bool

Sources

• [AIM-COMBINATORICS-0270] Source item 4, notes[269], Section A.4.

Used by 3

Used byThe perfect-graph decision problem · Graph of a valid instance · Valid adjacency-matrix instance

DefinitionValid adjacency-matrix instance#✓fully proved

An instance with \(n\) vertices and adjacency matrix \(A\) is valid when \(A\) is symmetric, that is, \(A_{yx}\) is true whenever \(A_{xy}\) is true, and has no loops, that is, \(A_{xx}\) is false for every vertex \(x\).

def PerfectGraphInstance.Valid (I : PerfectGraphInstance) : Prop :=
  (∀ x y : Fin I.n, I.adj x y = true → I.adj y x = true) ∧
    ∀ x : Fin I.n, I.adj x x = false

Uses 1 · Used by 2

Statement usesAdjacency-matrix graph instance

Used byThe perfect-graph decision problem · Graph of a valid instance

DefinitionGraph of a valid instance#✓fully proved

A valid instance with \(n\) vertices and adjacency matrix \(A\) determines the simple graph on the vertex set \(\{0, \dots, n-1\}\) in which vertices \(x\) and \(y\) are adjacent exactly when \(A_{xy}\) is true.

def PerfectGraphInstance.toSimpleGraph (I : PerfectGraphInstance)
    (h : I.Valid) : SimpleGraph (Fin I.n) where
  Adj x y := I.adj x y = true
  symm := ⟨fun a b hab => h.1 a b hab⟩
  loopless := ⟨fun a ha => by simp [h.2 a] at ha⟩

Uses 2 · Used by 1

Statement usesAdjacency-matrix graph instance · Valid adjacency-matrix instance

Used byThe perfect-graph decision problem

DefinitionThe perfect-graph decision problem#✓fully proved

The decision problem on bitstrings that accepts a bitstring \(x\) exactly when \(x\) decodes, under the bitstring encoding of adjacency-matrix instances, to a valid instance whose graph is perfect. Bitstrings that do not decode to an instance, or decode to an invalid one, are rejected.

noncomputable def perfectGraphProblem :
    MetaMathlibExt.ComplexityTheory.DecisionProblem :=
  fun l => match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := PerfectGraphInstance) l with
    | some I => if h : I.Valid then
        (if MathlibExt.Combinatorics.SimpleGraph.PerfectGraphWanted.IsPerfect
          (I.toSimpleGraph h) then true else false) else false
    | none => false

Sources

• [AIM-COMBINATORICS-0270] Source item 4, notes[269], Section A.4.

Uses 13 · Used by 1

Statement usesAdjacency-matrix graph instance · Valid adjacency-matrix instance · Graph of a valid instance · Perfect graph · Bitstring 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 byEdmonds's question: an NP description of perfect graphs

DefinitionEdmonds's question: an NP description of perfect graphs#✓fully proved

The perfect-graph decision problem, which accepts exactly the bitstrings that decode to a valid adjacency-matrix instance whose graph is perfect, lies in the complexity class NP: there are a polynomial \(p\) with natural-number coefficients and a polynomial-time verifier \(R\) on pairs of bitstrings such that a bitstring \(x\) is accepted if and only if \(R\) accepts \((x, w)\) for some bitstring \(w\) of length at most \(p(|x|)\).

def conjecture : Prop :=
  perfectGraphProblem ∈ MetaMathlibExt.ComplexityTheory.NP

Sources

• [AIM-COMBINATORICS-0270] Source item 4, notes[269], Section A.4, Contributor Jack Edmonds.

Uses 4 · Used by 1

Statement usesThe perfect-graph decision problem · Complexity classes · Decision problems · The complexity class NP

Used byPerfect graphs have an NP description

TheoremPerfect graphs have an NP description#●ready to prove

The perfect-graph decision problem, which accepts exactly the bitstrings that decode to a valid adjacency-matrix instance whose graph is perfect, lies in the complexity class NP.

Chudnovsky, Cornuéjols, Liu, Seymour and Vušković recognize Berge graphs in polynomial time, and the Strong Perfect Graph Theorem identifies Berge graphs with perfect graphs; hence perfect-graph recognition is in P, and so in NP.

public theorem_wanted conjecture_holds : conjecture

Sources

• Maria Chudnovsky, Gerard Cornuejols, Xinming Liu, Paul Seymour, Kristina Vuskovic, Recognizing Berge graphs, Combinatorica 25 (2005), 143-186, https://doi.org/10.1007/s00493-005-0012-8; Maria Chudnovsky, Neil Robertson, Paul Seymour, Robin Thomas, The strong perfect graph theorem, Annals of Mathematics 164 (2006), 51-229, https://doi.org/10.4007/annals.2006.164.51.

Uses 1

Statement usesEdmonds's question: an NP description of perfect graphs

10 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.