Clique, Independent Set and Vertex Cover: definitions

The three classical threshold problems on graphs, as decision problems on marked graphs: FirstOrder.Language.markedGraph-structures, carrying a binary adjacency relation and a unary mark. The marked set carries the numeric threshold k of the textbook problems in the unary representation of DescriptiveComplexity.Numbers.Unary: the threshold is the cardinality Set.ncard of the marked set, order-free and isomorphism-invariant for free.

• DescriptiveComplexity.Clique: some clique is at least as large as the marked set;
• DescriptiveComplexity.IndependentSet: some independent set is at least as large as the marked set;
• DescriptiveComplexity.VertexCover: some vertex cover is at most as large as the marked set.

The threshold comparisons are comparisons of decoded numbers, and the cardinality arithmetic they need is the shared kit of DescriptiveComplexity.Numbers.Unary: invariance of a decoded number under an equivalence of universes (DescriptiveComplexity.ncard_image_equiv) for the isomorphism-invariance proofs, the reversal of a comparison under complementation (DescriptiveComplexity.ncard_compl_le_ncard_compl_iff) for the Vertex Cover ↔ Independent Set reductions, and the equivalence with the existence of an injection (DescriptiveComplexity.nonempty_embedding_iff_ncard_le, here DescriptiveComplexity.cliqueOn_iff_embedding) for the second-order definition, which guesses that injection as a relation variable. Since cardinality thresholds are only meaningful on finite structures, finiteness of the universe is part of the yes-instances; by ComplexityClass.mem_congr_finite this does not affect any complexity-theoretic statement.

Self-loops are ignored (all three properties are about the underlying loopless graph), and adjacency is required in both directions on ordered pairs, so the problems agree with their standard versions on (structures encoding) simple graphs.

The three predicates are instances of generic properties DescriptiveComplexity.CliqueOn / IndepOn / CoverOn of a binary and a unary predicate on a type; the generic form is shared by the isomorphism-invariance proofs and by the reductions of DescriptiveComplexity.Problems.CliqueFamily.Reductions.

inductive FirstOrder.Language.markedGraphRel : ℕ → Type

Relation symbols of the language of marked graphs.

• adj : markedGraphRel 2

  adj a b: there is an edge from a to b.

• marked : markedGraphRel 1

  marked a: the element a belongs to the marked set.

