Documentation

Complexitylib.SAT.QBF

Quantified Boolean formulas #

Syntax and semantics of quantified Boolean formulas (QBF) — the canonical PSPACE object, and the target of the TQBF PSPACE-completeness theorem and the IP = PSPACE development (roadmap tracks N3, M4, L1).

A QBF is a Boolean formula over variables x_i (i : ℕ) closed under ¬, ∧, ∨, and the quantifiers ∃ x_i and ∀ x_i. Semantics are given by QBF.eval relative to an assignment α : ℕ → Bool; a quantifier over x_i ranges over the two Boolean values substituted for x_i via Function.update.

Main definitions and results #

source
inductive Complexity.QBF :
Type

Quantified Boolean formulas over variables indexed by ℕ.

  • var (i : ℕ) : QBF

    The variable x_i.

  • tru : QBF

    The constant ⊤.

  • fls : QBF

    The constant ⊥.

  • neg (φ : QBF) : QBF

    Negation ¬ φ.

  • conj (φ ψ : QBF) : QBF

    Conjunction φ ∧ ψ.

  • disj (φ ψ : QBF) : QBF

    Disjunction φ ∨ ψ.

  • ex (i : ℕ) (φ : QBF) : QBF

    Existential quantifier ∃ x_i, φ.

  • all (i : ℕ) (φ : QBF) : QBF

    Universal quantifier ∀ x_i, φ.

