A PCP verifier as a CNF formula

SubsetNP reduces "some proof is accepted on every coin string" to "some bitstring is a witness": a table, laid out one block of Q answers per coin string, that is consistent and accepted everywhere. Both conditions are predicates on individual bits of that bitstring, so both are CNF clauses.

That is what this module builds. The formula's variables are the positions of the witness — a SAT assignment and a witness are the same object, since both read out of range as false — so the encoding needs no translation of models.

• Consistency contributes, for each pair of query slots that read the same proof position, the two clauses saying their variables agree.
• Acceptance contributes, for each coin string and each answer vector the verdict rejects, the clause blocking that vector.

With r coins and q queries the formula has 2^r q variables and O(4^r q^2 + 2^r 2^q) clauses — polynomial when r is logarithmic and q constant.

Main definitions

• Complexity.allVecs — the bit vectors of a given length
• Complexity.PCPVerifier.varIdx — the variable holding one answer
• Complexity.PCPVerifier.toCNF — the formula

Main results

• Complexity.mem_allVecs_iff — allVecs n is exactly the vectors of length n

Enumerating bit vectors

def Complexity.allVecs : ℕ → List (List Bool)

Every bit vector of a given length.

Equations

• Complexity.allVecs 0 = [[]]
• Complexity.allVecs n.succ = List.flatMap (fun (v : List Bool) => [false :: v, true :: v]) (Complexity.allVecs n)

theorem Complexity.mem_allVecs_iff (n : ℕ) (b : List Bool) : b ∈ allVecs n ↔ b.length = n

Variables

def Complexity.PCPVerifier.varIdx (t Q : ℕ) (ρ : Fin t → Bool) (i : ℕ) : ℕ

The variable holding the answer to query i on coin string ρ. The blocks sit a stride Q apart, exactly as SubsetNP.tableOf reads them.

Equations

• Complexity.PCPVerifier.varIdx t Q ρ i = Complexity.PCPVerifier.coinIndex ρ * Q + i

theorem Complexity.PCPVerifier.get_varIdx (V : PCPVerifier) (t Q : ℕ) (x w : List Bool) (ρ : Fin t → Bool) {i : ℕ} (hi : i < (V.positions x (BitString.toList ρ)).length) : (V.tableOf t Q x w ρ)[i]? = some (SAT.Assignment.get w (varIdx t Q ρ i))

The clauses

def Complexity.PCPVerifier.coinList (t : ℕ) : List (Fin t → Bool)

The coin strings, listed by index. Computable, unlike an enumeration drawn from Finset.univ, because the reduction has to be carried out by a machine.

Equations

• Complexity.PCPVerifier.coinList t = List.map Complexity.PCPVerifier.coinOfIndex (List.finRange (2 ^ t))

theorem Complexity.PCPVerifier.mem_coinList (t : ℕ) (ρ : Fin t → Bool) : ρ ∈ coinList t

def Complexity.PCPVerifier.consClauses (V : PCPVerifier) (t Q : ℕ) (x : List Bool) : List SAT.Clause

Two query slots reading the same proof position must get the same answer.

Equations

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

def Complexity.PCPVerifier.acceptClauses (V : PCPVerifier) (g : List Bool → Bool) (t Q : ℕ) (x : List Bool) : List SAT.Clause

For each coin string, a clause blocking every answer vector the verdict rejects. The verdict arrives as a Boolean function, which is the form a polynomial-time decision procedure takes.

Equations

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

def Complexity.PCPVerifier.toCNF (V : PCPVerifier) (g : List Bool → Bool) (t Q : ℕ) (x : List Bool) : SAT.CNF

The formula of a verifier on an input.

Equations

• V.toCNF g t Q x = V.consClauses t Q x ++ V.acceptClauses g t Q x

Semantics of the consistency clauses