def FirstOrder.Language.instDecidableEqMarkedGraphRel.decEq {a✝ : ℕ} (x✝ x✝¹ : markedGraphRel a✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance FirstOrder.Language.instDecidableEqMarkedGraphRel {a✝ : ℕ} : DecidableEq (markedGraphRel a✝)

Equations

• FirstOrder.Language.instDecidableEqMarkedGraphRel = FirstOrder.Language.instDecidableEqMarkedGraphRel.decEq

def FirstOrder.Language.markedGraph : Language

The relational language of marked graphs: a graph together with a marked subset of its vertices, whose cardinality serves as threshold.

Equations

• FirstOrder.Language.markedGraph = { Functions := fun (x : ℕ) => Empty, Relations := FirstOrder.Language.markedGraphRel }

instance FirstOrder.Language.instIsRelationalMarkedGraph : Language.markedGraph.IsRelational

@[reducible, inline]

abbrev FirstOrder.Language.mgAdj : Language.markedGraph.Relations 2

The adjacency symbol of marked graphs.

Equations

• FirstOrder.Language.mgAdj = FirstOrder.Language.markedGraphRel.adj

@[reducible, inline]

abbrev FirstOrder.Language.mgMarked : Language.markedGraph.Relations 1

The mark symbol of marked graphs.

Equations

• FirstOrder.Language.mgMarked = FirstOrder.Language.markedGraphRel.marked

Generic threshold properties

The properties underlying the three problems, for an arbitrary binary predicate Adjp (adjacency) and unary predicate Kp (marks) on a type.

def DescriptiveComplexity.CliqueOn {A : Type} (Adjp : A → A → Prop) (Kp : A → Prop) : Prop

Some set that is pairwise Adjp-related (off the diagonal) is at least as large as the number encoded by the Kp-marked elements: “some clique is at least as large as the marked set”.

Equations

• DescriptiveComplexity.CliqueOn Adjp Kp = ∃ (S : A → Prop), (∀ (x y : A), S x → S y → x ≠ y → Adjp x y) ∧ {x : A | Kp x}.ncard ≤ {x : A | S x}.ncard

def DescriptiveComplexity.IndepOn {A : Type} (Adjp : A → A → Prop) (Kp : A → Prop) : Prop

Some set that is pairwise non-Adjp-related (off the diagonal) is at least as large as the number encoded by the Kp-marked elements: “some independent set is at least as large as the marked set”.

Equations

• DescriptiveComplexity.IndepOn Adjp Kp = DescriptiveComplexity.CliqueOn (fun (x y : A) => ¬Adjp x y) Kp

def DescriptiveComplexity.CoverOn {A : Type} (Adjp : A → A → Prop) (Kp : A → Prop) : Prop

Some set meeting every (off-diagonal) Adjp-edge is at most as large as the number encoded by the Kp-marked elements: “some vertex cover is at most as large as the marked set”.

Equations

• DescriptiveComplexity.CoverOn Adjp Kp = ∃ (C : A → Prop), (∀ (x y : A), x ≠ y → Adjp x y → C x ∨ C y) ∧ {x : A | C x}.ncard ≤ {x : A | Kp x}.ncard

The threshold as an injection

On a finite universe, comparing the decoded numbers is comparing sizes, so the threshold conditions can equivalently be read as the existence of an injection. This is the form the second-order definitions guess.

theorem DescriptiveComplexity.cliqueOn_iff_embedding {A : Type} [Finite A] (Adjp : A → A → Prop) (Kp : A → Prop) : CliqueOn Adjp Kp ↔ ∃ (S : A → Prop), (∀ (x y : A), S x → S y → x ≠ y → Adjp x y) ∧ Nonempty ({ x : A // Kp x } ↪ { x : A // S x })

The clique threshold as an injection of the marked set into the clique.

theorem DescriptiveComplexity.indepOn_iff_embedding {A : Type} [Finite A] (Adjp : A → A → Prop) (Kp : A → Prop) : IndepOn Adjp Kp ↔ ∃ (S : A → Prop), (∀ (x y : A), S x → S y → x ≠ y → ¬Adjp x y) ∧ Nonempty ({ x : A // Kp x } ↪ { x : A // S x })

The independent-set threshold as an injection of the marked set into the independent set.

theorem DescriptiveComplexity.coverOn_iff_embedding {A : Type} [Finite A] (Adjp : A → A → Prop) (Kp : A → Prop) : CoverOn Adjp Kp ↔ ∃ (C : A → Prop), (∀ (x y : A), x ≠ y → Adjp x y → C x ∨ C y) ∧ Nonempty ({ x : A // C x } ↪ { x : A // Kp x })

The vertex-cover threshold as an injection of the cover into the marked set.

theorem DescriptiveComplexity.CliqueOn.of_equiv {A B : Type} (u : B ≃ A) {AdjB : B → B → Prop} {KB : B → Prop} {AdjA : A → A → Prop} {KA : A → Prop} (hadj : ∀ (b b' : B), AdjB b b' ↔ AdjA (u b) (u b')) (hK : ∀ (b : B), KB b ↔ KA (u b)) (h : CliqueOn AdjB KB) : CliqueOn AdjA KA

CliqueOn transports along an equivalence commuting with the two predicates.

theorem DescriptiveComplexity.IndepOn.of_equiv {A B : Type} (u : B ≃ A) {AdjB : B → B → Prop} {KB : B → Prop} {AdjA : A → A → Prop} {KA : A → Prop} (hadj : ∀ (b b' : B), AdjB b b' ↔ AdjA (u b) (u b')) (hK : ∀ (b : B), KB b ↔ KA (u b)) (h : IndepOn AdjB KB) : IndepOn AdjA KA

IndepOn transports along an equivalence commuting with the two predicates.

theorem DescriptiveComplexity.CoverOn.of_equiv {A B : Type} (u : B ≃ A) {AdjB : B → B → Prop} {KB : B → Prop} {AdjA : A → A → Prop} {KA : A → Prop} (hadj : ∀ (b b' : B), AdjB b b' ↔ AdjA (u b) (u b')) (hK : ∀ (b : B), KB b ↔ KA (u b)) (h : CoverOn AdjB KB) : CoverOn AdjA KA

CoverOn transports along an equivalence commuting with the two predicates.

theorem DescriptiveComplexity.CliqueOn.equiv_iff {A B : Type} (u : B ≃ A) {AdjB : B → B → Prop} {KB : B → Prop} {AdjA : A → A → Prop} {KA : A → Prop} (hadj : ∀ (b b' : B), AdjB b b' ↔ AdjA (u b) (u b')) (hK : ∀ (b : B), KB b ↔ KA (u b)) : CliqueOn AdjB KB ↔ CliqueOn AdjA KA

CliqueOn transports along an equivalence, iff version.

theorem DescriptiveComplexity.IndepOn.equiv_iff {A B : Type} (u : B ≃ A) {AdjB : B → B → Prop} {KB : B → Prop} {AdjA : A → A → Prop} {KA : A → Prop} (hadj : ∀ (b b' : B), AdjB b b' ↔ AdjA (u b) (u b')) (hK : ∀ (b : B), KB b ↔ KA (u b)) : IndepOn AdjB KB ↔ IndepOn AdjA KA

IndepOn transports along an equivalence, iff version.

theorem DescriptiveComplexity.CoverOn.equiv_iff {A B : Type} (u : B ≃ A) {AdjB : B → B → Prop} {KB : B → Prop} {AdjA : A → A → Prop} {KA : A → Prop} (hadj : ∀ (b b' : B), AdjB b b' ↔ AdjA (u b) (u b')) (hK : ∀ (b : B), KB b ↔ KA (u b)) : CoverOn AdjB KB ↔ CoverOn AdjA KA

CoverOn transports along an equivalence, iff version.

theorem DescriptiveComplexity.cliqueOn_congr {A : Type} {P Q : A → A → Prop} {K K' : A → Prop} (hPQ : ∀ (x y : A), x ≠ y → (P x y ↔ Q x y)) (hK : ∀ (x : A), K x ↔ K' x) : CliqueOn P K ↔ CliqueOn Q K'

CliqueOn only depends on the off-diagonal part of the adjacency predicate and on the extension of the mark predicate.

theorem DescriptiveComplexity.indepOn_congr {A : Type} {P Q : A → A → Prop} {K K' : A → Prop} (hPQ : ∀ (x y : A), x ≠ y → (P x y ↔ Q x y)) (hK : ∀ (x : A), K x ↔ K' x) : IndepOn P K ↔ IndepOn Q K'

IndepOn only depends on the off-diagonal part of the adjacency predicate and on the extension of the mark predicate.

The three problems

def DescriptiveComplexity.MGAdj {A : Type} [FirstOrder.Language.markedGraph.Structure A] (a b : A) : Prop

Adjacency in a marked graph.

Equations

• DescriptiveComplexity.MGAdj a b = FirstOrder.Language.Structure.RelMap FirstOrder.Language.mgAdj ![a, b]

def DescriptiveComplexity.MGMarked {A : Type} [FirstOrder.Language.markedGraph.Structure A] (a : A) : Prop

Markedness in a marked graph.

Equations

• DescriptiveComplexity.MGMarked a = FirstOrder.Language.Structure.RelMap FirstOrder.Language.mgMarked ![a]

def DescriptiveComplexity.HasLargeClique (A : Type) [FirstOrder.Language.markedGraph.Structure A] : Prop

A marked graph contains a clique at least as large as its marked set. (Finiteness of the universe is part of the property: cardinality thresholds are only meaningful on finite structures.)

Equations

• DescriptiveComplexity.HasLargeClique A = (Finite A ∧ DescriptiveComplexity.CliqueOn DescriptiveComplexity.MGAdj DescriptiveComplexity.MGMarked)

def DescriptiveComplexity.HasLargeIndependentSet (A : Type) [FirstOrder.Language.markedGraph.Structure A] : Prop

A marked graph contains an independent set at least as large as its marked set.

Equations

• DescriptiveComplexity.HasLargeIndependentSet A = (Finite A ∧ DescriptiveComplexity.IndepOn DescriptiveComplexity.MGAdj DescriptiveComplexity.MGMarked)

def DescriptiveComplexity.HasSmallVertexCover (A : Type) [FirstOrder.Language.markedGraph.Structure A] : Prop

A marked graph contains a vertex cover at most as large as its marked set.

Equations

• DescriptiveComplexity.HasSmallVertexCover A = (Finite A ∧ DescriptiveComplexity.CoverOn DescriptiveComplexity.MGAdj DescriptiveComplexity.MGMarked)

Isomorphism-invariance and the bundled problems

theorem DescriptiveComplexity.hasLargeClique_iso {A B : Type} [FirstOrder.Language.markedGraph.Structure A] [FirstOrder.Language.markedGraph.Structure B] (e : FirstOrder.Language.markedGraph.Equiv A B) : HasLargeClique A ↔ HasLargeClique B

The clique threshold property is isomorphism-invariant.

theorem DescriptiveComplexity.hasLargeIndependentSet_iso {A B : Type} [FirstOrder.Language.markedGraph.Structure A] [FirstOrder.Language.markedGraph.Structure B] (e : FirstOrder.Language.markedGraph.Equiv A B) : HasLargeIndependentSet A ↔ HasLargeIndependentSet B

The independent-set threshold property is isomorphism-invariant.

theorem DescriptiveComplexity.hasSmallVertexCover_iso {A B : Type} [FirstOrder.Language.markedGraph.Structure A] [FirstOrder.Language.markedGraph.Structure B] (e : FirstOrder.Language.markedGraph.Equiv A B) : HasSmallVertexCover A ↔ HasSmallVertexCover B

The vertex-cover threshold property is isomorphism-invariant.

def DescriptiveComplexity.Clique : DecisionProblem FirstOrder.Language.markedGraph

CLIQUE, as a problem on marked graphs: is there a clique at least as large as the marked set?

Equations

• DescriptiveComplexity.Clique = { Holds := fun (A : Type) (inst : FirstOrder.Language.markedGraph.Structure A) => DescriptiveComplexity.HasLargeClique A, iso_invariant := ⋯ }

def DescriptiveComplexity.IndependentSet : DecisionProblem FirstOrder.Language.markedGraph

INDEPENDENT SET, as a problem on marked graphs: is there an independent set at least as large as the marked set?

Equations

• One or more equations did not get rendered due to their size.

def DescriptiveComplexity.VertexCover : DecisionProblem FirstOrder.Language.markedGraph

VERTEX COVER, as a problem on marked graphs: is there a vertex cover at most as large as the marked set?

Equations

• DescriptiveComplexity.VertexCover = { Holds := fun (A : Type) (inst : FirstOrder.Language.markedGraph.Structure A) => DescriptiveComplexity.HasSmallVertexCover A, iso_invariant := ⋯ }