Documentation

Complexitylib.Circuits.Formula

Boolean formulas and formula size #

Boolean formulas as trees over ∧, ∨, ¬, variables, and constants, with a tree size (total node count) and leaves count (roadmap track L4). Formula size is deliberately kept separate from DAG circuit size: a formula counts every occurrence of a subformula, whereas a DAG-shaped Circuit may share a subcircuit among several parents. Consequently formula size can be exponentially larger than the size of an equivalent circuit, and the two measures must not be conflated in lower-bound arguments.

Main definitions and results #

source
inductive Complexity.BoolFormula :
Type

A Boolean formula: a tree over variables, the constants ⊤/⊥, and the connectives ¬, ∧, ∨. Unlike a Circuit, subformulas are not shared.

Instances For
    source
    def Complexity.instReprBoolFormula.repr :
    BoolFormula → ℕ → Std.Format
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[implicit_reducible]
      instance Complexity.instReprBoolFormula :
      Repr BoolFormula
      Equations
      source
      @[implicit_reducible]
      instance Complexity.instDecidableEqBoolFormula :
      DecidableEq BoolFormula
      Equations
      source
      def Complexity.instDecidableEqBoolFormula.decEq (x✝ x✝¹ : BoolFormula) :
      Decidable (x✝ = x✝¹)
      Equations
      Instances For
        source
        def Complexity.BoolFormula.eval (α : ℕ → Bool) :
        BoolFormula → Bool

        Evaluate a formula under an assignment α : ℕ → Bool.

        Equations
        Instances For
          source
          def Complexity.BoolFormula.size :
          BoolFormula → ℕ

          The tree size: the total number of nodes (leaves and connectives).

          Equations
          Instances For
            source
            def Complexity.BoolFormula.leaves :
            BoolFormula → ℕ

            The number of leaf nodes (variables and constants).

            Equations
            Instances For
              source
              def Complexity.BoolFormula.depth :
              BoolFormula → ℕ

              The depth of a formula: the longest root-to-leaf path (the NC¹ complexity measure). Leaves have depth 0; each connective adds 1.

              Equations
              Instances For
                source
                def Complexity.BoolFormula.vars :
                BoolFormula → Finset ℕ

                The set of variables occurring in a formula.

                Equations
                Instances For
                  source
                  theorem Complexity.BoolFormula.one_le_size (φ : BoolFormula) :
                  1 ≤ φ.size

                  Every formula has at least one node.

                  source
                  theorem Complexity.BoolFormula.leaves_le_size (φ : BoolFormula) :
                  φ.leaves ≤ φ.size

                  The leaf count never exceeds the tree size (leaves are among the nodes).

                  source
                  theorem Complexity.BoolFormula.leaves_le_two_pow_depth (φ : BoolFormula) :
                  φ.leaves ≤ 2 ^ φ.depth

                  A formula of depth d has at most 2 ^ d leaves (a depth-d binary tree has at most 2 ^ d leaves).

                  source
                  theorem Complexity.BoolFormula.size_lt_two_pow_depth_succ (φ : BoolFormula) :
                  φ.size < 2 ^ (φ.depth + 1)

                  A formula of depth d has fewer than 2 ^ (d + 1) total nodes. This is the tree-size counterpart of leaves_le_two_pow_depth.

                  source
                  theorem Complexity.BoolFormula.depth_le_size (φ : BoolFormula) :
                  φ.depth ≤ φ.size

                  Depth never exceeds size: a longest path uses at most every node.

                  source
                  theorem Complexity.BoolFormula.eval_eq_of_agree (φ : BoolFormula) {α β : ℕ → Bool} :
                  (∀ i ∈ φ.vars, α i = β i) → eval α φ = eval β φ

                  Locality. A formula's value depends only on the variables that occur in it: if two assignments agree on vars φ, they give φ the same value.

                  source
                  theorem Complexity.BoolFormula.eval_const_of_vars_empty {φ : BoolFormula} (hv : φ.vars = ∅) (α β : ℕ → Bool) :
                  eval α φ = eval β φ

                  A formula with no variables evaluates to a constant: its value is assignment-independent (a corollary of locality).