Independent sets

IndependentSet is the set of graphs, given by a list of vertices and a list of edges, together with a number m, such that the graph has an independent set of m declared vertices Arora and Barak, Section 2.4. Graphs are read on their declared vertices through Cslib.Complexity.Graph.induced, and independent sets through SimpleGraph.IsNIndepSet.

The reduction SAT.toIndependentSet from SAT is Karp's: one vertex for each occurrence of a literal, edges between occurrences in the same clause and between complementary occurrences, and m the number of clauses [Kar72]. An independent set with one vertex in each clause picks a literal in each clause without contradictions, which is exactly a satisfying assignment.

Vertices and target sizes use binary encoding (encNat). A certificate masks the declared vertex list at first occurrences so duplicate vertex entries cannot inflate the selected set, and checks the selected count in binary without unary expansion of m. The verifier is an instance of the subset-witness verifier Cslib.Complexity.subsetVerifier, which handles the certificate length.

The same problem as a class of finite structures, closed under isomorphism and without an encoding, with the target size given by a unary relation, is Cslib.Logic.FO.sizedGraph.IndependentSet. There loops are ignored, edges need not be symmetric, and the reductions between independent set, clique and vertex cover are quantifier-free first-order interpretations.

Main definitions

• Cslib.Complexity.IndependentSetInstance, Cslib.Complexity.IndependentSet.
• Cslib.Complexity.IndependentSet.verifier.
• Cslib.Complexity.SAT.toIndependentSet.
• Cslib.Complexity.Graph.indepNum: the independence number (G.induced.indepNum).

Main results

• Cslib.Complexity.mem_IndependentSet_iff: independent sets as subsets of ℕ contained in the declared vertices.
• Cslib.Complexity.SAT.toIndependentSet_mem_iff: toIndependentSet φ ∈ IndependentSet ↔ φ ∈ SAT.
• Cslib.Complexity.SAT.exists_card_add_countUnsat_le: an independent set of Karp's graph gives an assignment satisfying as many clauses.
• Cslib.Complexity.Graph.le_indepNum_iff: the independence number is the largest target of IndependentSet.
• Cslib.Complexity.SAT.computableInPolyTime_toIndependentSet: Karp's reduction is polynomial-time.
• Cslib.Complexity.IndependentSet.isVerifier, Cslib.Complexity.IndependentSet.mem_NP: IndependentSet ∈ NP encIndependentSetInstance.
• Cslib.Complexity.polyTimeReducible_SAT_IndependentSet, Cslib.Complexity.IndependentSet_npHard, Cslib.Complexity.IndependentSet_npComplete: IndependentSet is NP-complete.

References

• S. Arora, B. Barak, Computational Complexity: A Modern Approach
• R. M. Karp, Reducibility among combinatorial problems

structure Cslib.Complexity.IndependentSetInstance : Type

An instance (graph, m) of Independent Set.

• graph : Graph

  The graph in which to find an independent set.

• m : ℕ

  The target number of declared vertices.

theorem Cslib.Complexity.IndependentSetInstance.ext_iff {x y : IndependentSetInstance} : x = y ↔ x.graph = y.graph ∧ x.m = y.m

theorem Cslib.Complexity.IndependentSetInstance.ext {x y : IndependentSetInstance} (graph : x.graph = y.graph) (m : x.m = y.m) : x = y

@[instance_reducible]

instance Cslib.Complexity.instDecidableEqIndependentSetInstance : DecidableEq IndependentSetInstance

def Cslib.Complexity.instDecidableEqIndependentSetInstance.decEq (x✝ x✝¹ : IndependentSetInstance) : Decidable (x✝ = x✝¹)

def Cslib.Complexity.instReprIndependentSetInstance.repr : IndependentSetInstance → ℕ → Std.Format

@[instance_reducible]

instance Cslib.Complexity.instReprIndependentSetInstance : Repr IndependentSetInstance

@[instance_reducible]

instance Cslib.Complexity.instInhabitedIndependentSetInstance : Inhabited IndependentSetInstance

