From 3CNF-SAT to binary constraint graphs

The standard reduction turning a 3CNF formula into a constraint graph over the alphabet Fin 3 → Bool, together with its correctness proof. This is the entry point of Dinur's proof of the PCP theorem: it produces the constraint graph whose unsatisfiability value the amplification step then boosts.

The construction

Given φ : CNF, the graph toGraph φ has

• one variable vertex for each variable index 0 … φ.maxVar, and
• one clause vertex for each clause of φ, numbered (φ.maxVar + 1) + j;
• one edge for each (clause, position) pair, so 3 * φ.length edges in all.

A variable vertex is meant to carry the value of its variable in bit 0 of its label; a clause vertex is meant to carry the values of the three variables its clause mentions, one per coordinate. The edge for clause j and position p checks both that the clause vertex's triple satisfies clause j and that its p-th coordinate agrees with the p-th variable vertex — the usual consistency-plus-satisfaction pair of constraints.

Main definitions

• litOf — a total lookup of the literal at a given clause and position
• numVerts, numEdges, varVertex, clauseVertex, edgeClause, edgePos
• clauseSat — whether a triple of bits satisfies a clause
• toGraph — the constraint graph produced by the reduction
• vertexLabel, mkAssign — the two translations between assignments

Main results

• numVerts_toGraph, numEdges_toGraph — the size of the produced graph
• satisfiable_toGraph_iff — correctness of the reduction on 3CNF inputs

Indexing helpers

def Complexity.ThreeSATCSP.litOf (φ : SAT.CNF) (j : ℕ) (p : Fin 3) : SAT.Lit

The literal at position p of clause j of φ, defaulting to the positive literal on variable 0 when either index is out of range. Totality keeps the reduction free of dependent-index bookkeeping.

Equations

• Complexity.ThreeSATCSP.litOf φ j p = List.getD (φ[j]?.getD []) ↑p { sign := false, var := 0 }

def Complexity.ThreeSATCSP.numVerts (φ : SAT.CNF) : ℕ

The number of vertices of the constraint graph of φ: one per variable index 0 … φ.maxVar, then one per clause.

Equations

• Complexity.ThreeSATCSP.numVerts φ = φ.maxVar + 1 + List.length φ

def Complexity.ThreeSATCSP.numEdges (φ : SAT.CNF) : ℕ

The number of edges of the constraint graph of φ: three per clause.

Equations

• Complexity.ThreeSATCSP.numEdges φ = 3 * List.length φ

theorem Complexity.ThreeSATCSP.numVerts_pos (φ : SAT.CNF) : 0 < numVerts φ

The constraint graph of φ always has at least one vertex, namely the variable vertex 0.

def Complexity.ThreeSATCSP.varVertex (φ : SAT.CNF) (v : ℕ) : Fin (numVerts φ)

The vertex carrying the value of variable v; out-of-range indices are folded onto vertex 0.

Equations

• Complexity.ThreeSATCSP.varVertex φ v = if h : v < Complexity.ThreeSATCSP.numVerts φ then ⟨v, h⟩ else ⟨0, ⋯⟩

def Complexity.ThreeSATCSP.clauseVertex (φ : SAT.CNF) (j : ℕ) : Fin (numVerts φ)

The vertex carrying the claimed values of the variables of clause j; out-of-range indices are folded onto vertex 0.

Equations

• Complexity.ThreeSATCSP.clauseVertex φ j = if h : φ.maxVar + 1 + j < Complexity.ThreeSATCSP.numVerts φ then ⟨φ.maxVar + 1 + j, h⟩ else ⟨0, ⋯⟩

def Complexity.ThreeSATCSP.edgeClause (e : ℕ) : ℕ

The clause that edge number e belongs to.

Equations

• Complexity.ThreeSATCSP.edgeClause e = e / 3

def Complexity.ThreeSATCSP.edgePos (e : ℕ) : Fin 3

The position inside its clause that edge number e checks.

Equations

• Complexity.ThreeSATCSP.edgePos e = ⟨e % 3, ⋯⟩

def Complexity.ThreeSATCSP.clauseSat (φ : SAT.CNF) (j : ℕ) (cl : Fin 3 → Bool) : Bool

Whether the triple cl of claimed variable values satisfies clause j: some position's claimed value matches that literal's sign.

Equations

• Complexity.ThreeSATCSP.clauseSat φ j cl = decide (∃ (q : Fin 3), cl q = (Complexity.ThreeSATCSP.litOf φ j q).sign)

theorem Complexity.ThreeSATCSP.clauseSat_eq_true_iff {φ : SAT.CNF} {j : ℕ} {cl : Fin 3 → Bool} : clauseSat φ j cl = true ↔ ∃ (q : Fin 3), cl q = (litOf φ j q).sign

clauseSat reflects the existential it decides.

The reduction

def Complexity.ThreeSATCSP.toGraph (φ : SAT.CNF) : ConstraintGraph (Fin 3 → Bool)

The constraint graph of a 3CNF formula φ. Variable vertices come first, clause vertices after them; edge e links clause vertex edgeClause e to the variable vertex of the literal at position edgePos e of that clause, and its constraint demands both that the clause vertex's triple satisfies the clause and that it agrees with the variable vertex on bit 0.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.ThreeSATCSP.numEdges_toGraph (φ : SAT.CNF) : (toGraph φ).numEdges = 3 * List.length φ

