Guess and verify, for any language

The guess-and-verify machine built for SAT is not in fact specific to SAT: it takes an arbitrary deterministic verifier M, guesses a string of length at most |x| + 1, pairs it with the input and runs M on the result. Every structural theorem about it in SAT/Internal/GuessVerify is already stated for an arbitrary language L; only the final assembly mentions SAT.

This module performs that assembly generically. The result is the guess-and-verify bridge NP.WitnessNTMConstruction was meant to provide, restricted to witnesses of linear length — which costs nothing, since padding the input makes any polynomial witness bound linear.

Main results

• Complexity.mem_NP_of_linear_witness — a language with a polynomial-time verifier and witnesses of length at most |x| + 1 is in NP
• Complexity.mem_NP_of_poly_witness — the same for any polynomial witness bound, by padding the input until the bound is linear

theorem Complexity.guessVerify_decidesInTime {k : ℕ} (M : TM k) {L L₀ : Language} {f : ℕ → ℕ} (hM : M.DecidesInTime L₀ f) (hchar : ∀ (x : List Bool), x ∈ L ↔ ∃ (y : List Bool), y.length ≤ x.length + 1 ∧ pair x y ∈ L₀) : (SAT.satGuessVerifyNTM M).DecidesInTime L (SAT.satGuessVerifyTime f)

The guess-and-verify machine decides any language whose members are exactly the inputs with a short certificate accepted by M.

theorem Complexity.mem_NP_of_linear_witness {L L₀ : Language} (hL₀ : L₀ ∈ P) (hchar : ∀ (x : List Bool), x ∈ L ↔ ∃ (y : List Bool), y.length ≤ x.length + 1 ∧ pair x y ∈ L₀) : L ∈ NP

Guess and verify. A language whose members are exactly the inputs carrying a certificate of length at most |x| + 1 that a polynomial-time verifier accepts is in NP.

Any polynomial witness bound

noncomputable def Complexity.padWith (p : Polynomial ℕ) (x : List Bool) : List Bool

The input padded with a ruler long enough to make the witness bound linear.

Equations

• Complexity.padWith p x = Complexity.pair x (Complexity.polyRuler p x)

theorem Complexity.padWith_mem_FP (p : Polynomial ℕ) : padWith p ∈ FP

noncomputable def Complexity.padVerifier (p : Polynomial ℕ) (L₀ : Language) : Language

The verifier for the padded language: run the original verifier on the unpadded input, and check that the padding really is long enough.

Equations

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

theorem Complexity.padVerifier_mem_P {p : Polynomial ℕ} {L₀ : Language} (hL₀ : L₀ ∈ P) : padVerifier p L₀ ∈ P

noncomputable def Complexity.padLang (p : Polynomial ℕ) (L₀ : Language) : Language

The padded language, whose witnesses are short enough for the linear guess-and-verify machine.

Equations

• Complexity.padLang p L₀ = {z : List Bool | ∃ (y : List Bool), y.length ≤ z.length + 1 ∧ Complexity.pair z y ∈ Complexity.padVerifier p L₀}

theorem Complexity.padLang_mem_NP {p : Polynomial ℕ} {L₀ : Language} (hL₀ : L₀ ∈ P) : padLang p L₀ ∈ NP

theorem Complexity.mem_NP_of_poly_witness {L L₀ : Language} (p : Polynomial ℕ) (hL₀ : L₀ ∈ P) (hbal : ∀ (x y : List Bool), pair x y ∈ L₀ → y.length ≤ Polynomial.eval x.length p) (hchar : ∀ (x : List Bool), x ∈ L ↔ ∃ (y : List Bool), pair x y ∈ L₀) : L ∈ NP

Guess and verify, with any polynomial witness bound. A language whose members are exactly the inputs carrying a certificate a polynomial-time verifier accepts is in NP, provided the verifier only accepts certificates of polynomial length.