theorem List.length_wf {α : Type} : WellFounded fun (x y : List α) => x.length < y.length

@[irreducible]

def SimpleGraph.Bron_Kerbosch_full {α : Type} [Fintype α] [DecidableEq α] (G : SimpleGraph α) [DecidableRel G.Adj] {R P X : List α} (Pnd : P.Nodup) (RP : R.Disjoint P) (RX : R.Disjoint X) (PX : P.Disjoint X) : List (Finset α)

Equations

• G.Bron_Kerbosch_full Pnd_2 RP_2 RX_2 PX_3 = [R.toFinset]
• G.Bron_Kerbosch_full Pnd_2 RP_2 RX_2 PX_3 = []
• G.Bron_Kerbosch_full Pnd_2 RP_2 RX PX_2 = G.Bron_Kerbosch_full ⋯ ⋯ ⋯ ⋯ ++ G.Bron_Kerbosch_full ⋯ ⋯ ⋯ ⋯

theorem SimpleGraph.Bron_Kerbosch_maximal_clique {α : Type} [Fintype α] [deceq : DecidableEq α] (G : SimpleGraph α) [DecidableRel G.Adj] {R P X : List α} (Pnd : P.Nodup) (RP : R.Disjoint P) (RX : R.Disjoint X) (PX : P.Disjoint X) : G.IsClique ↑R.toFinset → (∀ (v : α), v ∈ P.toFinset ∪ X.toFinset ↔ ∀ u ∈ R, G.Adj v u) → ∀ (S : Finset α), S ∈ G.Bron_Kerbosch_full Pnd RP RX PX ↔ R.toFinset ⊆ S ∧ S ⊆ R.toFinset ∪ P.toFinset ∧ Maximal G.IsClique ↑S

def SimpleGraph.Bron_Kerbosch {α : Type} [fe : FinEnum α] (G : SimpleGraph α) [DecidableRel G.Adj] : List (Finset α)

Equations

• G.Bron_Kerbosch = G.Bron_Kerbosch_full ⋯ ⋯ ⋯ ⋯

theorem SimpleGraph.Bron_Kerbosch_correct {α : Type} [FinEnum α] (G : SimpleGraph α) [DecidableRel G.Adj] (S : Finset α) : Maximal G.IsClique ↑S ↔ S ∈ G.Bron_Kerbosch

theorem SimpleGraph.Bron_Kerbosch_maximum_clique {α : Type} [FinEnum α] (G : SimpleGraph α) [DecidableRel G.Adj] (S : Finset α) : G.IsMaximumClique S → S ∈ G.Bron_Kerbosch

theorem SimpleGraph.Bron_Kerbosch_cliqueNum {α : Type} [FinEnum α] (G : SimpleGraph α) [DecidableRel G.Adj] : G.cliqueNum = (List.map Finset.card G.Bron_Kerbosch).max?.getD 0