Independent Set, Clique and Vertex Cover are NP-hard to approximate

The values of a graph (Cslib.Complexity.Graph, read on its declared vertices) are its independence number Graph.indepNum, its clique number Graph.cliqueNum and its vertex cover number Graph.vertexCoverNum, the extreme targets of the decision problems IndependentSet, Clique and VertexCover. The gap problems ask, for an instance (G, k):

• GapIndependentSet s: is indepNum G ≥ k, or indepNum G ≤ s * k?
• GapClique s: is cliqueNum G ≥ k, or cliqueNum G ≤ s * k?
• GapVertexCover r: is vertexCoverNum G ≤ k, or vertexCoverNum G ≥ r * k?

The yes-instances of the first two are exactly IndependentSet and Clique.

The reductions use Karp's graph of a formula (Cslib.Complexity.SAT.toIndependentSet: a vertex for each occurrence of a literal, edges inside clauses and between complementary occurrences), not the graph of Feige, Goldwasser, Lovász, Safra and Szegedy built from a PCP verifier [FGL+96]. An independent set of Karp's graph picks consistent literals in distinct clauses, so it has at most as many vertices as some assignment satisfies clauses (Cslib.Complexity.SAT.exists_card_add_countUnsat_le). Hence the gap of MAX-3SAT (Cslib.Complexity.GapThreeSAT) Arora, Lund, Motwani, Sudan and Szegedy transfers to independent sets with the same soundness, and to cliques of the complement graph (Cslib.Complexity.Graph.compl) Arora and Barak, Chapter 11.

A vertex cover is the complement of an independent set, so vertexCoverNum G = n - indepNum G for the number n of distinct declared vertices (Graph.vertexCoverNum_eq_card_sub_indepNum). For a formula with m clauses of exactly three, not necessarily distinct, literals (Cslib.Complexity.GapExactThreeSAT), Karp's graph has n = 3 m vertices, a satisfiable formula has a cover of 2 m vertices, and if every assignment satisfies at most s * m clauses every cover has at least (3 - s) * m = (1 + (1 - s) / 2) * 2 m vertices Arora and Barak, Chapter 11.

From the gap 1 - 1 / (3 * 2 ^ 77) of MAX-3SAT (Cslib.Complexity.GapThreeSAT_npHard), it is NP-hard to approximate the independence number and the clique number within 1 - 1 / (3 * 2 ^ 77) and the vertex cover number within 1 + 1 / (3 * 2 ^ 78). The constants are far from the best known; amplification to every constant (and beyond) for Independent Set and Clique, as in Feige, Goldwasser, Lovász, Safra and Szegedy, is not proved here.

Main definitions

• Cslib.Complexity.GapIndependentSet, Cslib.Complexity.GapClique, Cslib.Complexity.GapVertexCover: the gap problems.

Main results

• Cslib.Complexity.SAT.card_toFinset_vertices_toIndependentSet: Karp's graph of a formula with clauses of three literals has three vertices per clause.
• Cslib.Complexity.SAT.indepNum_toIndependentSet_le: the independence number of Karp's graph is at most (1 - unsatVal φ) * m.
• Cslib.Complexity.yes_GapIndependentSet, Cslib.Complexity.yes_GapClique: the yes-instances.
• Cslib.Complexity.polyTimeReducible_GapThreeSAT_GapIndependentSet, Cslib.Complexity.polyTimeReducible_GapIndependentSet_GapClique, Cslib.Complexity.polyTimeReducible_GapExactThreeSAT_GapVertexCover: the gap-preserving reductions.
• Cslib.Complexity.GapIndependentSet_npHard, Cslib.Complexity.GapClique_npHard, Cslib.Complexity.GapVertexCover_npHard: constant-factor inapproximability.
• Cslib.Complexity.GapIndependentSet_notMem_PromiseP, Cslib.Complexity.GapClique_notMem_PromiseP, Cslib.Complexity.GapVertexCover_notMem_PromiseP: unless P = NP, no polynomial-time algorithm separates the gap problems.

