The reduction to TQBF

Acceptance of a nondeterministic machine within polynomial space is reachability of the accepting code from the code of the initial view, along the edges between the codes of its finite views (Turing.MultiTapeNTM.savitchDecide_eq_true_iff). This file writes this reachability as a closed quantified Boolean formula Sipser, Theorem 8.9 Arora and Barak, Theorem 4.13: Savitch's formula (Cslib.Complexity.TQBF.savitchFormula) on the codes, of width w = 2 * W + 2 for the width W of the codes, at depth w. Each of its w levels has O(w) tokens, so it has O(w ^ 2) tokens besides those of its formula of level 0; it is computed in polynomial time in Cslib.Computability.Complexity.Classes.Space.TQBF.PolyTime.

Its formula of level 0 must express one step or none between the words held by two blocks. The step test of codes is polynomial-time (Cslib.Complexity.TQBF.computableInPolyTime_edgeTest), so some tidy machine computes, on encPair enc encBits (a, x ++ y), the Boolean Cslib.Reachability.reach e w 0 x y for the edge test e of the codes, within a polynomial time bound T. Its Cook–Levin tableau (Cslib.Complexity.CookLevin.tableau) on the inputs frame (enc a) ++ z with |z| = 2 * w, unrolled for T steps, has a satisfying assignment with certificate bits z exactly when the machine accepts frame (enc a) ++ z (Cslib.Complexity.CookLevin.exists_eval_tableau_iff). The formula of level 0 (Cslib.Complexity.TQBF.baseFormula) numbers the variables of the tableau by odd numbers, links its certificate variables to the source and target blocks of level 0, and quantifies all of them existentially (Cslib.Complexity.TQBF.eval_baseFormula); its free variables are the blocks.

Main definitions

• Cslib.Complexity.TQBF.tabVar: the numbering of the tableau variables by odd numbers.
• Cslib.Complexity.TQBF.baseFormula: a tableau as a formula on the blocks of level 0.
• Cslib.Complexity.TQBF.edgeTest: the test of one step or none between codes.
• Cslib.Complexity.TQBF.reduce: the reduction.

Main results

• Cslib.Complexity.TQBF.eval_baseFormula, Cslib.Complexity.TQBF.mem_freeVars_baseFormula: the formula of level 0.
• Cslib.Complexity.TQBF.reduce_mem_TQBF_iff: the reduction is correct.

References

• M. Sipser, Introduction to the Theory of Computation, Theorem 8.9
• S. Arora, B. Barak, Computational Complexity: A Modern Approach, Theorem 4.13

A tableau as the formula of level 0

noncomputable def Cslib.Complexity.TQBF.tabVar {k : ℕ} {State : Type} [Fintype State] (v : CookLevin.Var k State) : ℕ

The tableau variables, numbered by odd numbers.

theorem Cslib.Complexity.TQBF.tabVar_injective {k : ℕ} {State : Type} [Fintype State] : Function.Injective tabVar

theorem Cslib.Complexity.TQBF.tabVar_mod_two {k : ℕ} {State : Type} [Fintype State] (v : CookLevin.Var k State) : tabVar v % 2 = 1

def Cslib.Complexity.TQBF.certVar (w j : ℕ) : ℕ

The variable of a block of level 0 holding the j-th certificate bit: the source block for the first w bits, then the target block.

noncomputable def Cslib.Complexity.TQBF.baseVars {k : ℕ} {State : Type} [Fintype State] (tab : Logic.PL.CNF (CookLevin.Var k State)) (w : ℕ) : List ℕ

The variables quantified in the formula of level 0: the variables of the tableau and its first 2 * w certificate variables.

noncomputable def Cslib.Complexity.TQBF.certLinks (k : ℕ) (State : Type) [Fintype State] (w : ℕ) : Logic.PL.QBF ℕ

The links of the certificate variables to the blocks of level 0.

noncomputable def Cslib.Complexity.TQBF.baseFormula {k : ℕ} {State : Type} [Fintype State] (tab : Logic.PL.CNF (CookLevin.Var k State)) (w : ℕ) : Logic.PL.QBF ℕ

