Independent set, clique and vertex cover as classes of finite structures

An instance of independent set, clique or vertex cover is a graph together with a target size. Here it is a finite structure of the vocabulary sizedGraph: a binary relation adj, the edges, and a unary relation size, whose number of elements is the target size. Giving the size as a set of elements rather than as a number keeps the vocabulary free of numeric predicates, and makes the reductions below one-dimensional.

The edge relation need not be symmetric, and loops are ignored: an independent set has no edge between two distinct vertices in either direction, a clique has edges between any two distinct vertices in both directions, and a vertex cover contains an endpoint of every edge between distinct vertices. On simple graphs these are the usual problems: clique and node cover [Kar72] and independent set [GJ79]. The sets asked for have exactly |size| vertices; since subsets of independent sets and of cliques, and supersets of vertex covers, are again such sets, this is equivalent to the usual thresholds "at least |size|" for independent sets and cliques and "at most |size|" for vertex covers, as |size| never exceeds the number of vertices.

The machine-level versions of these problems, on graphs encoded as lists of vertices and edges with a binary target size, are Cslib.Complexity.IndependentSet, Cslib.Complexity.Clique and Cslib.Complexity.VertexCover, which are proved NP-complete. Those read graphs as simple graphs on their declared vertices; the classes here are classes of finite structures, closed under isomorphism, without an encoding, and their reductions are first-order interpretations rather than polynomial-time functions.

• sizedGraph.IndependentSet: the graph has an independent set of |size| vertices.
• sizedGraph.Clique: the graph has a clique of |size| vertices.
• sizedGraph.VertexCover: the graph has a vertex cover of |size| vertices.

The three classes are closed under isomorphism, and quantifier-free reducible to each other. Complementing the edge relation off the diagonal (sizedGraph.complementEdges) turns independent sets into cliques and back, and complementing the size relation (sizedGraph.complementSize) turns an instance asking for an independent set of size k into one asking for a vertex cover of size n - k: a set is independent exactly when its complement is a vertex cover. Both are one-dimensional quantifier-free interpretations, and their composite is Karp's reduction from clique to node cover [Kar72]. The reductions are proved with fo_reduction, which leaves only these facts about sets of vertices.

Main definitions

• Cslib.Logic.FO.sizedGraph: the vocabulary of graphs with a size relation.
• Cslib.Logic.FO.sizedGraph.IndependentSet, Cslib.Logic.FO.sizedGraph.Clique, Cslib.Logic.FO.sizedGraph.VertexCover: the classes of finite structures.
• Cslib.Logic.FO.sizedGraph.complementEdges, Cslib.Logic.FO.sizedGraph.complementSize: the interpretations complementing the edge relation and the size relation.

Main results

• Cslib.Logic.FO.sizedGraph.isoClosed_IndependentSet, Cslib.Logic.FO.sizedGraph.isoClosed_Clique, Cslib.Logic.FO.sizedGraph.isoClosed_VertexCover: closure under isomorphism.
• Cslib.Logic.FO.sizedGraph.qfReduces_IndependentSet_Clique, Cslib.Logic.FO.sizedGraph.qfReduces_Clique_IndependentSet: complementing the edges.
• Cslib.Logic.FO.sizedGraph.qfReduces_IndependentSet_VertexCover, Cslib.Logic.FO.sizedGraph.qfReduces_VertexCover_IndependentSet: complementing the size.
• Cslib.Logic.FO.sizedGraph.qfReduces_Clique_VertexCover, Cslib.Logic.FO.sizedGraph.qfReduces_VertexCover_Clique: by transitivity.

References

• N. Immerman, Descriptive Complexity
• R. M. Karp, Reducibility among combinatorial problems
• M. R. Garey and D. S. Johnson, Computers and Intractability

inductive Cslib.Logic.FO.SizedGraphRel : ℕ → Type

The relation symbols of graphs with a size relation.

• adj : SizedGraphRel 2

  The edge relation.

• size : SizedGraphRel 1

  The size relation, whose number of elements is the target size.

def Cslib.Logic.FO.instDecidableEqSizedGraphRel.decEq {a✝ : ℕ} (x✝ x✝¹ : SizedGraphRel a✝) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance Cslib.Logic.FO.instDecidableEqSizedGraphRel {a✝ : ℕ} : DecidableEq (SizedGraphRel a✝)

def Cslib.Logic.FO.sizedGraph : FirstOrder.Language

The vocabulary of graphs with a size relation: a binary edge relation and a unary relation whose number of elements is a target size.

instance Cslib.Logic.FO.instIsRelationalSizedGraph : sizedGraph.IsRelational

@[reducible, inline]

abbrev Cslib.Logic.FO.sizedGraph.adj : sizedGraph.Relations 2

