Documentation

Complexitylib.Classes.PCP.Internal.GapTheorem

Dinur's gap theorem for 3-SAT #

The mathematical conclusion of the development. Every 3CNF formula is turned into a constraint graph over a fixed constant-size alphabet, of size polynomial in the formula, which is satisfiable when the formula is and whose unsatisfiability value is at least a universal constant when it is not.

Three ingredients meet: the reduction of ThreeSATCSP carried across alphabets by GapReduction, the explicit expander family algFamily of FamilyFin (a numbered tower over a constant-size base picked once by Classical.choose exists_finBase), and the amplifier of Dinur, whose dichotomy supplies the gap after logarithmically many rounds.

This module states the gap theorem as a reduction in the mathematical sense: gapGraph is a noncomputable definition and no running time is claimed here. The polynomial-time implementation is elsewhere: exists_pcp_of_mem_NP in Complexitylib.Classes.PCP.Internal.AlgPCP runs the same amplifier over the same tower (Dinur.amplifier (algF.toFamily algHd), with algF = algBase) and packages it as a PCPVerifier with an FP query function and a P verdict.

Main definitions #

Main results #

source
noncomputable def Complexity.dinurAmp :
Amplifier DinurAlpha

Dinur's amplifier, with the expander family supplied.

Equations
Instances For
    source
    def Complexity.gapRounds (φ : SAT.CNF) :
    ℕ

    How many rounds of amplification a formula needs: enough that the doubling of the unsatisfiability value reaches the threshold, which is the bit length of the edge count.

    Equations
    Instances For
      source
      theorem Complexity.numEdges_baseCSP_le_pow_rounds (φ : SAT.CNF) :
      (baseCSP φ).numEdges ≤ 2 ^ gapRounds φ
      source
      noncomputable def Complexity.gapGraph (φ : SAT.CNF) :
      ConstraintGraph DinurAlpha

      The gap graph of a formula: logarithmically many rounds of amplification applied to its constraint graph.

      Equations
      Instances For
        source
        theorem Complexity.satisfiable_gapGraph {φ : SAT.CNF} (h3 : φ.Is3CNF) (h : φ.Satisfiable) :
        (gapGraph φ).Satisfiable

        Completeness.

        source
        theorem Complexity.gap_le_unsatVal_gapGraph {φ : SAT.CNF} (h3 : φ.Is3CNF) (h : ¬φ.Satisfiable) :
        dinurAmp.gap ≤ (gapGraph φ).unsatVal

        Soundness, with a gap that does not depend on the formula.

        source
        theorem Complexity.dinurAmp_gap_pos :
        0 < dinurAmp.gap

        The gap is a positive constant.

        source
        theorem Complexity.dinurAmp_gap_le_one :
        dinurAmp.gap ≤ 1

        The gap is at most one, as any unsatisfiability value is.

        source
        theorem Complexity.two_pow_log_succ_le (n : ℕ) :
        2 ^ (Nat.log 2 n + 1) ≤ 2 * n + 2

        A bit length costs at most a doubling.

        source
        theorem Complexity.numEdges_gapGraph_le (φ : SAT.CNF) :
        (gapGraph φ).numEdges ≤ (2 * (3 * List.length φ) + 2) ^ (Nat.log 2 dinurAmp.edgeFactor + 1) * (3 * List.length φ)

        The size bound: a constant factor per round, and logarithmically many rounds, so polynomially many edges.