The problem of true quantified Boolean formulas

TQBF is the set of true closed quantified Boolean formulas over variables numbered by ℕ: formulas without free variables whose value is true Sipser, Section 8.3 Arora and Barak, Section 4.2. A closed formula has the same value under every assignment (Cslib.Logic.PL.QBF.eval_eq_of_closed), so the assignment fun _ => false in the definition is immaterial. Instances are formulas, not words, and every formula is an instance: formulas with a free variable are simply not in TQBF. Formulas are not required to be in prenex form; the prenex formulas of the textbooks are among them.

A formula is encoded by its tokens in prefix (Polish) order (Cslib.Logic.PL.QBF.tokens): the kind of each node, with its variable for variables and quantifiers and 0 otherwise, as a framed list of framed pairs of the kind in unary and the variable in binary (Cslib.Complexity.encQBF). The prefix order makes the encoding injective without delimiters (Cslib.Logic.PL.QBF.tokens_append_inj), and every node takes at least three bits, so a formula with n nodes has an encoding of length at least 3 * n.

Boundary cases: the empty list is the tokens of no formula; the formulas without variables are built from top and bot, and top ∈ TQBF while bot ∉ TQBF; a variable on its own is never closed, so var v ∉ TQBF, while ex v (var v) ∈ TQBF and all v (var v) ∉ TQBF.

Main definitions

• Cslib.Logic.PL.QBF.Kind, Cslib.Logic.PL.QBF.tokens: the tokens of a formula.
• Cslib.Complexity.encQBF: the encoding of formulas.
• Cslib.Complexity.TQBF: the true closed formulas.

Main results

• Cslib.Logic.PL.QBF.tokens_append_inj: tokens in prefix order determine the formula.
• Cslib.Logic.PL.QBF.length_tokens: one token for each node.
• Cslib.Complexity.mem_TQBF, Cslib.Complexity.top_mem_TQBF, Cslib.Complexity.bot_notMem_TQBF, Cslib.Complexity.var_notMem_TQBF: membership and the boundary cases.

References

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

Tokens

inductive Cslib.Logic.PL.QBF.Kind : Type

The kinds of nodes of a quantified Boolean formula.

• var : Kind

  A variable.

• top : Kind

  The constant true.

• bot : Kind

  The constant false.

• not : Kind

  Negation.

• and : Kind

  Conjunction.

• or : Kind

  Disjunction.

• ex : Kind

  Existential quantification.

• all : Kind

  Universal quantification.

@[instance_reducible]

instance Cslib.Logic.PL.QBF.instDecidableEqKind : DecidableEq Kind

@[instance_reducible]

instance Cslib.Logic.PL.QBF.instInhabitedKind : Inhabited Kind

@[instance_reducible]

instance Cslib.Logic.PL.QBF.instFintypeKind : Fintype Kind

def Cslib.Logic.PL.QBF.tokens : QBF ℕ → List (Kind × ℕ)

The tokens of a formula in prefix order: the kind of each node, with its variable for variables and quantifiers, and 0 for the other nodes.

def Cslib.Logic.PL.QBF.readToken : Kind × ℕ → Option (PrefixParser.Step (QBF ℕ))

Interpret an existing formula token as its constructor. Nonzero payloads on constants and connectives are rejected. Variables and quantifiers retain their binary-encoded variable.

theorem Cslib.Logic.PL.QBF.parseFuel_tokens (φ : QBF ℕ) (rest : List (Kind × ℕ)) (fuel : ℕ) (hf : φ.tokens.length ≤ fuel) : PrefixParser.parseFuel readToken fuel (φ.tokens ++ rest) = some (φ, rest)

Parsing a formula's tokens recovers it and leaves the following suffix untouched.

theorem Cslib.Logic.PL.QBF.tokens_append_inj {φ ψ : QBF ℕ} {r r' : List (Kind × ℕ)} (h : φ.tokens ++ r = ψ.tokens ++ r') : φ = ψ ∧ r = r'

Tokens in prefix order determine the formula, and what follows them.

theorem Cslib.Logic.PL.QBF.tokens_injective : Function.Injective tokens

theorem Cslib.Logic.PL.QBF.tokens_ne_nil (φ : QBF ℕ) : φ.tokens ≠ []

Every formula has a token.

theorem Cslib.Logic.PL.QBF.length_tokens (φ : QBF ℕ) : φ.tokens.length = φ.size

A formula has one token for each of its nodes.

def Cslib.Complexity.TQBF.kindIndex : Logic.PL.QBF.Kind → ℕ

The index of a kind, from 0 for variables to 7 for universal quantifiers.

theorem Cslib.Complexity.TQBF.kindIndex_injective : Function.Injective kindIndex

def Cslib.Complexity.TQBF.encKind : Logic.PL.QBF.Kind ↪ List Bool

Kinds encoded by their index in unary.

@[reducible, inline]

abbrev Cslib.Complexity.TQBF.encToken : Logic.PL.QBF.Kind × ℕ ↪ List Bool

Tokens encoded as framed pairs of the kind in unary and the variable in binary.

def Cslib.Complexity.encQBF : Logic.PL.QBF ℕ ↪ List Bool

Formulas encoded by their tokens in prefix order (Cslib.Logic.PL.QBF.tokens), as a list of framed tokens.

theorem Cslib.Complexity.encQBF_apply (φ : Logic.PL.QBF ℕ) : encQBF φ = (Turing.MultiTapeTM.encList TQBF.encToken) φ.tokens

A formula is encoded as the list of its framed tokens in prefix order.

theorem Cslib.Complexity.three_mul_length_tokens_le (φ : Logic.PL.QBF ℕ) : 3 * φ.tokens.length ≤ (encQBF φ).length

Every node takes at least three bits.

True closed formulas

def Cslib.Complexity.TQBF : Set (Logic.PL.QBF ℕ)

The true closed quantified Boolean formulas over variables numbered by natural numbers Sipser, Section 8.3, Arora and Barak, Section 4.2.

theorem Cslib.Complexity.mem_TQBF {φ : Logic.PL.QBF ℕ} : φ ∈ TQBF ↔ φ.Closed ∧ Logic.PL.QBF.eval (fun (x : ℕ) => false) φ = true

A formula is in TQBF exactly when it is closed and true under the assignment fun _ => false.

theorem Cslib.Complexity.mem_TQBF_iff_of_closed {φ : Logic.PL.QBF ℕ} (hφ : φ.Closed) (σ : ℕ → Bool) : φ ∈ TQBF ↔ Logic.PL.QBF.eval σ φ = true

A closed formula is in TQBF exactly when it is true under some, equivalently every, assignment.

theorem Cslib.Complexity.top_mem_TQBF : Logic.PL.QBF.top ∈ TQBF

The constant true is a true closed formula.

theorem Cslib.Complexity.bot_notMem_TQBF : Logic.PL.QBF.bot ∉ TQBF

The constant false is not true.

theorem Cslib.Complexity.var_notMem_TQBF (v : ℕ) : Logic.PL.QBF.var v ∉ TQBF

A variable on its own is not closed.