MAX-3SAT is NP-hard to approximate

The unsatisfiability value CNF.unsatVal φ of a formula is the least proportion of its clauses that an assignment falsifies (Complexity.Logics.Propositional.CNF.UnsatVal), and 1 - CNF.unsatVal φ is its value as an instance of MAX-SAT. GapThreeSAT s is the gap problem of MAX-3SAT with perfect completeness: its instances are formulas whose clauses have at most three literals, its yes-instances are the satisfiable ones (ThreeSAT) and its no-instances those in which every assignment satisfies at most the proportion s of the clauses.

A binary constraint on labels written in k bits is a conjunction of clauses of width 2 k, one excluding each pair of labels the constraint forbids Arora and Barak, Chapter 11. Graph.toCNF writes a constraint graph this way, and splitting the clauses to width three (Cslib.Complexity.toThreeSAT) gives a gap-preserving reduction from MAX-2CSP to MAX-3SAT: every violated edge leaves a falsified clause, and each edge produces at most |α| ^ 2 * (2 k - 2) clauses. From the gap of Dinur's construction (Cslib.Complexity.GapTwoCSP_npHard) over 128 = 2 ^ 7 symbols, MAX-3SAT is NP-hard to approximate within 1 - 1 / (3 * 2 ^ 77): the loss is the factor 128 ^ 2 * 12 = 3 * 2 ^ 16. That MAX-3SAT is NP-hard to approximate within some constant is due to Arora, Lund, Motwani, Sudan and Szegedy [ALM+98].

Main definitions

• Cslib.PCP.Encoded.Graph.toCNF: a constraint graph written as a formula.
• Cslib.Complexity.GapThreeSAT: the gap problem of MAX-3SAT with perfect completeness.

Main results

• Cslib.PCP.Encoded.Graph.div_le_unsatVal_toThreeSAT_toCNF: the gap-preserving bound.
• Cslib.Complexity.GapThreeSAT_npHard: distinguishing satisfiable 3CNF formulas from those in which every assignment satisfies at most the proportion 1 - 1 / (3 * 2 ^ 77) of the clauses is NP-hard.

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
• I. Dinur, The PCP theorem by gap amplification

Constraint graphs as formulas

def Cslib.PCP.Encoded.Graph.excludeClause {α : Type} {k : ℕ} (e : α ≃ (Fin k → Bool)) (u v : ℕ) (p : α × α) : Logic.PL.Clause ℕ

The clause excluding the label p.1 at the vertex u and the label p.2 at v. The label of a vertex u is written in k bits, in the variables Nat.pair u i for i < k, along e.

def Cslib.PCP.Encoded.Graph.edgeCNF {α : Type} {k : ℕ} (e : α ≃ (Fin k → Bool)) (pairs : List (α × α)) (d : Edge (α → α → Bool)) : Logic.PL.CNF ℕ

One clause for each pair in the list pairs violating the constraint of the edge.

def Cslib.PCP.Encoded.Graph.toCNF {α : Type} {k : ℕ} (e : α ≃ (Fin k → Bool)) (pairs : List (α × α)) (g : Graph (α → α → Bool)) : Logic.PL.CNF ℕ

A constraint graph written as a formula: one clause of width 2 k for each edge and each pair of labels, listed in pairs, that its constraint forbids.

def Cslib.PCP.Encoded.Graph.readLabel {α : Type} {k : ℕ} (e : α ≃ (Fin k → Bool)) (τ : ℕ → Bool) (u : ℕ) : α

The label of the vertex u written by an assignment.

theorem Cslib.PCP.Encoded.Graph.eval_excludeClause_eq_true_iff {α : Type} {k : ℕ} (e : α ≃ (Fin k → Bool)) (τ : ℕ → Bool) (u v : ℕ) (p : α × α) : Logic.PL.Clause.eval τ (excludeClause e u v p) = true ↔ readLabel e τ u ≠ p.1 ∨ readLabel e τ v ≠ p.2

An assignment satisfies excludeClause e u v p exactly when it does not write the labels p at u and v.

theorem Cslib.PCP.Encoded.Graph.satisfiable_toCNF {α : Type} {k : ℕ} (e : α ≃ (Fin k → Bool)) (pairs : List (α × α)) {g : Graph (α → α → Bool)} (h : (g.toGraph id).Satisfiable) : (toCNF e pairs g).Satisfiable

A labelling satisfying the constraint graph, written in bits, satisfies its formula.

