MAX-2CSP is NP-hard to approximate

An instance of MAX-2CSP over a finite alphabet α is an executable constraint graph (Cslib.PCP.Encoded.Graph): numbered vertices and a list of edges, each carrying the complete table of a binary constraint on α. Its value is the largest proportion of the edges that a labelling of the vertices satisfies, 1 - unsatVal; the declared vertex count plays no role. GapTwoCSP α s is the gap problem with perfect completeness: the yes-instances are the satisfiable ones and the no-instances those of value at most s.

The PCP theorem in its hardness-of-approximation form Arora and Barak, Chapter 11 is Dinur's gap construction [Din07]: composed with the Cook–Levin reduction, the concrete executable SAT-to-gap pipeline Cslib.PCP.Encoded.gapGraph maps satisfiable formulas to satisfiable constraint graphs and unsatisfiable ones to constraint graphs in which every labelling violates at least the proportion 2 ^ (-61) of the edges, over the alphabet Bool × (Fin 6 → Bool) of 128 symbols. Hence MAX-2CSP over 128 symbols is NP-hard to approximate within 1 - 2 ^ (-61). The constants are those of the landed construction, which was not optimized for them.

Main definitions

• Cslib.Complexity.GapTwoCSP: the gap problem of MAX-2CSP with perfect completeness.

Main results

• Cslib.Complexity.GapTwoCSP_npHard: distinguishing satisfiable MAX-2CSP instances over 128 symbols from those of value at most 1 - 2 ^ (-61) is NP-hard.
• Cslib.Complexity.GapTwoCSP_notMem_PromiseP: unless P = NP, no polynomial-time algorithm does so.

References

• I. Dinur, The PCP theorem by gap amplification
• S. Arora, B. Barak, Computational Complexity: A Modern Approach, Chapters 11 and 22

noncomputable def Cslib.Complexity.GapTwoCSP (α : Type) (s : ℝ) : PromiseProblem (PCP.Encoded.Graph (α → α → Bool))

The gap problem of MAX-2CSP over the alphabet α with perfect completeness and soundness s. Instances are executable constraint graphs whose edges carry constraint tables; their value is the largest proportion of the edges satisfied by a labelling of the vertices. The yes-instances have value one, the no-instances value at most s.

theorem Cslib.Complexity.mem_yes_GapTwoCSP {α : Type} {s : ℝ} {g : PCP.Encoded.Graph (α → α → Bool)} [Nonempty α] : g ∈ (GapTwoCSP α s).yes ↔ (g.toGraph id).Satisfiable

The yes-instances of GapTwoCSP are the satisfiable constraint graphs.

theorem Cslib.Complexity.mem_no_GapTwoCSP {α : Type} {s : ℝ} {g : PCP.Encoded.Graph (α → α → Bool)} (hs : s < 1) : g ∈ (GapTwoCSP α s).no ↔ 1 - s ≤ (g.toGraph id).unsatVal

For s < 1, the no-instances of GapTwoCSP are the constraint graphs in which every labelling violates at least the proportion 1 - s of the edges.

theorem Cslib.Complexity.GapTwoCSP_npHard : PromiseProblem.NPHard (PCP.Encoded.Graph.encoding (Turing.MultiTapeTM.encPi (Turing.MultiTapeTM.encPi Turing.MultiTapeTM.encBool))) (GapTwoCSP (Bool × (Fin 6 → Bool)) (1 - 1 / 2 ^ 61))

MAX-2CSP is NP-hard to approximate [Din07]: over the alphabet Bool × (Fin 6 → Bool) of 128 symbols, distinguishing satisfiable constraint graphs from those in which every labelling violates at least the proportion 2 ^ (-61) of the edges is NP-hard. The reduction is Dinur's gap construction Cslib.PCP.Encoded.gapGraph composed with the Cook–Levin reduction.

theorem Cslib.Complexity.GapTwoCSP_notMem_PromiseP {β : Type} {enc : β ↪ List Bool} (h : P enc ≠ NP enc) : GapTwoCSP (Bool × (Fin 6 → Bool)) (1 - 1 / 2 ^ 61) ∉ PromiseP (PCP.Encoded.Graph.encoding (Turing.MultiTapeTM.encPi (Turing.MultiTapeTM.encPi Turing.MultiTapeTM.encBool)))

Unless P = NP, no polynomial-time algorithm distinguishes satisfiable MAX-2CSP instances over 128 symbols from those of value at most 1 - 2 ^ (-61).