References

• S. Arora, C. Lund, R. Motwani, M. Sudan, M. Szegedy, Proof verification and the hardness of approximation problems
• S. Arora, B. Barak, Computational Complexity: A Modern Approach, Chapter 11
• U. Feige, S. Goldwasser, L. Lovász, S. Safra, M. Szegedy, Interactive proofs and the hardness of approximating cliques
• R. M. Karp, Reducibility among combinatorial problems

Karp's graph of a formula

theorem Cslib.Complexity.SAT.card_toFinset_vertices_toIndependentSet {φ : Logic.PL.CNF ℕ} (h3 : ∀ c ∈ φ, List.length c = 3) : (toIndependentSet φ).1.1.toFinset.card = 3 * List.length φ

Every occurrence of a formula whose clauses have exactly three literals is a vertex of Karp's graph, and there are 3 m of them for m clauses.

theorem Cslib.Complexity.SAT.indepNum_toIndependentSet_le (φ : Logic.PL.CNF ℕ) : ↑(toIndependentSet φ).1.indepNum ≤ (1 - φ.unsatVal) * ↑(List.length φ)

The independence number of Karp's graph is at most the largest number of clauses an assignment satisfies, which is at most (1 - unsatVal φ) * m for m clauses.

Gap problems

noncomputable def Cslib.Complexity.GapIndependentSet (s : ℝ) : PromiseProblem (Graph × ℕ)

The gap problem of maximum independent set with soundness s: on an instance (G, k), the yes-instances have an independent set of k declared vertices, and the no-instances have no independent set of more than s * k declared vertices.

noncomputable def Cslib.Complexity.GapClique (s : ℝ) : PromiseProblem (Graph × ℕ)

The gap problem of maximum clique with soundness s: on an instance (G, k), the yes-instances have a clique of k declared vertices, and the no-instances have no clique of more than s * k declared vertices.

noncomputable def Cslib.Complexity.GapVertexCover (r : ℝ) : PromiseProblem (Graph × ℕ)

The gap problem of minimum vertex cover with ratio r: on an instance (G, k), the yes-instances have a vertex cover of at most k declared vertices, and the no-instances have no vertex cover of fewer than r * k declared vertices.

theorem Cslib.Complexity.yes_GapIndependentSet {s : ℝ} : (GapIndependentSet s).yes = IndependentSet

The yes-instances of GapIndependentSet are the members of IndependentSet.

theorem Cslib.Complexity.yes_GapClique {s : ℝ} : (GapClique s).yes = Clique

The yes-instances of GapClique are the members of Clique.

Reductions

theorem Cslib.Complexity.polyTimeReducible_GapThreeSAT_GapIndependentSet {s : ℝ} (hs : s < 1) : PromiseProblem.PolyTimeReducible encCNF (Turing.MultiTapeTM.encPair encGraph Turing.MultiTapeTM.encNat) (GapThreeSAT s) (GapIndependentSet s)

MAX-3SAT reduces to maximum independent set with the same gap, by Karp's graph: a satisfiable formula has an independent set with a vertex in each clause, and an independent set gives an assignment satisfying as many clauses.

theorem Cslib.Complexity.polyTimeReducible_GapIndependentSet_GapClique {s : ℝ} : PromiseProblem.PolyTimeReducible (Turing.MultiTapeTM.encPair encGraph Turing.MultiTapeTM.encNat) (Turing.MultiTapeTM.encPair encGraph Turing.MultiTapeTM.encNat) (GapIndependentSet s) (GapClique s)

Maximum independent set reduces to maximum clique with the same gap, by complementing the graph on its declared vertices.

theorem Cslib.Complexity.polyTimeReducible_GapExactThreeSAT_GapVertexCover {s : ℝ} (hs : s < 1) : PromiseProblem.PolyTimeReducible encCNF (Turing.MultiTapeTM.encPair encGraph Turing.MultiTapeTM.encNat) (GapExactThreeSAT s) (GapVertexCover (1 + (1 - s) / 2))