theorem Cslib.PCP.Encoded.Graph.div_le_unsatVal_toThreeSAT_toCNF {α : Type} {k : ℕ} (e : α ≃ (Fin k → Bool)) (pairs : List (α × α)) (hpairs : ∀ (p : α × α), p ∈ pairs) (g : Graph (α → α → Bool)) : (g.toGraph id).unsatVal / ↑(pairs.length * max 1 (2 * k - 2)) ≤ (Complexity.toThreeSAT (toCNF e pairs g)).unsatVal

MAX-2CSP reduces to MAX-3SAT, preserving the gap: if every labelling of the constraint graph violates the proportion ε of its edges, every assignment falsifies the proportion ε / (pairs.length * max 1 (2 k - 2)) of the clauses of its formula, split to width three. Labels are written in k bits, along e, and pairs lists every pair of labels.

Polynomial time

theorem Cslib.PCP.Encoded.Graph.isPolyTime_toCNF {α : Type} {k : ℕ} (e : α ≃ (Fin k → Bool)) (pairs : List (α × α)) [Fintype α] : Turing.MultiTapeTM.ComputableTidilyInPolyTime (toCNF e pairs) (encoding (Turing.MultiTapeTM.encPi (Turing.MultiTapeTM.encPi Turing.MultiTapeTM.encBool))) Complexity.encCNF

Writing a constraint graph as a formula is polynomial-time: for each edge, every pair in the fixed list pairs is tested against its constraint table.

noncomputable def Cslib.Complexity.GapThreeSAT (s : ℝ) : PromiseProblem (Logic.PL.CNF ℕ)

The gap problem of MAX-3SAT with perfect completeness and soundness s. The instances are the formulas whose clauses have at most three literals; their value is the largest proportion of the clauses, counted with multiplicity, that an assignment satisfies. The yes-instances have value one, the no-instances value at most s.

theorem Cslib.Complexity.yes_GapThreeSAT {s : ℝ} : (GapThreeSAT s).yes = ThreeSAT

The yes-instances of GapThreeSAT are the members of ThreeSAT.

theorem Cslib.Complexity.mem_no_GapThreeSAT {s : ℝ} {φ : Logic.PL.CNF ℕ} (hs : s < 1) : φ ∈ (GapThreeSAT s).no ↔ (∀ c ∈ φ, List.length c ≤ 3) ∧ 1 - s ≤ φ.unsatVal

For s < 1, the no-instances of GapThreeSAT are the formulas of width at most three in which every assignment falsifies at least the proportion 1 - s of the clauses.

theorem Cslib.Complexity.polyTimeReducible_GapTwoCSP_GapThreeSAT {s : ℝ} {α : Type} [Fintype α] {k : ℕ} (e : α ≃ (Fin k → Bool)) (hs : s < 1) : PromiseProblem.PolyTimeReducible (PCP.Encoded.Graph.encoding (Turing.MultiTapeTM.encPi (Turing.MultiTapeTM.encPi Turing.MultiTapeTM.encBool))) encCNF (GapTwoCSP α s) (GapThreeSAT (1 - (1 - s) / ↑(Fintype.card α ^ 2 * max 1 (2 * k - 2))))

MAX-2CSP reduces to MAX-3SAT: for labels written in k bits along an equivalence e, the gap problem of MAX-2CSP with soundness s < 1 reduces in polynomial time to that of MAX-3SAT with soundness 1 - (1 - s) / (|α| ^ 2 * (2 k - 2)), through Cslib.PCP.Encoded.Graph.toCNF and splitting to width three.

theorem Cslib.Complexity.GapThreeSAT_npHard : PromiseProblem.NPHard encCNF (GapThreeSAT (1 - 1 / (3 * 2 ^ 77)))

MAX-3SAT is NP-hard to approximate [ALM+98], Arora and Barak, Chapter 11: distinguishing satisfiable formulas with at most three literals per clause from those in which every assignment satisfies at most the proportion 1 - 1 / (3 * 2 ^ 77) of the clauses is NP-hard. The constant comes from Dinur's gap 2 ^ (-61) over 128 = 2 ^ 7 symbols (GapTwoCSP_npHard), divided by 128 ^ 2 * 12 = 3 * 2 ^ 16 clauses per edge.

theorem Cslib.Complexity.GapThreeSAT_notMem_PromiseP {β : Type} {enc : β ↪ List Bool} (h : P enc ≠ NP enc) : GapThreeSAT (1 - 1 / (3 * 2 ^ 77)) ∉ PromiseP encCNF

Unless P = NP, no polynomial-time algorithm distinguishes satisfiable 3CNF formulas from those in which every assignment satisfies at most the proportion 1 - 1 / (3 * 2 ^ 77) of the clauses.