theorem Cslib.Complexity.encIndependentSetInstance_graph_deg : Turing.MultiTapeTM.ComputableInDegree IndependentSetInstance.graph encIndependentSetInstance encGraph 1 1

theorem Cslib.Complexity.encIndependentSetInstance_m_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → IndependentSetInstance} : Turing.MultiTapeTM.ComputableInSpace g✝ encIn✝ encIndependentSetInstance S✝ → Turing.MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).m) encIn✝ Turing.MultiTapeTM.encNat S✝

theorem Cslib.Complexity.encIndependentSetInstance_m_deg : Turing.MultiTapeTM.ComputableInDegree IndependentSetInstance.m encIndependentSetInstance Turing.MultiTapeTM.encNat 1 1

@[simp]

theorem Cslib.Complexity.encIndependentSetInstance_apply (a : IndependentSetInstance) : encIndependentSetInstance a = encIndependentSetInstanceFields (a.graph, a.m)

@[reducible, inline]

abbrev Cslib.Complexity.encIndependentSetInstanceFields : Graph × ℕ ↪ List Bool

The tuple of the fields of encIndependentSetInstance.

theorem Cslib.Complexity.encIndependentSetInstance_mk_inO {γ : Type} {encIn : γ ↪ List Bool} {x0 : γ → Graph} {T0 S0 x1 T1 S1 : γ → ℕ} (h0 : Turing.MultiTapeTM.ComputableInO x0 encIn encGraph T0 S0) (h1 : Turing.MultiTapeTM.ComputableInO x1 encIn Turing.MultiTapeTM.encNat T1 S1) : Turing.MultiTapeTM.ComputableInO (fun (x : γ) => { graph := x0 x, m := x1 x }) encIn encIndependentSetInstance (fun (x : γ) => T0 x + T1 x) fun (x : γ) => S0 x + S1 x

theorem Cslib.Complexity.encIndependentSetInstance_graph_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → IndependentSetInstance} : Turing.MultiTapeTM.ComputableInSpace g✝ encIn✝ encIndependentSetInstance S✝ → Turing.MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).graph) encIn✝ encGraph S✝

theorem Cslib.Complexity.encIndependentSetInstance_graph_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → IndependentSetInstance} : Turing.MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encIndependentSetInstance → Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).graph) encIn✝ encGraph

theorem Cslib.Complexity.encIndependentSetInstance_graph_inO : Turing.MultiTapeTM.ComputableInO IndependentSetInstance.graph encIndependentSetInstance encGraph (fun (a : IndependentSetInstance) => (encIndependentSetInstance a).length) fun (a : IndependentSetInstance) => (encIndependentSetInstance a).length

theorem Cslib.Complexity.encIndependentSetInstance_mk_polyTime {γ : Type} {encIn : γ ↪ List Bool} {x0 : γ → Graph} {x1 : γ → ℕ} (h0 : Turing.MultiTapeTM.ComputableInPolyTime x0 encIn encGraph) (h1 : Turing.MultiTapeTM.ComputableInPolyTime x1 encIn Turing.MultiTapeTM.encNat) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : γ) => { graph := x0 x, m := x1 x }) encIn encIndependentSetInstance

def Cslib.Complexity.encIndependentSetInstance : IndependentSetInstance ↪ List Bool

Framed encGraph followed by binary target encNat, encoding IndependentSetInstance.

theorem Cslib.Complexity.encIndependentSetInstance_m_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → IndependentSetInstance} : Turing.MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encIndependentSetInstance → Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).m) encIn✝ Turing.MultiTapeTM.encNat

theorem Cslib.Complexity.encIndependentSetInstance_mk_budget {γ : Type} {encIn : γ ↪ List Bool} {budget : γ → ℕ} {x0 : γ → Graph} {x1 : γ → ℕ} (h0 : Turing.MultiTapeTM.ComputableInSpace x0 encIn encGraph budget) (h1 : Turing.MultiTapeTM.ComputableInSpace x1 encIn Turing.MultiTapeTM.encNat budget) : Turing.MultiTapeTM.ComputableInSpace (fun (x : γ) => { graph := x0 x, m := x1 x }) encIn encIndependentSetInstance budget

