From 3-SAT to constraint graphs

The standard reduction from 3-SAT to the satisfiability of constraint graphs over a constant alphabet, with binary constraints Arora and Barak, Chapter 22. It can serve as the starting point of Dinur's proof of the PCP theorem, which starts instead from graph 3-colouring Dinur, Proposition 2.1 and Corollary 4.2: it produces a constraint graph whose value is at least a constant fraction of the proportion of clauses that every assignment falsifies, and the rest of the proof amplifies that value.

The constraint graph ConstraintGraph.ofCNF φ of a formula φ with m clauses has

• a variable vertex inl x for each variable x, meant to carry the value of x as the first bit of its label, and
• a clause vertex inr j for each clause, meant to carry the values of the variables at the first three positions of clause j, one bit per position;
• three edges (j, q) per clause, so 3 m in all. The edge (j, q) goes from clause vertex j to the variable vertex of the literal at position q of clause j, or back to clause vertex j when the clause has no such position. Its constraint asks that the label of the clause vertex satisfy clause j, and that its bit q agree with the first bit of the label of the variable vertex.

The alphabet is Fin 3 → Bool, with eight symbols. If an assignment of the variables falsifies k clauses, labelling the vertices by it violates at most 3 k edges (card_unsatEdges_cnfLabelling_le); conversely, from a labelling violating k' edges, reading off the variables from the variable vertices gives an assignment falsifying at most k' clauses (countUnsat_cnfAssignment_le_card_unsatEdges), since a clause is falsified only if one of its three edges is violated. The second direction holds for every formula; the first needs the clauses to have at most three literals.

Main definitions

• Cslib.PCP.ConstraintGraph.ofCNF: the constraint graph of a formula.
• Cslib.PCP.ConstraintGraph.cnfLabelling, Cslib.PCP.ConstraintGraph.cnfAssignment: the translations between assignments of the variables and labellings of the vertices.

Main results

• Cslib.PCP.ConstraintGraph.satisfiable_ofCNF_iff: the constraint graph of a formula whose clauses have at most three literals is satisfiable exactly when the formula is.
• Cslib.PCP.ConstraintGraph.le_unsatVal_ofCNF: if every assignment falsifies a proportion at least ε of the clauses, the value of the constraint graph is at least ε / 3.
• Cslib.PCP.ConstraintGraph.unsatVal_ofCNF_le: conversely, its value is at most the proportion of clauses that any assignment falsifies.

References

• S. Arora, B. Barak, Computational Complexity: A Modern Approach
• I. Dinur, The PCP theorem by gap amplification
• I. Dinur, The PCP theorem by gap amplification, ECCC TR05-046, revision 1

def Cslib.PCP.ConstraintGraph.ClauseHolds {V : Type u_1} (κ : Logic.PL.Clause V) (a : Fin 3 → Bool) : Prop

The values a q of the variables at the first three positions q of the clause κ satisfy κ: some position q of κ holds a literal (x, b) with a q = b.

def Cslib.PCP.ConstraintGraph.ofCNF {V : Type u_1} (φ : Logic.PL.CNF V) : ConstraintGraph (V ⊕ Fin (List.length φ)) (Fin (List.length φ) × Fin 3) (Fin 3 → Bool)

The constraint graph of a formula φ Arora and Barak, Chapter 22, over the alphabet Fin 3 → Bool. Its vertices are the variables (inl x) and the clauses (inr j); the edge (j, q) goes from clause j to the variable of the literal at position q of clause j, or back to clause j when there is no such literal. Its constraint asks that the label of clause j, read as the values of the variables at its first three positions, satisfy it, and that its bit q agree with the first bit of the label of the variable.

def Cslib.PCP.ConstraintGraph.cnfLabelling {V : Type u_1} (φ : Logic.PL.CNF V) (τ : V → Bool) : V ⊕ Fin (List.length φ) → Fin 3 → Bool

The labelling of the vertices of ofCNF φ by an assignment τ of the variables: a variable is labelled by its value, a clause by the values of the variables at its first three positions.

def Cslib.PCP.ConstraintGraph.cnfAssignment {V : Type u_1} {φ : Logic.PL.CNF V} (A : V ⊕ Fin (List.length φ) → Fin 3 → Bool) (x : V) : Bool

The assignment of the variables read off from a labelling of the vertices of ofCNF φ: the value of a variable is the first bit of its label.

theorem Cslib.PCP.ConstraintGraph.countUnsat_cnfAssignment_le_card_unsatEdges {V : Type u_1} {φ : Logic.PL.CNF V} (A : V ⊕ Fin (List.length φ) → Fin 3 → Bool) : Logic.PL.CNF.countUnsat (cnfAssignment A) φ ≤ ((ofCNF φ).unsatEdges A).card

Soundness, counted: the assignment read off from a labelling falsifies at most as many clauses as the labelling violates edges.

theorem Cslib.PCP.ConstraintGraph.card_unsatEdges_cnfLabelling_le {V : Type u_1} (φ : Logic.PL.CNF V) (h3 : ∀ c ∈ φ, List.length c ≤ 3) (τ : V → Bool) : ((ofCNF φ).unsatEdges (cnfLabelling φ τ)).card ≤ 3 * Logic.PL.CNF.countUnsat τ φ

Completeness, counted: if the clauses of φ have at most three literals, the labelling by an assignment violates at most three edges per clause the assignment falsifies.

theorem Cslib.PCP.ConstraintGraph.satisfiable_ofCNF_iff {V : Type u_1} (φ : Logic.PL.CNF V) (h3 : ∀ c ∈ φ, List.length c ≤ 3) : (ofCNF φ).Satisfiable ↔ φ.Satisfiable

The reduction preserves satisfiability: the constraint graph of a formula whose clauses have at most three literals is satisfiable exactly when the formula is.

theorem Cslib.PCP.ConstraintGraph.le_unsatVal_ofCNF {V : Type u_1} (φ : Logic.PL.CNF V) {ε : ℝ} (h : ∀ (τ : V → Bool), ε ≤ ↑(Logic.PL.CNF.countUnsat τ φ) / ↑(List.length φ)) : ε / 3 ≤ (ofCNF φ).unsatVal

The gap is preserved: if every assignment falsifies a proportion at least ε of the clauses of φ, the value of its constraint graph is at least ε / 3.

theorem Cslib.PCP.ConstraintGraph.unsatVal_ofCNF_le {V : Type u_1} (φ : Logic.PL.CNF V) (h3 : ∀ c ∈ φ, List.length c ≤ 3) (τ : V → Bool) : (ofCNF φ).unsatVal ≤ ↑(Logic.PL.CNF.countUnsat τ φ) / ↑(List.length φ)

Conversely, if the clauses of φ have at most three literals, the value of its constraint graph is at most the proportion of clauses that any assignment falsifies.