Documentation

Complexity.Computability.Complexity.Problems.TQBF

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 #

Main results #

References #

Tokens #

source
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.

Instances For
    source
    @[instance_reducible]
    instance Cslib.Logic.PL.QBF.instDecidableEqKind :
    DecidableEq Kind
    source
    @[instance_reducible]
    instance Cslib.Logic.PL.QBF.instInhabitedKind :
    Inhabited Kind
    source
    @[instance_reducible]
    instance Cslib.Logic.PL.QBF.instFintypeKind :
    Fintype Kind
    source
    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.

    Instances For
      source
      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.

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

      Every formula has a token.

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

      A formula has one token for each of its nodes.

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

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

      Instances For
        source
        theorem Cslib.Complexity.TQBF.kindIndex_injective :
        Function.Injective kindIndex
        source
        def Cslib.Complexity.TQBF.encKind :
        Logic.PL.QBF.Kind ↪ List Bool

        Kinds encoded by their index in unary.

        Instances For
          source
          @[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.

          Instances For
            source
            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.

            Instances For
              source
              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.

              source
              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 #

              source
              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.

              Instances For
                source
                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.

                source
                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.

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

                The constant true is a true closed formula.

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

                The constant false is not true.

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

                A variable on its own is not closed.