A tableau as the formula of level 0: its variables numbered by odd numbers, its first 2 * w certificate variables linked to the source and target blocks of level 0, and all of them quantified existentially.

theorem Cslib.Complexity.TQBF.eval_baseFormula {k : ℕ} {State : Type} [Fintype State] (tab : Logic.PL.CNF (CookLevin.Var k State)) (w : ℕ) (σ : ℕ → Bool) : Logic.PL.QBF.eval σ (baseFormula tab w) = true ↔ ∃ (τ : CookLevin.Var k State → Bool), CookLevin.certWord τ (2 * w) = block σ w 0 0 ++ block σ w 1 0 ∧ Logic.PL.CNF.eval τ tab = true

The formula of level 0 holds exactly when the tableau has a satisfying assignment whose first 2 * w certificate bits are the words held by the source and target blocks of level 0.

theorem Cslib.Complexity.TQBF.mem_freeVars_baseFormula {k : ℕ} {State : Type} [Fintype State] (tab : Logic.PL.CNF (CookLevin.Var k State)) (w x : ℕ) : x ∈ (baseFormula tab w).freeVars → x ∈ blockVars w 0 0 ∨ x ∈ blockVars w 1 0

The free variables of the formula of level 0 lie in the source and target blocks of level 0.

The reduction

noncomputable def Cslib.Complexity.TQBF.edgeTest {α : Type} (enc : α ↪ List Bool) {k : ℕ} {State : Type} [Finite State] (ntm : Turing.MultiTapeNTM k Bool State) (c d : ℕ) (p : α × List Bool) : Bool

The test of one step or none between codes, on the instance a and the concatenation of the two codes.

noncomputable def Cslib.Complexity.TQBF.edgeTime {α : Type} (enc : α ↪ List Bool) {k : ℕ} {State : Type} [Finite State] (ntm : Turing.MultiTapeNTM k Bool State) (c d cV dV : ℕ) (a : α) : ℕ

The time allowed to a machine computing the test on encPair enc encBits (a, z) with |z| = 2 * ntm.viewCodeWidth c d (enc a), for the time bound cV * (n + 1) ^ dV.

noncomputable def Cslib.Complexity.TQBF.reduce {α : Type} (enc : α ↪ List Bool) {k : ℕ} {State : Type} [Finite State] (ntm : Turing.MultiTapeNTM k Bool State) (c d : ℕ) {kV : ℕ} {StateV : Type} [Fintype StateV] [DecidableEq StateV] (tmV : Turing.MultiTapeTM kV Bool StateV) (cV dV : ℕ) (a : α) : Logic.PL.QBF ℕ

The reduction to TQBF: Savitch's formula on the codes of the views of ntm on enc a, from the code of the initial view to the accepting code, with the Cook–Levin tableau of the machine tmV computing the test of one step or none as its formula of level 0.

theorem Cslib.Complexity.TQBF.reduce_mem_TQBF_iff {α : Type} {enc : α ↪ List Bool} {k : ℕ} {State : Type} [Finite State] {ntm : Turing.MultiTapeNTM k Bool State} {c d kV : ℕ} {StateV : Type} [Fintype StateV] [DecidableEq StateV] {tmV : Turing.MultiTapeTM kV Bool StateV} {cV dV : ℕ} {sV : α × List Bool → ℕ} (htm : tmV.ComputesFunTidilyInTimeAndSpace (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool (edgeTest enc ntm c d) (fun (x : α × List Bool) => cV * (((Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) x).length + 1) ^ dV) sV) {a : α} {s : ℕ} (hs : ntm.RunsInSpace (enc a) s) (hsc : s ≤ c * ((enc a).length + 1) ^ d) : reduce enc ntm c d tmV cV dV a ∈ TQBF ↔ ntm.Accepts (enc a)

The reduction is correct. If tmV computes the test of one step or none tidily within time cV * (n + 1) ^ dV, and every computation path of ntm on enc a visits at most c * ((enc a).length + 1) ^ d work cells, then the formula of a is a true closed formula exactly when ntm accepts enc a.