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, first for witnesses of linear length and then for any polynomial witness bound, by padding the input until the bound is linear. Complexitylib.Classes.NP.WitnessConstruction repackages the result as the proof NP.witnessNTMConstruction of the guess-and-verify interface NP.WitnessNTMConstruction.

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.