The edge relation symbol.

@[reducible, inline]

abbrev Cslib.Logic.FO.sizedGraph.size : sizedGraph.Relations 1

The size relation symbol.

The classes

def Cslib.Logic.FO.sizedGraph.IndependentSet : Set (CategoryTheory.Bundled sizedGraph.Structure)

Independent set: the structures whose graph has an independent set, a set of vertices no two distinct of which are adjacent, with as many vertices as the size relation holds of.

def Cslib.Logic.FO.sizedGraph.Clique : Set (CategoryTheory.Bundled sizedGraph.Structure)

Clique: the structures whose graph has a clique, a set of vertices any two distinct of which are adjacent, with as many vertices as the size relation holds of.

def Cslib.Logic.FO.sizedGraph.VertexCover : Set (CategoryTheory.Bundled sizedGraph.Structure)

Vertex cover: the structures whose graph has a vertex cover, a set of vertices containing an endpoint of every edge between distinct vertices, with as many vertices as the size relation holds of.

theorem Cslib.Logic.FO.sizedGraph.mem_IndependentSet {M : CategoryTheory.Bundled sizedGraph.Structure} : M ∈ IndependentSet ↔ ∃ (s : Set ↑M), s.ncard = {x : ↑M | FirstOrder.Language.Structure.RelMap sizedGraph.size ![x]}.ncard ∧ s.Pairwise fun (x y : ↑M) => ¬FirstOrder.Language.Structure.RelMap sizedGraph.adj ![x, y]

theorem Cslib.Logic.FO.sizedGraph.mem_Clique {M : CategoryTheory.Bundled sizedGraph.Structure} : M ∈ Clique ↔ ∃ (s : Set ↑M), s.ncard = {x : ↑M | FirstOrder.Language.Structure.RelMap sizedGraph.size ![x]}.ncard ∧ s.Pairwise fun (x y : ↑M) => FirstOrder.Language.Structure.RelMap sizedGraph.adj ![x, y]

theorem Cslib.Logic.FO.sizedGraph.mem_VertexCover {M : CategoryTheory.Bundled sizedGraph.Structure} : M ∈ VertexCover ↔ ∃ (s : Set ↑M), s.ncard = {x : ↑M | FirstOrder.Language.Structure.RelMap sizedGraph.size ![x]}.ncard ∧ ∀ (x y : ↑M), x ≠ y → FirstOrder.Language.Structure.RelMap sizedGraph.adj ![x, y] → x ∈ s ∨ y ∈ s

Closure under isomorphism

theorem Cslib.Logic.FO.sizedGraph.isoClosed_IndependentSet : IsoClosed IndependentSet

Independent set is closed under isomorphism.

theorem Cslib.Logic.FO.sizedGraph.isoClosed_Clique : IsoClosed Clique

Clique is closed under isomorphism.

theorem Cslib.Logic.FO.sizedGraph.isoClosed_VertexCover : IsoClosed VertexCover

Vertex cover is closed under isomorphism.

Reductions

def Cslib.Logic.FO.sizedGraph.complementEdges : Interpretation sizedGraph sizedGraph Unit

Complement the edge relation off the diagonal, keeping the size relation.

def Cslib.Logic.FO.sizedGraph.complementSize : Interpretation sizedGraph sizedGraph Unit

Complement the size relation, keeping the edge relation.

theorem Cslib.Logic.FO.sizedGraph.qfReduces_IndependentSet_Clique : QFReduces IndependentSet Clique

Independent set reduces to clique by complementing the edge relation: an independent set of G is a clique of its complement.

theorem Cslib.Logic.FO.sizedGraph.qfReduces_Clique_IndependentSet : QFReduces Clique IndependentSet

Clique reduces to independent set by complementing the edge relation: a clique of G is an independent set of its complement.

theorem Cslib.Logic.FO.sizedGraph.qfReduces_IndependentSet_VertexCover : QFReduces IndependentSet VertexCover

Independent set reduces to vertex cover by complementing the size relation: a set of k vertices is independent exactly when its complement, of n - k vertices, is a vertex cover.

theorem Cslib.Logic.FO.sizedGraph.qfReduces_VertexCover_IndependentSet : QFReduces VertexCover IndependentSet

Vertex cover reduces to independent set by complementing the size relation: a set of k vertices is a vertex cover exactly when its complement, of n - k vertices, is independent.

theorem Cslib.Logic.FO.sizedGraph.qfReduces_Clique_VertexCover : QFReduces Clique VertexCover

Clique reduces to vertex cover, through independent set.

theorem Cslib.Logic.FO.sizedGraph.qfReduces_VertexCover_Clique : QFReduces VertexCover Clique

Vertex cover reduces to clique, through independent set.