MAX-E3SAT: NP-hardness of approximation and the 7 / 8 random-assignment bound

GapExactThreeSAT s is the gap problem of MAX-3SAT (Cslib.Complexity.GapThreeSAT) restricted to formulas all of whose clauses have exactly three, not necessarily distinct, literals. Here "MAX-E3SAT" (Cslib.Complexity.GapExactThreeSAT) allows repeated literals in a clause, as Cslib.Complexity.ExactThreeSAT does. Its yes-instances are the members of Cslib.Complexity.ExactThreeSAT.

The gap of MAX-3SAT transfers unchanged: repeating a literal of every clause with one or two literals (Cslib.Complexity.toExactThreeSAT) changes neither the value of a clause nor the number of clauses, so every assignment falsifies the same clauses. An empty clause cannot be padded; a formula with one is unsatisfiable, so it is mapped to a fixed formula (Cslib.Complexity.GapExactThreeSAT.contradiction) in which every assignment falsifies one of two clauses, a no-instance for every soundness s ≥ 1 / 2. Hence distinguishing satisfiable formulas with clauses of exactly three literals from those in which every assignment satisfies at most the proportion 1 - 1 / (3 * 2 ^ 77) of the clauses is NP-hard (Cslib.Complexity.GapExactThreeSAT_npHard) Arora, Lund, Motwani, Sudan and Szegedy.

In the other direction, when the three variables of every clause are distinct (Cslib.Logic.PL.CNF.IsExactThreeDistinct), a uniform random assignment falsifies each clause with probability 1 / 8 (Cslib.Logic.PL.Clause.IsExactThreeDistinct.expect_eval_eq_false), so some assignment falsifies at most 1 / 8 of the clauses (Cslib.Logic.PL.CNF.IsExactThreeDistinct.unsatVal_le_one_eighth, developed in Complexity.Logics.Propositional.CNF.UnsatVal and re-exported here). Håstad showed that this 7 / 8 threshold is optimal [Has01]; that hardness result is not formalized here.

Main definitions

• Cslib.Complexity.GapExactThreeSAT: the gap problem of MAX-E3SAT with perfect completeness.
• Cslib.Complexity.GapExactThreeSAT.reduce: the reduction from GapThreeSAT.

Main results

• Cslib.Complexity.yes_GapExactThreeSAT, Cslib.Complexity.mem_no_GapExactThreeSAT: the instances of the gap problem.
• Cslib.Complexity.polyTimeReducible_GapThreeSAT_GapExactThreeSAT: MAX-3SAT reduces to MAX-E3SAT with the same gap, for every soundness 1 / 2 ≤ s < 1.
• Cslib.Complexity.GapExactThreeSAT_npHard: MAX-E3SAT, with repeated literals allowed, is NP-hard to approximate within 1 - 1 / (3 * 2 ^ 77).
• Cslib.Complexity.GapExactThreeSAT_notMem_PromiseP: unless P = NP, no polynomial-time algorithm separates its gap problem.

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
• J. Håstad, Some optimal inapproximability results

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

The gap problem of MAX-E3SAT with perfect completeness and soundness s: the gap problem of MAX-3SAT (GapThreeSAT) on the formulas all of whose clauses have exactly three literals, not necessarily distinct.

theorem Cslib.Complexity.yes_GapExactThreeSAT {s : ℝ} : (GapExactThreeSAT s).yes = ExactThreeSAT

The yes-instances of GapExactThreeSAT are the members of ExactThreeSAT.

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

For s < 1, the no-instances of GapExactThreeSAT are the formulas with clauses of exactly three literals in which every assignment falsifies at least the proportion 1 - s of the clauses.

def Cslib.Complexity.GapExactThreeSAT.contradiction : Logic.PL.CNF ℕ

A formula with two clauses of three literals, x₀ ∨ x₀ ∨ x₀ and ¬x₀ ∨ ¬x₀ ∨ ¬x₀: every assignment falsifies exactly one of them.

theorem Cslib.Complexity.GapExactThreeSAT.unsatVal_contradiction : contradiction.unsatVal = 1 / 2

Every assignment falsifies half of the clauses of contradiction.

def Cslib.Complexity.GapExactThreeSAT.reduce (φ : Logic.PL.CNF ℕ) : Logic.PL.CNF ℕ

The reduction from MAX-3SAT to MAX-E3SAT: a formula with an empty clause goes to contradiction; otherwise every clause with one or two literals is padded to three by repeating a literal (toExactThreeSAT).

theorem Cslib.Complexity.GapExactThreeSAT.computableTidilyInPolyTime_reduce : Turing.MultiTapeTM.ComputableTidilyInPolyTime reduce encCNF encCNF

The reduction is polynomial-time.

theorem Cslib.Complexity.polyTimeReducible_GapThreeSAT_GapExactThreeSAT {s : ℝ} (hs : 1 / 2 ≤ s) (hs1 : s < 1) : PromiseProblem.PolyTimeReducible encCNF encCNF (GapThreeSAT s) (GapExactThreeSAT s)

MAX-3SAT reduces to MAX-E3SAT with the same gap, repeated literals allowed, for every soundness 1 / 2 ≤ s < 1, by GapExactThreeSAT.reduce.

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

MAX-E3SAT is NP-hard to approximate [ALM+98]: distinguishing satisfiable formulas with exactly three, not necessarily distinct, 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.

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

Unless P = NP, no polynomial-time algorithm distinguishes satisfiable formulas with exactly three, not necessarily distinct, literals per clause from those in which every assignment satisfies at most the proportion 1 - 1 / (3 * 2 ^ 77) of the clauses.