MAX-E3SAT reduces to minimum vertex cover: Karp's graph of a formula with m clauses of three, not necessarily distinct, literals has 3 m vertices, so the target m of an independent set becomes the target 2 m of a vertex cover (IndependentSet.toVertexCover), and soundness s for MAX-E3SAT becomes the ratio 1 + (1 - s) / 2 for vertex covers.

Inapproximability

theorem Cslib.Complexity.GapIndependentSet_npHard : PromiseProblem.NPHard (Turing.MultiTapeTM.encPair encGraph Turing.MultiTapeTM.encNat) (GapIndependentSet (1 - 1 / (3 * 2 ^ 77)))

Maximum independent set is NP-hard to approximate within 1 - 1 / (3 * 2 ^ 77): given a graph and a target k, distinguishing graphs with an independent set of k vertices from graphs without an independent set of more than (1 - 1 / (3 * 2 ^ 77)) * k vertices is NP-hard. The gap comes from MAX-3SAT [ALM+98] through Karp's graph.

theorem Cslib.Complexity.GapClique_npHard : PromiseProblem.NPHard (Turing.MultiTapeTM.encPair encGraph Turing.MultiTapeTM.encNat) (GapClique (1 - 1 / (3 * 2 ^ 77)))

Maximum clique is NP-hard to approximate within 1 - 1 / (3 * 2 ^ 77): given a graph and a target k, distinguishing graphs with a clique of k vertices from graphs without a clique of more than (1 - 1 / (3 * 2 ^ 77)) * k vertices is NP-hard. The gap of maximum independent set transfers to the complement graph.

theorem Cslib.Complexity.GapVertexCover_npHard : PromiseProblem.NPHard (Turing.MultiTapeTM.encPair encGraph Turing.MultiTapeTM.encNat) (GapVertexCover (1 + 1 / (3 * 2 ^ 78)))

Minimum vertex cover is NP-hard to approximate within 1 + 1 / (3 * 2 ^ 78) [ALM+98]: given a graph and a target k, distinguishing graphs with a vertex cover of at most k vertices from graphs without a vertex cover of fewer than (1 + 1 / (3 * 2 ^ 78)) * k vertices is NP-hard.

theorem Cslib.Complexity.GapIndependentSet_notMem_PromiseP {β : Type} {enc : β ↪ List Bool} (h : P enc ≠ NP enc) : GapIndependentSet (1 - 1 / (3 * 2 ^ 77)) ∉ PromiseP (Turing.MultiTapeTM.encPair encGraph Turing.MultiTapeTM.encNat)

Unless P = NP, no polynomial-time algorithm distinguishes graphs with an independent set of k vertices from graphs without one of more than (1 - 1 / (3 * 2 ^ 77)) * k vertices.

theorem Cslib.Complexity.GapClique_notMem_PromiseP {β : Type} {enc : β ↪ List Bool} (h : P enc ≠ NP enc) : GapClique (1 - 1 / (3 * 2 ^ 77)) ∉ PromiseP (Turing.MultiTapeTM.encPair encGraph Turing.MultiTapeTM.encNat)

Unless P = NP, no polynomial-time algorithm distinguishes graphs with a clique of k vertices from graphs without one of more than (1 - 1 / (3 * 2 ^ 77)) * k vertices.

theorem Cslib.Complexity.GapVertexCover_notMem_PromiseP {β : Type} {enc : β ↪ List Bool} (h : P enc ≠ NP enc) : GapVertexCover (1 + 1 / (3 * 2 ^ 78)) ∉ PromiseP (Turing.MultiTapeTM.encPair encGraph Turing.MultiTapeTM.encNat)

Unless P = NP, no polynomial-time algorithm distinguishes graphs with a vertex cover of at most k vertices from graphs without one of fewer than (1 + 1 / (3 * 2 ^ 78)) * k vertices.