theorem Cslib.Complexity.encIndependentSetInstance_mk_deg : Turing.MultiTapeTM.ComputableInDegree (fun (p : Graph × ℕ) => { graph := p.1, m := p.2 }) encIndependentSetInstanceFields encIndependentSetInstance 1 1

theorem Cslib.Complexity.encIndependentSetInstance_m_inO : Turing.MultiTapeTM.ComputableInO IndependentSetInstance.m encIndependentSetInstance Turing.MultiTapeTM.encNat (fun (a : IndependentSetInstance) => (encIndependentSetInstance a).length) fun (a : IndependentSetInstance) => (encIndependentSetInstance a).length

theorem Cslib.Complexity.encIndependentSetInstance_fields_deg : Turing.MultiTapeTM.ComputableInDegree (fun (a : IndependentSetInstance) => (a.graph, a.m)) encIndependentSetInstance encIndependentSetInstanceFields 1 1

def Cslib.Complexity.IndependentSet : Set IndependentSetInstance

The graphs with an independent set of m of their vertices Arora and Barak, Section 2.4.

theorem Cslib.Complexity.mem_IndependentSet_iff {x : IndependentSetInstance} : x ∈ IndependentSet ↔ ∃ (S : Finset ℕ), (∀ v ∈ S, v ∈ x.graph.vertices) ∧ x.graph.toSimpleGraph.IsNIndepSet x.m S

Membership in IndependentSet as a finite set of m declared vertices that is independent in x.graph.toSimpleGraph.

@[simp]

theorem Cslib.Complexity.mem_IndependentSet_iff_mk {G : Graph} {m : ℕ} : { graph := G, m := m } ∈ IndependentSet ↔ ∃ (S : Finset ℕ), (∀ v ∈ S, v ∈ G.vertices) ∧ G.toSimpleGraph.IsNIndepSet m S

Karp's reduction

def Cslib.Logic.PL.Occurrence.vertex (o : Occurrence ℕ) : ℕ

The vertex of an occurrence.

def Cslib.Logic.PL.Occurrence.Conflict (o o' : Occurrence ℕ) : Prop

Two occurrences conflict when they are in the same clause or are complementary.

@[instance_reducible]

instance Cslib.Complexity.SAT.instDecidableRelOccurrenceNatConflict : DecidableRel Logic.PL.Occurrence.Conflict

def Cslib.Complexity.SAT.toIndependentSet (φ : Logic.PL.CNF ℕ) : IndependentSetInstance

Karp's reduction from SAT to IndependentSet.

theorem Cslib.Logic.PL.Occurrence.Conflict.symm {o o' : Occurrence ℕ} (h : o.Conflict o') : o'.Conflict o

theorem Cslib.Complexity.SAT.adj_toIndependentSet_iff {φ : Logic.PL.CNF ℕ} {o o' : Logic.PL.Occurrence ℕ} (ho : o ∈ Logic.PL.occurrences φ) (ho' : o' ∈ Logic.PL.occurrences φ) : (toIndependentSet φ).graph.toSimpleGraph.Adj o.vertex o'.vertex ↔ o.Conflict o'

In the graph of Karp's reduction, two occurrences are adjacent exactly when they conflict.

theorem Cslib.Complexity.SAT.exists_card_add_countUnsat_le {φ : Logic.PL.CNF ℕ} {S : Finset ℕ} (hSV : ∀ v ∈ S, v ∈ (toIndependentSet φ).graph.vertices) (hS : (toIndependentSet φ).graph.toSimpleGraph.IsIndepSet ↑S) : ∃ (σ : ℕ → Bool), S.card + Logic.PL.CNF.countUnsat σ φ ≤ List.length φ

An independent set of Karp's graph gives an assignment satisfying as many clauses: the assignment making the chosen positive literals true satisfies the clause of every chosen occurrence, and distinct chosen occurrences lie in distinct clauses.

theorem Cslib.Complexity.SAT.toIndependentSet_mem_iff (φ : Logic.PL.CNF ℕ) : toIndependentSet φ ∈ IndependentSet ↔ φ ∈ SAT

Correctness of Karp's reduction. A formula is satisfiable exactly when its graph has an independent set with as many vertices as the formula has clauses.

Polynomial-time reduction

theorem Cslib.Logic.PL.Occurrence.computableInPolyTime_vertex : Turing.MultiTapeTM.ComputableInPolyTime vertex Complexity.SAT.encOccurrence Turing.MultiTapeTM.encNat

Computing the binary vertex label of an occurrence from its unary indices is polynomial-time.

theorem Cslib.Logic.PL.Occurrence.computableInPolyTime_conflict : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : Occurrence ℕ × Occurrence ℕ) => decide (p.1.Conflict p.2)) (Turing.MultiTapeTM.encPair Complexity.SAT.encOccurrence Complexity.SAT.encOccurrence) Turing.MultiTapeTM.encBool