theorem Complexity.PCPVerifier.eval_consClauses_iff (V : PCPVerifier) (t Q : ℕ) (x w : List Bool) : SAT.CNF.eval w (V.consClauses t Q x) = true ↔ ∀ (ρ ρ' : Fin t → Bool) (i i' : ℕ), i < (V.positions x (BitString.toList ρ)).length → i' < (V.positions x (BitString.toList ρ')).length → (V.positions x (BitString.toList ρ))[i]? = (V.positions x (BitString.toList ρ'))[i']? → SAT.Assignment.get w (varIdx t Q ρ i) = SAT.Assignment.get w (varIdx t Q ρ' i')

Semantics of the acceptance clauses

theorem Complexity.PCPVerifier.tableOf_getD (V : PCPVerifier) (t Q : ℕ) (x w : List Bool) (ρ : Fin t → Bool) {i : ℕ} (hi : i < (V.positions x (BitString.toList ρ)).length) : (V.tableOf t Q x w ρ).getD i false = SAT.Assignment.get w (varIdx t Q ρ i)

theorem Complexity.PCPVerifier.eval_acceptClauses_iff (V : PCPVerifier) {g : List Bool → Bool} (hg : ∀ (z : List Bool), g z = true ↔ z ∈ V.verdict) (t Q : ℕ) (x w : List Bool) : SAT.CNF.eval w (V.acceptClauses g t Q x) = true ↔ ∀ (ρ : Fin t → Bool), pair (pair x (BitString.toList ρ)) (V.tableOf t Q x w ρ) ∈ V.verdict

The formula is equivalent to the witness relation

theorem Complexity.PCPVerifier.eval_toCNF_iff (V : PCPVerifier) {g : List Bool → Bool} (hg : ∀ (z : List Bool), g z = true ↔ z ∈ V.verdict) (t Q : ℕ) (x w : List Bool) : SAT.CNF.eval w (V.toCNF g t Q x) = true ↔ V.Witness t Q x w

A satisfying assignment is exactly a witness.

theorem Complexity.PCPVerifier.satisfiable_toCNF_iff (V : PCPVerifier) {g : List Bool → Bool} (hg : ∀ (z : List Bool), g z = true ↔ z ∈ V.verdict) (t Q : ℕ) (x : List Bool) : (V.toCNF g t Q x).Satisfiable ↔ ∃ (w : List Bool), V.Witness t Q x w

The formula is satisfiable exactly when a proof exists.

The reduction, at the level of membership

def Complexity.PCPVerifier.budget (q : ℕ → ℕ) (x : List Bool) : ℕ

The query budget used for a given input: one more than the bound, so that the stride is positive even when the verifier makes no queries.

Equations

• Complexity.PCPVerifier.budget q x = q x.length + 1

theorem Complexity.PCPVerifier.budget_pos (q : ℕ → ℕ) (x : List Bool) : 0 < budget q x

theorem Complexity.PCPVerifier.length_positions_le_budget (V : PCPVerifier) {q : ℕ → ℕ} (hq : V.QueryBounded q) (x r : List Bool) : (V.positions x r).length ≤ budget q x

theorem Complexity.PCPVerifier.satisfiable_toCNF_iff_exists_proof (V : PCPVerifier) {g : List Bool → Bool} (hg : ∀ (z : List Bool), g z = true ↔ z ∈ V.verdict) {q : ℕ → ℕ} (hq : V.QueryBounded q) (t : ℕ) (x : List Bool) : (V.toCNF g t (budget q x) x).Satisfiable ↔ ∃ (π : List Bool), ∀ (ρ : Fin t → Bool), V.Accepts x π (BitString.toList ρ)

The encoded formula tracks membership. For an input on which the verifier is either certainly accepted or accepted with probability at most a half, the formula is satisfiable exactly when some proof is always accepted.

theorem Complexity.PCPVerifier.mem_language_toCNF_iff (V : PCPVerifier) {L : Language} {g : List Bool → Bool} (hg : ∀ (z : List Bool), g z = true ↔ z ∈ V.verdict) {q : ℕ → ℕ} {t : ℕ} (hq : V.QueryBounded q) (hcomp : ∀ x ∈ L, ∃ (π : List Bool), eventProb (V.acceptEvent t x π) = 1) (hsound : ∀ x ∉ L, ∀ (π : List Bool), eventProb (V.acceptEvent t x π) ≤ 1 / 2) (x : List Bool) : x ∈ L ↔ (V.toCNF g t (budget q x) x).encode ∈ SAT.language

The reduction is correct. If L is decided by the verifier with t coins in the sense of PCP, then membership in L is membership of the encoded formula in SAT.