Executable constraint graphs for 3-SAT

First-occurrence renaming bounds every variable index by the number of literal occurrences. Variable vertices use even numbers and clause vertices use odd numbers. Each clause contributes three ordered edges, including the self-loops for missing literal positions. Constraints are complete Boolean tables on the eight-symbol alphabet Fin 3 → Bool.

Main definitions

• Cslib.PCP.Encoded.Graph.ofCNF: construct a graph from a compactly numbered formula.
• Cslib.PCP.Encoded.Graph.ofCompactCNF: compact arbitrary variable names and construct the graph.

Main results

• Cslib.PCP.Encoded.Graph.isPolyTime_ofCompactCNF: charge renaming, enumeration, and truth tables.

References

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

def Cslib.PCP.Encoded.Graph.clauseHolds (κ : Logic.PL.Clause ℕ) (a : Fin 3 → Bool) : Bool

Check the first three literal positions against a clause label.

def Cslib.PCP.Encoded.Graph.cnfEdge (φ : Logic.PL.CNF ℕ) (p : ℕ × Fin 3) : Edge ((Fin 3 → Bool) → (Fin 3 → Bool) → Bool)

Construct one edge, computing its entire fixed-alphabet relation.

def Cslib.PCP.Encoded.Graph.ofCNF (variableCount : ℕ) (φ : Logic.PL.CNF ℕ) : Graph ((Fin 3 → Bool) → (Fin 3 → Bool) → Bool)

Construct three edges per clause. variableCount bounds compact variable names; it is used only for the declared vertex count, and correctness does not inspect a bound proof.

def Cslib.PCP.Encoded.Graph.ofCompactCNF {V : Type} [DecidableEq V] (φ : Logic.PL.CNF V) : Graph ((Fin 3 → Bool) → (Fin 3 → Bool) → Bool)

Compact the original variable names before producing unary graph indices.

theorem Cslib.PCP.Encoded.Graph.isPolyTime_clauseHolds : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (p : Logic.PL.Clause ℕ × (Fin 3 → Bool)) => clauseHolds p.1 p.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBool)) (Turing.MultiTapeTM.encPi Turing.MultiTapeTM.encBool)) Turing.MultiTapeTM.encBool

Checking a clause label includes lookup of the literals at its three positions.

theorem Cslib.PCP.Encoded.Graph.isPolyTime_cnfEdge : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (p : Logic.PL.CNF ℕ × ℕ × Fin 3) => cnfEdge p.1 p.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBool))) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encFinEnum (Fin 3)))) (Edge.encoding (Turing.MultiTapeTM.encPi (Turing.MultiTapeTM.encPi Turing.MultiTapeTM.encBool)))

The per-edge program charges clause lookup, endpoints, and all 64 entries of its relation.

theorem Cslib.PCP.Encoded.Graph.isPolyTime_ofCNF : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (p : ℕ × Logic.PL.CNF ℕ) => ofCNF p.1 p.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBool)))) (encoding (Turing.MultiTapeTM.encPi (Turing.MultiTapeTM.encPi Turing.MultiTapeTM.encBool)))

Constructing all edges and copying their constraints is polynomial-time.

theorem Cslib.PCP.Encoded.Graph.isPolyTime_ofCompactCNF {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) => ofCompactCNF (formula x)) input (encoding (Turing.MultiTapeTM.encPi (Turing.MultiTapeTM.encPi Turing.MultiTapeTM.encBool)))

The complete construction accepts any variable encoding and charges compact renaming.

def Cslib.PCP.Encoded.Graph.cnfVertexNumber {m : ℕ} : ℕ ⊕ Fin m → ℕ

Even numbers name variables; odd numbers name clause positions.

theorem Cslib.PCP.Encoded.Graph.cnfVertexNumber_injective (m : ℕ) : Function.Injective cnfVertexNumber

The numbering separates all variable vertices and clause vertices.

@[simp]

theorem Cslib.PCP.Encoded.Graph.length_edges_ofCNF (variableCount : ℕ) (φ : Logic.PL.CNF ℕ) : (ofCNF variableCount φ).edges.length = List.length φ * 3

Every clause contributes exactly three edges, including missing-position self-loops.

def Cslib.PCP.Encoded.Graph.ofCNFEnumeration (variableCount : ℕ) (φ : Logic.PL.CNF ℕ) : (ofCNF variableCount φ).edges.Enumeration fun (p : Fin (List.length φ) × Fin 3) => cnfEdge φ (↑p.1, p.2)

The concrete edge occurrences are indexed by clause and literal position.

theorem Cslib.PCP.Encoded.Graph.toGraph_ofCNF (variableCount : ℕ) (φ : Logic.PL.CNF ℕ) : (ofCNF variableCount φ).toGraph id = ((ConstraintGraph.ofCNF φ).map cnfVertexNumber).comap ⇑(ofCNFEnumeration variableCount φ).equiv

The executable graph is exactly the existing mathematical graph with concrete numbering.

theorem Cslib.PCP.Encoded.Graph.unsatVal_ofCNF (variableCount : ℕ) (φ : Logic.PL.CNF ℕ) : ((ofCNF variableCount φ).toGraph id).unsatVal = (ConstraintGraph.ofCNF φ).unsatVal

The exact graph interpretation retains the mathematical unsatisfied value.

theorem Cslib.PCP.Encoded.Graph.satisfiable_ofCNF_iff (variableCount : ℕ) (φ : Logic.PL.CNF ℕ) (h3 : ∀ c ∈ φ, List.length c ≤ 3) : ((ofCNF variableCount φ).toGraph id).Satisfiable ↔ φ.Satisfiable

For clauses of length at most three, the executable construction preserves satisfiability.

theorem Cslib.PCP.Encoded.Graph.wellFormed_ofCompactCNF {V : Type} [DecidableEq V] (φ : Logic.PL.CNF V) : (ofCompactCNF φ).WellFormed

The complete construction always produces well-formed numbered graphs.

@[simp]

theorem Cslib.PCP.Encoded.Graph.vertices_ofCompactCNF {V : Type} [DecidableEq V] (φ : Logic.PL.CNF V) : (ofCompactCNF φ).vertices = 2 * (φ.vars.length + List.length φ)

There are two declared vertex slots per literal occurrence or clause position.

@[simp]

theorem Cslib.PCP.Encoded.Graph.length_edges_ofCompactCNF {V : Type} [DecidableEq V] (φ : Logic.PL.CNF V) : (ofCompactCNF φ).edges.length = List.length φ * 3

Compaction does not change the three edges contributed by each original clause.

theorem Cslib.PCP.Encoded.Graph.satisfiable_ofCompactCNF_iff {V : Type} [DecidableEq V] (φ : Logic.PL.CNF V) (h3 : ∀ c ∈ φ, List.length c ≤ 3) : ((ofCompactCNF φ).toGraph id).Satisfiable ↔ φ.Satisfiable

The full construction accepts exactly the satisfiable formulas with at most three literals per clause, including repeated variables and missing literal positions.

theorem Cslib.PCP.Encoded.Graph.inv_edges_le_unsatVal_ofCompactCNF {V : Type} [DecidableEq V] (φ : Logic.PL.CNF V) (h3 : ∀ c ∈ φ, List.length c ≤ 3) (hφ : ¬φ.Satisfiable) : (↑(List.length φ) * 3)⁻¹ ≤ ((ofCompactCNF φ).toGraph id).unsatVal

An unsatisfiable input supplies the inverse-polynomial starting gap for amplification.