Guess and verify

Every problem in Cslib.Complexity.NP is decided in polynomial time by a nondeterministic machine with a binary alphabet and finitely many states, which guesses a certificate and runs the verifier on it: the inclusion of NP in nondeterministic polynomial time Arora and Barak, Theorem 2.6. The converse, and hence the characterization of NP, is in CslibFrontier.Computability.Complexity.Classes.NP.Nondeterministic.

The machine is built from the PPT calculus and its clock compiler rather than by hand. For a verifier V with certificates of length p (enc a).length, the probabilistic program that samples a word of this length and returns the verdict of V is uniformly polynomial-time. The clock compiler Cslib.Probability.IsPPTOn.exists_halting_machine turns it into a finite fair-coin machine that actually halts on every branch within a polynomial clock. Its nondeterministic machine Turing.MultiTapePTM.toNTM guesses the coins: its computation paths are exactly the coin replays, so it accepts exactly when some certificate of the required length is accepted. It is never stuck, so every branch actually halts within the bound.

Main results

• Cslib.Complexity.IsVerifier.exists_decidesInTime: a verifier gives a fair-coin machine whose nondeterministic machine decides the problem within an explicit polynomial and is never stuck.
• Cslib.Complexity.decidableInPolyTime_of_mem_NP: NP problems are decidable in nondeterministic polynomial time.

References

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

theorem Cslib.Complexity.IsVerifier.exists_decidesInTime {α : Type} {enc : α ↪ List Bool} {p : Polynomial ℕ} {V : α × List Bool → Bool} {A : Set α} (hV : Turing.MultiTapeTM.ComputableInPolyTime V (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool) (hA : IsVerifier enc p V A) : ∃ (k : ℕ) (State : Type) (_ : Finite State) (machine : Turing.MultiTapePTM k Bool State) (c : ℕ) (d : ℕ), (machine.toNTM.DecidesInTime enc A fun (a : α) => c * ((enc a).length + 1) ^ d) ∧ ∀ (input : List Bool) (cfg : Turing.Cfg k Bool State input), ∃ (cfg' : Turing.Cfg k Bool State input), machine.toNTM.Step cfg cfg'

Guess and verify, the inclusion of NP in nondeterministic polynomial time Arora and Barak, Theorem 2.6. A polynomial-time verifier gives a finite fair-coin machine whose nondeterministic machine decides the problem within the explicit polynomial c * ((enc a).length + 1) ^ d. That machine is never stuck, so its branches actually halt within the bound.

theorem Cslib.Complexity.decidableInPolyTime_of_mem_NP {α : Type} {enc : α ↪ List Bool} {A : Set α} (h : A ∈ NP enc) : Turing.MultiTapeNTM.DecidableInPolyTime A enc

Problems in NP are decidable in polynomial time by nondeterministic machines with a binary alphabet and finitely many states.