TQBF in alternating prenex conjunctive normal form

A quantified Boolean formula is in alternating prenex conjunctive normal form when it is ∃ x₁, ∀ y₁, ⋯, ∃ xₙ, ∀ yₙ, ψ for a formula ψ in conjunctive normal form (Cslib.Logic.PL.QBF.rounds, Cslib.Logic.PL.QBF.ofCNF). TQBFCNF is the set of pairs of a list of rounds (xᵢ, yᵢ) and a formula ψ whose formula is a true closed formula (Cslib.Complexity.TQBF). The game played on such a formula is Sipser's FORMULA-GAME Sipser, Theorem 8.11, the starting point of the textbook PSPACE-hardness proofs of games such as Generalized Geography Sipser, Theorem 8.14.

TQBFCNF is PSPACE-complete (Cslib.Complexity.TQBFCNF_pspaceComplete): it is in PSPACE because writing the formula is polynomial-time, and it is PSPACE-hard because the formulas of games (Cslib.Complexity.TQBF.gameFormula), which every problem in PSPACE reduces to (Cslib.Complexity.exists_isGameVerifier_of_mem_PSPACE), are already almost in this form: rounds over the moves, then existential quantifiers over the variables of a Cook–Levin tableau and the conjunction of the tableau with equivalences linking its certificate variables to the moves. Each equivalence a ↔ b is written as the two clauses ¬a ∨ b and a ∨ ¬b (Cslib.Complexity.TQBF.certLinkCNF), and each existential quantifier ∃ v becomes the round ∃ v, ∀ d over a fixed variable d that occurs nowhere else (Cslib.Complexity.TQBF.dummyVar), which does not change the value (Cslib.Logic.PL.QBF.eval_rounds_map_pair).

Main definitions

• Cslib.Complexity.TQBFCNF, Cslib.Complexity.encPrenexCNF: the problem and its encoding.
• Cslib.Complexity.TQBF.prenexReduce: the formula of a game in alternating prenex conjunctive normal form.

Main results

• Cslib.Complexity.TQBF.eval_prenex, Cslib.Complexity.TQBF.closed_prenex: the normal form of the formula of a game has its value and is closed.
• Cslib.Complexity.TQBF.prenexReduce_mem_TQBFCNF_iff, Cslib.Complexity.TQBF.computableInPolyTime_prenexReduce: the normal form is correct and polynomial-time.
• Cslib.Complexity.TQBFCNF_mem_PSPACE, Cslib.Complexity.TQBFCNF_pspaceHard, Cslib.Complexity.TQBFCNF_pspaceComplete: TQBFCNF is PSPACE-complete.

References

• M. Sipser, Introduction to the Theory of Computation, Section 8.3
• L. Stockmeyer, A. Meyer, Word problems requiring exponential time

@[reducible, inline]

abbrev Cslib.Complexity.encPrenexCNF : List (ℕ × ℕ) × Logic.PL.CNF ℕ ↪ List Bool

Instances (ps, ψ) of TQBFCNF: the rounds of quantifiers as framed pairs of binary variables, and the formula as in Cslib.Complexity.encCNF.

def Cslib.Complexity.TQBFCNF : Set (List (ℕ × ℕ) × Logic.PL.CNF ℕ)

True closed formulas in alternating prenex conjunctive normal form: the pairs of rounds (x₁, y₁), …, (xₙ, yₙ) and a formula ψ in conjunctive normal form such that ∃ x₁, ∀ y₁, ⋯, ∃ xₙ, ∀ yₙ, ψ is a true closed formula.

theorem Cslib.Complexity.TQBF.computableInPolyTime_rounds {γ : Type} {encIn : γ ↪ List Bool} {ps : γ → List (ℕ × ℕ)} {φ : γ → Logic.PL.QBF ℕ} (hps : Turing.MultiTapeTM.ComputableInPolyTime ps encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat Turing.MultiTapeTM.encNat))) (hφ : Turing.MultiTapeTM.ComputableInPolyTime φ encIn encQBF) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : γ) => Logic.PL.QBF.rounds (ps x) (φ x)) encIn encQBF

Rounds of quantifiers are polynomial-time in the rounds and the body.

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

The links of the certificate variables to the blocks of level 0 (certLinks) as clauses: ¬a ∨ b and a ∨ ¬b for each link a ↔ b.