The reduction produces 3 * φ.length edges.

theorem Complexity.ThreeSATCSP.numVerts_toGraph (φ : SAT.CNF) : (toGraph φ).numVerts = φ.maxVar + 1 + List.length φ

The reduction produces (φ.maxVar + 1) + φ.length vertices.

Basic facts about the indexing helpers

theorem Complexity.ThreeSATCSP.varVertex_val {φ : SAT.CNF} {v : ℕ} (hv : v ≤ φ.maxVar) : ↑(varVertex φ v) = v

A variable vertex within range keeps its index.

theorem Complexity.ThreeSATCSP.clauseVertex_val {φ : SAT.CNF} {j : ℕ} (hj : j < List.length φ) : ↑(clauseVertex φ j) = φ.maxVar + 1 + j

A clause vertex of an existing clause sits at index (φ.maxVar + 1) + j.

theorem Complexity.ThreeSATCSP.litOf_eq {φ : SAT.CNF} {j : ℕ} {c : SAT.Clause} (hc : φ[j]? = some c) {p : Fin 3} (hp : ↑p < List.length c) : litOf φ j p = c[↑p]

litOf really reads the list entry it is meant to read.

theorem Complexity.ThreeSATCSP.litOf_mem {φ : SAT.CNF} {j : ℕ} {c : SAT.Clause} (hc : φ[j]? = some c) (hlen : List.length c = 3) (p : Fin 3) : litOf φ j p ∈ c

Every literal produced by litOf at an existing clause really occurs in that clause, provided the clause has three literals.

theorem Complexity.ThreeSATCSP.edgeClause_lt {φ : SAT.CNF} (e : Fin (toGraph φ).numEdges) : edgeClause ↑e < List.length φ

Every edge belongs to a clause that exists.

theorem Complexity.ThreeSATCSP.exists_edge {φ : SAT.CNF} {j : ℕ} (hj : j < List.length φ) (q : Fin 3) : ∃ (e : Fin (toGraph φ).numEdges), edgeClause ↑e = j ∧ edgePos ↑e = q

Every (clause, position) pair is realized by an edge.

theorem Complexity.ThreeSATCSP.satisfies_iff {φ : SAT.CNF} {a : (toGraph φ).Assignment} (e : Fin (toGraph φ).numEdges) : (toGraph φ).Satisfies a e ↔ clauseSat φ (edgeClause ↑e) (a (clauseVertex φ (edgeClause ↑e))) = true ∧ a (clauseVertex φ (edgeClause ↑e)) (edgePos ↑e) = a (varVertex φ (litOf φ (edgeClause ↑e) (edgePos ↑e)).var) 0

The edge constraint of toGraph, spelled out.

theorem Complexity.ThreeSATCSP.var_litOf_le_maxVar {φ : SAT.CNF} (h3 : φ.Is3CNF) {j : ℕ} (hj : j < List.length φ) (p : Fin 3) : (litOf φ j p).var ≤ φ.maxVar

Every literal of a 3CNF formula mentions a variable at most φ.maxVar.

Translating assignments

def Complexity.ThreeSATCSP.vertexLabel (φ : SAT.CNF) (α : SAT.Assignment) (w : ℕ) : Fin 3 → Bool

The label the graph assignment induced by a CNF assignment α puts on vertex number w: a variable vertex gets the constant value of its variable, a clause vertex gets the values of the three variables its clause mentions.

Equations

• Complexity.ThreeSATCSP.vertexLabel φ α w = if w < φ.maxVar + 1 then fun (x : Fin 3) => α.get w else fun (q : Fin 3) => α.get (Complexity.ThreeSATCSP.litOf φ (w - (φ.maxVar + 1)) q).var

theorem Complexity.ThreeSATCSP.vertexLabel_var {φ : SAT.CNF} {α : SAT.Assignment} {v : ℕ} (hv : v ≤ φ.maxVar) : vertexLabel φ α v = fun (x : Fin 3) => α.get v

The label of a variable vertex.

theorem Complexity.ThreeSATCSP.vertexLabel_clause {φ : SAT.CNF} {α : SAT.Assignment} {j : ℕ} : vertexLabel φ α (φ.maxVar + 1 + j) = fun (q : Fin 3) => α.get (litOf φ j q).var

The label of a clause vertex.

def Complexity.ThreeSATCSP.mkAssign (φ : SAT.CNF) (a : (toGraph φ).Assignment) : SAT.Assignment

The CNF assignment read off from a graph assignment: variable v takes the value of bit 0 of the label of its variable vertex.

Equations

• Complexity.ThreeSATCSP.mkAssign φ a = List.map (fun (v : ℕ) => a (Complexity.ThreeSATCSP.varVertex φ v) 0) (List.range (φ.maxVar + 1))

theorem Complexity.ThreeSATCSP.get_mkAssign {φ : SAT.CNF} {a : (toGraph φ).Assignment} {v : ℕ} (hv : v ≤ φ.maxVar) : (mkAssign φ a).get v = a (varVertex φ v) 0

mkAssign reads back the label bit it was built from.

Correctness

theorem Complexity.ThreeSATCSP.satisfiable_toGraph_iff {φ : SAT.CNF} (h3 : φ.Is3CNF) : (toGraph φ).Satisfiable ↔ φ.Satisfiable

Correctness of the reduction. For a 3CNF formula, the constraint graph produced by toGraph is satisfiable exactly when the formula is.