Testing whether two occurrences conflict is polynomial-time.

theorem Cslib.Complexity.SAT.computableInPolyTime_toIndependentSet : Turing.MultiTapeTM.ComputableInPolyTime toIndependentSet encCNF encIndependentSetInstance

Karp's reduction toIndependentSet is computable in polynomial time.

def Cslib.Complexity.IndependentSet.verifier : IndependentSetInstance × List Bool → Bool

The verifier for IndependentSet: select distinct declared vertices from the certificate mask, check that their count equals m, and check that no two distinct selected vertices are adjacent.

theorem Cslib.Complexity.IndependentSet.isVerifier : IsVerifier encIndependentSetInstance Polynomial.X verifier IndependentSet

IndependentSet.verifier verifies IndependentSet with certificates as long as the encoded instance.

theorem Cslib.Complexity.IndependentSet.computableInPolyTime_verifier : Turing.MultiTapeTM.ComputableInPolyTime verifier (Turing.MultiTapeTM.encPair encIndependentSetInstance Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool

The IndependentSet verifier is polynomial-time.

theorem Cslib.Complexity.IndependentSet.mem_NP : IndependentSet ∈ NP encIndependentSetInstance

IndependentSet belongs to NP.

theorem Cslib.Complexity.polyTimeReducible_SAT_IndependentSet : PolyTimeReducible encCNF encIndependentSetInstance SAT IndependentSet

SAT reduces to IndependentSet in polynomial time via SAT.toIndependentSet.

theorem Cslib.Complexity.IndependentSet_npHard : NPHard encIndependentSetInstance IndependentSet

IndependentSet is NP-hard.

theorem Cslib.Complexity.IndependentSet_npComplete : NPComplete encIndependentSetInstance IndependentSet

IndependentSet is NP-complete Arora and Barak, Section 2.4.

The independence number

noncomputable def Cslib.Complexity.Graph.indepNum (G : Graph) : ℕ

The independence number of a graph: the largest number of declared vertices that are pairwise non-adjacent.

theorem Cslib.Complexity.Graph.mem_IndependentSet_of_le {G : Graph} {k k' : ℕ} (h : { graph := G, m := k } ∈ IndependentSet) (hk : k' ≤ k) : { graph := G, m := k' } ∈ IndependentSet

Fewer vertices of an independent set are independent.

theorem Cslib.Complexity.Graph.indepNum_mem_IndependentSet (G : Graph) : { graph := G, m := G.indepNum } ∈ IndependentSet

The independence number is the size of an independent set.

theorem Cslib.Complexity.Graph.le_indepNum_iff {G : Graph} {k : ℕ} : k ≤ G.indepNum ↔ { graph := G, m := k } ∈ IndependentSet

The independence number is the largest target of IndependentSet.

theorem Cslib.Complexity.Graph.indepNum_le_card (G : Graph) : G.indepNum ≤ G.vertices.toFinset.card

The independence number is at most the number of distinct declared vertices.

theorem Cslib.Complexity.Graph.le_card_of_mem_IndependentSet {G : Graph} {k : ℕ} (h : { graph := G, m := k } ∈ IndependentSet) : k ≤ G.vertices.toFinset.card

An independent set has at most as many vertices as the distinct declared vertices.