def Cslib.Complexity.TQBF.dummyVar : ℕ

A variable of the blocks of level 0 that no formula of a game uses: the first variable of the midpoint block of level 0.

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

The rounds of the normal form of the formula of a game: those over the moves, then a round ∃ v, ∀ dummyVar for each variable v of the formula of level 0.

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

The matrix of the normal form of the formula of a game: the links of the certificate variables as clauses, then the tableau.

theorem Cslib.Complexity.TQBF.eval_prenex {k : ℕ} {State : Type} [Fintype State] (tab : Logic.PL.CNF (CookLevin.Var k State)) (w : ℕ) (σ : ℕ → Bool) : Logic.PL.QBF.eval σ (Logic.PL.QBF.rounds (prenexPairs tab w) (Logic.PL.QBF.ofCNF (prenexMatrix tab w))) = Logic.PL.QBF.eval σ (gameFormula tab w)

The normal form of the formula of a game has its value.

theorem Cslib.Complexity.TQBF.closed_prenex {k : ℕ} {State : Type} [Fintype State] (tab : Logic.PL.CNF (CookLevin.Var k State)) (w : ℕ) : (Logic.PL.QBF.rounds (prenexPairs tab w) (Logic.PL.QBF.ofCNF (prenexMatrix tab w))).Closed

The normal form of the formula of a game is closed.

noncomputable def Cslib.Complexity.TQBF.gameTableau {α : Type} (enc : α ↪ List Bool) (p : Polynomial ℕ) {kV : ℕ} {StateV : Type} [Fintype StateV] [DecidableEq StateV] (tmV : Turing.MultiTapeTM kV Bool StateV) (cV dV : ℕ) (a : α) : Logic.PL.CNF (CookLevin.Var kV StateV)

The Cook–Levin tableau of the formula of a game (gameReduce).

noncomputable def Cslib.Complexity.TQBF.prenexReduce {α : Type} (enc : α ↪ List Bool) (p : Polynomial ℕ) {kV : ℕ} {StateV : Type} [Fintype StateV] [DecidableEq StateV] (tmV : Turing.MultiTapeTM kV Bool StateV) (cV dV : ℕ) (a : α) : List (ℕ × ℕ) × Logic.PL.CNF ℕ

The reduction of a game to TQBFCNF: the formula of the game (gameReduce) in alternating prenex conjunctive normal form.

theorem Cslib.Complexity.TQBF.prenexReduce_mem_TQBFCNF_iff {α : Type} {enc : α ↪ List Bool} {p : Polynomial ℕ} {kV : ℕ} {StateV : Type} [Fintype StateV] [DecidableEq StateV] (tmV : Turing.MultiTapeTM kV Bool StateV) (cV dV : ℕ) (a : α) : prenexReduce enc p tmV cV dV a ∈ TQBFCNF ↔ gameReduce enc p tmV cV dV a ∈ TQBF

The normal form of the formula of a game is in TQBFCNF exactly when the formula is in TQBF.

theorem Cslib.Complexity.TQBF.computableInPolyTime_prenexReduce {α : Type} {enc : α ↪ List Bool} {p : Polynomial ℕ} {kV : ℕ} {StateV : Type} [Fintype StateV] [DecidableEq StateV] (tmV : Turing.MultiTapeTM kV Bool StateV) (cV dV : ℕ) : Turing.MultiTapeTM.ComputableInPolyTime (prenexReduce enc p tmV cV dV) enc encPrenexCNF

The reduction of a game to TQBFCNF is polynomial-time.

theorem Cslib.Complexity.TQBFCNF_mem_PSPACE : TQBFCNF ∈ PSPACE encPrenexCNF

TQBFCNF is in PSPACE: writing the formula is polynomial-time.

theorem Cslib.Complexity.TQBFCNF_pspaceHard : PSPACEHard encPrenexCNF TQBFCNF

TQBFCNF is PSPACE-hard: a problem in PSPACE is a game of polynomially many moves with a polynomial-time winning condition, whose formula is put in alternating prenex conjunctive normal form.

theorem Cslib.Complexity.TQBFCNF_pspaceComplete : PSPACEComplete encPrenexCNF TQBFCNF

TQBF in alternating prenex conjunctive normal form is PSPACE-complete Sipser, Section 8.3.