Documentation

Complexity.Computability.PCP.Encoded.GapTheorem

An executable constant-gap reduction from SAT #

Split clauses to width three, compact variable names, construct the initial constraint graph, normalize its alphabet by composition, and apply logarithmically many arithmetic amplification rounds. Every stage is a functional program. The expander and all finite enumerations are fixed constructively; the enormous fixed parameters make this an asymptotic construction.

The reduction accepts arbitrary CNF formulas and preserves satisfiability. Unsatisfiable inputs produce graphs above the fixed positive gap, with all endpoints in the declared vertex range.

Main definitions #

Main results #

References #

source
@[reducible, inline]
abbrev Cslib.PCP.Encoded.GapAlphabet :
Type

The fixed output alphabet of the selected composition and arithmetic amplification pipeline.

Instances For
    source
    def Cslib.PCP.Encoded.gapGraph {V : Type} [DecidableEq V] (φ : Logic.PL.CNF V) :
    Graph (GapAlphabet → GapAlphabet → Bool)

    Split, compact, normalize, and amplify a CNF formula using the concrete arithmetic family.

    Instances For
      source
      theorem Cslib.PCP.Encoded.isPolyTime_gapGraph {V Input : Type} [DecidableEq V] {enc : V ↪ List Bool} {input : Input ↪ List Bool} {formula : Input → Logic.PL.CNF V} (hformula : Turing.MultiTapeTM.ComputableTidilyInPolyTime formula input (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBool)))) :
      Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (x : Input) => gapGraph (formula x)) input (Graph.encoding (Turing.MultiTapeTM.encPi (Turing.MultiTapeTM.encPi Turing.MultiTapeTM.encBool)))

      The whole reduction is polynomial-time in any efficiently computed input formula. Variable names retain their supplied encoding until compaction, including sparse or repeated names.

      source
      theorem Cslib.PCP.Encoded.wellFormed_gapGraph {V : Type} [DecidableEq V] (φ : Logic.PL.CNF V) :
      (gapGraph φ).WellFormed

      Every output edge has endpoints in the declared finite vertex range.

      source
      theorem Cslib.PCP.Encoded.satisfiable_gapGraph_iff {V : Type} [DecidableEq V] (φ : Logic.PL.CNF V) :
      ((gapGraph φ).toGraph id).Satisfiable ↔ φ.Satisfiable

      The complete construction preserves satisfiability for arbitrary clause lengths.

      source
      theorem Cslib.PCP.Encoded.gap_le_unsatVal_gapGraph {V : Type} [DecidableEq V] (φ : Logic.PL.CNF V) (hφ : ¬φ.Satisfiable) :
      ConstraintGraph.Amplification.Arithmetic.gap ≤ ((gapGraph φ).toGraph id).unsatVal

      Every unsatisfiable formula produces a graph above the fixed arithmetic gap.