True quantified Boolean formulas

DefinitionEvaluation of a quantified CNF formula#✓fully proved

Let \(\varphi\) be a CNF formula, let \(a : \mathbb{N} \to \{\mathrm{true}, \mathrm{false}\}\) be an assignment, and let \(Q\) be a quantifier prefix, a list of pairs \((e, v)\) of a flag \(e\) (true for \(\exists\), false for \(\forall\)) and a variable \(v \in \mathbb{N}\). Write \(a[v \mapsto b]\) for the assignment that agrees with \(a\) except that it sends \(v\) to \(b\). With the empty prefix, the formula holds under \(a\) when \(a\) satisfies \(\varphi\). With a prefix whose first entry is \((e, v)\) and whose remaining entries form \(Q'\), it holds under \(a\) when, if \(e\) is true, the formula with prefix \(Q'\) holds under \(a[v \mapsto \mathrm{true}]\) or under \(a[v \mapsto \mathrm{false}]\), and, if \(e\) is false, the formula with prefix \(Q'\) holds under both \(a[v \mapsto \mathrm{true}]\) and \(a[v \mapsto \mathrm{false}]\).

def EvalQBF (pref : List (Bool × ℕ)) (φ : Cslib.Logic.PL.CNF)
    (assign : ℕ → Bool) : Prop :=
  match pref with
  | [] => Cslib.Logic.PL.CNF.Satisfies assign φ
  | (isEx, v) :: rest =>
    if isEx then
      EvalQBF rest φ (Function.update assign v true) ∨
        EvalQBF rest φ (Function.update assign v false)
    else
      EvalQBF rest φ (Function.update assign v true) ∧
        EvalQBF rest φ (Function.update assign v false)

Uses 2 · Used by 1

Statement usesCNF formula · Satisfaction of a CNF formula

Used byTQBF as a decision problem

DefinitionTQBF as a decision problem#✓fully proved

The TQBF decision problem accepts a bitstring \(x\) exactly when \(x\) decodes, under the canonical bitstring encoding, to a pair \((Q, \varphi)\), where \(Q\) is a quantifier prefix, a list of \(m\) pairs \((e_1, v_1), \dots, (e_m, v_m)\) of a flag \(e_i\) (true for \(\exists\), false for \(\forall\)) and a variable \(v_i \in \mathbb{N}\), and \(\varphi\) is a CNF formula, such that \(v_1, \dots, v_m\) are \(0, 1, \dots, m - 1\) in some order, every variable occurring in \(\varphi\) is less than \(m\), and the quantified formula with prefix \(Q\) and matrix \(\varphi\) holds under the assignment that sends every variable to false.

noncomputable def tqbfDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := List (Bool × ℕ) × Cslib.Logic.PL.CNF) x with
  | some i => decide (
      List.Perm (i.1.map Prod.snd) (List.range i.1.length) ∧
      (∀ clause ∈ i.2, ∀ l ∈ clause, l.1 < i.1.length) ∧
      EvalQBF i.1 i.2 (fun _ => false))
  | none => false

Uses 12 · Used by 1

Statement usesCNF formula · CNF clause · Bitstring encodings · Decoding function of a bitstring encoding · Decoding inverts bitstring encoding · Encoding function of a bitstring encoding · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Parsing a list of booleans into self-delimiting blocks · Bounded parsing of self-delimiting blocks · Evaluation of a quantified CNF formula · Decision problems

Used byTQBF is PSPACE-complete

TheoremTQBF is PSPACE-complete#●ready to prove

The TQBF decision problem, of true quantified Boolean formulas with a CNF matrix, lies in the class PSPACE of decision problems, and every decision problem in PSPACE has a polynomial-time many-one reduction to it.

public theorem_wanted tqbf_pspace_complete :
    tqbfDec ∈ PSPACE ∧ ∀ L : MetaMathlibExt.ComplexityTheory.DecisionProblem,
      L ∈ PSPACE → Cslib.CookLevin.PolyManyOneRed L tqbfDec

Sources

• L. J. Stockmeyer and A. R. Meyer, "Word problems requiring exponential time", Proceedings of the Fifth Annual ACM Symposium on Theory of Computing (STOC 1973), 1-9; C. H. Papadimitriou, Computational Complexity, 1994, Theorem 7.4.

Uses 5

Statement usesPolynomial space for decision problems · Polynomial-time many-one reduction · TQBF as a decision problem · Complexity classes · Decision problems

2 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.