Nondeterministic time through verifiers, with explicit bounds

This module characterizes Cslib.Complexity.NTIME enc t by deterministic verifiers, keeping the time bound up to constant factors. The polynomial characterization of NP (Cslib.Complexity.mem_NP_iff_decidableInPolyTime) loses the degree in both directions. The two directions here keep it.

• Guess and verify (Cslib.Complexity.setOf_exists_mem_NTIME). Suppose a verifier V is computable within time T (a, w) on encoded pairs, and a certificate length ℓ a is computable in unary within time Tℓ a. Then the problem {a | ∃ w, w.length = ℓ a ∧ V (a, w) = true} lies in NTIME enc t whenever (enc a).length + Tℓ a + T (a, w) is within O(t (enc a).length) on certificates of that length. The certificate length may depend on the instance, not only on its encoded length. The machine is the nondeterministic reading of the sample-and-verify machine (Cslib.Complexity.exists_machine_sampleVerify), a closed fair-coin composition that writes frame (enc a) followed by ℓ ones, replaces the ones by fair coins with the fixed sampler Turing.MultiTapePTM.pairSampler, and runs the verifier. Its computation paths are exactly the coin replays, so it accepts exactly when some certificate is accepted, and every branch halts within the clock.
• Verifiers from nondeterministic time (Cslib.Complexity.exists_verifier_of_mem_NTIME). A problem in NTIME enc t has a verifier that is computable in linear time on encoded pairs: check that the certificate, read as coins of the choice table (Turing.MultiTapeNTM.checkChoices), replays an accepting computation. Every certificate length of at least c * t (enc a).length + c works, for a constant c.

These are explicit-time forms of the guess-and-verify characterization of nondeterministic polynomial time Arora and Barak: the choices of an accepting computation are a certificate, and a certificate can be guessed and then checked.

Main results

• Cslib.Complexity.setOf_exists_mem_NTIME: guess and verify within explicit time.
• Cslib.Complexity.exists_verifier_of_mem_NTIME: a linear-time verifier for a problem in NTIME, with certificates of every sufficient length.

References

• S. Arora, B. Barak, Computational Complexity: A Modern Approach

theorem Cslib.Complexity.setOf_exists_mem_NTIME {α : Type} {enc : α ↪ List Bool} {V : α × List Bool → Bool} {ℓ : α → ℕ} {t : ℕ → ℕ} {Tℓ Sℓ : α → ℕ} {T S : α × List Bool → ℕ} {C : ℕ} (hℓ : Turing.MultiTapeTM.ComputableInO ℓ enc Turing.MultiTapeTM.encUnary Tℓ Sℓ) (hV : Turing.MultiTapeTM.ComputableInO V (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool T S) (ht : ∀ (a : α) (w : List Bool), w.length = ℓ a → (enc a).length + Tℓ a + T (a, w) ≤ C * t (enc a).length + C) : {a : α | ∃ (w : List Bool), w.length = ℓ a ∧ V (a, w) = true} ∈ NTIME enc t

Guess and verify, within explicit time. If a verifier V is computable within time T (a, w) on encoded pairs, and the certificate length ℓ a is computable in unary within time Tℓ a, then the problem of instances with an accepted certificate of that length is in NTIME enc t, provided (enc a).length + Tℓ a + T (a, w) ≤ C * t (enc a).length + C for every certificate w of that length.

theorem Cslib.Complexity.exists_verifier_of_mem_NTIME {α : Type} {enc : α ↪ List Bool} {A : Set α} {t : ℕ → ℕ} (hA : A ∈ NTIME enc t) : ∃ (V : α × List Bool → Bool) (c : ℕ), (Turing.MultiTapeTM.ComputableInO V (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool (fun (p : α × List Bool) => ((Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) p).length) fun (p : α × List Bool) => ((Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) p).length) ∧ ∀ (a : α) (L : ℕ), c * t (enc a).length + c ≤ L → (a ∈ A ↔ ∃ (w : List Bool), w.length = L ∧ V (a, w) = true)

A linear-time verifier for nondeterministic time. A problem in NTIME enc t has a verifier computable in linear time on encoded pairs. For a constant c, every certificate length L ≥ c * t (enc a).length + c works: a ∈ A exactly when some certificate of length L is accepted. The verifier checks that the certificate, read as coins of the choice table, replays an accepting computation.