Instances For
    source
    @[implicit_reducible]
    instance Complexity.instReprQBF :
    Repr QBF
    Equations
    source
    def Complexity.instReprQBF.repr :
    QBF → ℕ → Std.Format
    Equations
    Instances For
      source
      def Complexity.instDecidableEqQBF.decEq (x✝ x✝¹ : QBF) :
      Decidable (x✝ = x✝¹)
      Equations
      Instances For
        source
        @[implicit_reducible]
        instance Complexity.instDecidableEqQBF :
        DecidableEq QBF
        Equations
        source
        def Complexity.QBF.eval (α : ℕ → Bool) :
        QBF → Bool

        Evaluate a QBF under an assignment α : ℕ → Bool. A quantifier over x_i substitutes both Boolean values for x_i (via Function.update) and combines the results disjunctively (ex) or conjunctively (all).

        Equations
        Instances For
          source
          @[simp]
          theorem Complexity.QBF.eval_var (α : ℕ → Bool) (i : ℕ) :
          eval α (var i) = α i
          source
          @[simp]
          theorem Complexity.QBF.eval_tru (α : ℕ → Bool) :
          eval α tru = true
          source
          @[simp]
          theorem Complexity.QBF.eval_fls (α : ℕ → Bool) :
          eval α fls = false
          source
          @[simp]
          theorem Complexity.QBF.eval_neg (α : ℕ → Bool) (φ : QBF) :
          eval α φ.neg = !eval α φ
          source
          @[simp]
          theorem Complexity.QBF.eval_conj (α : ℕ → Bool) (φ ψ : QBF) :
          eval α (φ.conj ψ) = (eval α φ && eval α ψ)
          source
          @[simp]
          theorem Complexity.QBF.eval_disj (α : ℕ → Bool) (φ ψ : QBF) :
          eval α (φ.disj ψ) = (eval α φ || eval α ψ)
          source
          theorem Complexity.QBF.eval_ex_iff (α : ℕ → Bool) (i : ℕ) (φ : QBF) :
          eval α (ex i φ) = true ↔ ∃ (b : Bool), eval (Function.update α i b) φ = true

          Existential substitution semantics. ∃ x_i, φ is true under α iff φ is true for some Boolean value substituted for x_i.

          source
          theorem Complexity.QBF.eval_all_iff (α : ℕ → Bool) (i : ℕ) (φ : QBF) :
          eval α (all i φ) = true ↔ ∀ (b : Bool), eval (Function.update α i b) φ = true

          Universal substitution semantics. ∀ x_i, φ is true under α iff φ is true for every Boolean value substituted for x_i.

          source
          def Complexity.QBF.quantDepth :
          QBF → ℕ

          The quantifier nesting depth of a QBF — an upper bound on the number of quantifier alternations, used to stratify QBF (and hence the polynomial hierarchy) by bounded alternation.

          Equations
          Instances For
            source
            def Complexity.QBF.QuantifierFree (φ : QBF) :
            Prop

            A QBF is quantifier-free when it has no quantifiers (depth 0).

            Equations
            Instances For
              source
              theorem Complexity.QBF.quantifierFree_conj {φ ψ : QBF} :
              (φ.conj ψ).QuantifierFree ↔ φ.QuantifierFree ∧ ψ.QuantifierFree

              A conjunction is quantifier-free iff both conjuncts are.

              source
              def Complexity.QBF.freeVars :
              QBF → Finset ℕ

              The free variables of a QBF: variables not captured by an enclosing quantifier. A quantifier ∃ x_i / ∀ x_i removes i from the free set.

              Equations
              Instances For
                source
                theorem Complexity.QBF.eval_eq_of_agree (φ : QBF) (α β : ℕ → Bool) :
                (∀ i ∈ φ.freeVars, α i = β i) → eval α φ = eval β φ

                Semantic locality of QBF. Evaluation depends only on the free variables: if two assignments agree on freeVars φ, they give φ the same value. In particular a closed formula (empty freeVars) has an assignment-independent truth value. The quantifier cases use that updating the bound variable makes the two assignments agree on the quantified subformula.

                source
                theorem Complexity.QBF.eval_update_not_mem (α : ℕ → Bool) (i : ℕ) (b : Bool) (φ : QBF) (hi : i ∉ φ.freeVars) :
                eval (Function.update α i b) φ = eval α φ

                Updating a non-free variable does not change a formula's value.

                source
                theorem Complexity.QBF.eval_ex_not_mem (α : ℕ → Bool) (i : ℕ) (φ : QBF) (hi : i ∉ φ.freeVars) :
                eval α (ex i φ) = eval α φ

                Vacuous existential quantification. Quantifying ∃ over a variable that does not occur free is a no-op: eval α (∃ x_i, φ) = eval α φ.

                source
                theorem Complexity.QBF.eval_all_not_mem (α : ℕ → Bool) (i : ℕ) (φ : QBF) (hi : i ∉ φ.freeVars) :
                eval α (all i φ) = eval α φ

                Vacuous universal quantification. Quantifying ∀ over a variable that does not occur free is a no-op: eval α (∀ x_i, φ) = eval α φ.

                source
                def Complexity.QBF.Closed (φ : QBF) :
                Prop

                A QBF is closed when it has no free variables.

                Equations
                Instances For
                  source
                  theorem Complexity.QBF.eval_closed_eq {φ : QBF} (hφ : φ.Closed) (α β : ℕ → Bool) :
                  eval α φ = eval β φ

                  A closed QBF evaluates to the same value under any assignment: the truth value of a fully-quantified formula is well defined.

                  source
                  def Complexity.QBF.IsTrue (φ : QBF) :
                  Prop

                  A closed QBF is true when it evaluates to true. By eval_closed_eq the choice of assignment is immaterial; this uses the all-false one. The set of true closed QBFs is the canonical PSPACE-complete problem TQBF.

                  Equations
                  Instances For
                    source
                    @[implicit_reducible]
                    instance Complexity.QBF.instDecidableClosed (φ : QBF) :
                    Decidable φ.Closed
                    Equations
                    source
                    @[implicit_reducible]
                    instance Complexity.QBF.instDecidableIsTrue (φ : QBF) :
                    Decidable φ.IsTrue
                    Equations
                    source
                    theorem Complexity.QBF.isTrue_ex_of_isTrue_all {i : ℕ} {φ : QBF} (h : (all i φ).IsTrue) :
                    (ex i φ).IsTrue

                    Universal implies existential: over the (nonempty) Boolean domain, if ∀ x_i, φ is true then ∃ x_i, φ is true.

                    source
                    theorem Complexity.QBF.isTrue_neg_iff (φ : QBF) :
                    φ.neg.IsTrue ↔ ¬φ.IsTrue

                    Truth of a negation: ¬φ is true iff φ is not (the TQBF membership rule for negation).

                    source
                    theorem Complexity.QBF.isTrue_conj_iff (φ ψ : QBF) :
                    (φ.conj ψ).IsTrue ↔ φ.IsTrue ∧ ψ.IsTrue

                    Truth of a conjunction distributes: φ ∧ ψ is true iff both are.

                    source
                    theorem Complexity.QBF.isTrue_disj_iff (φ ψ : QBF) :
                    (φ.disj ψ).IsTrue ↔ φ.IsTrue ∨ ψ.IsTrue

                    Truth of a disjunction distributes: φ ∨ ψ is true iff at least one is.

                    source
                    theorem Complexity.QBF.eval_neg_ex (α : ℕ → Bool) (i : ℕ) (φ : QBF) :
                    eval α (ex i φ).neg = eval α (all i φ.neg)

                    Quantifier De Morgan (¬∃ = ∀¬): ¬(∃ x_i, φ) is equivalent to ∀ x_i, ¬φ.

                    source
                    theorem Complexity.QBF.eval_neg_all (α : ℕ → Bool) (i : ℕ) (φ : QBF) :
                    eval α (all i φ).neg = eval α (ex i φ.neg)

                    Quantifier De Morgan (¬∀ = ∃¬): ¬(∀ x_i, φ) is equivalent to ∃ x_i, ¬φ.