Depth-three formulas with bounded bottom fan-in -- definitions

A Σ₃^k formula is an OR of CNFs of width at most k: a depth-three OR-AND-OR formula whose bottom gates have fan-in at most k. Its size is the number of CNFs (the top fan-in). Dually, a Π₃^k formula is an AND of DNFs of width at most k. The CNFs and DNFs are the library's Complexity.CNF and Complexity.DNF; the size measures count only the top gate's inputs, so they lower-bound every reasonable size measure of these formulas.

Main definitions

• IsSigmaThree k f Fs: the OR of the CNFs Fs, each of width at most k, computes f.
• IsPiThree k f Gs: the AND of the DNFs Gs, each of width at most k, computes f.
• sigmaThreeSize k f, piThreeSize k f: the least number of CNFs, respectively DNFs, in such a formula for f (Σ₃^k(f) and Π₃^k(f)).

def Complexity.IsSigmaThree {N : ℕ} (k : ℕ) (f : BitString N → Bool) (Fs : List (CNF N)) : Prop

Fs is a Σ₃^k formula for f: an OR of CNFs, each of width at most k, that computes f.

Equations

• Complexity.IsSigmaThree k f Fs = ((∀ F ∈ Fs, F.width ≤ k) ∧ ∀ (x : Complexity.BitString N), f x = Fs.any fun (F : Complexity.CNF N) => F.eval x)

def Complexity.IsPiThree {N : ℕ} (k : ℕ) (f : BitString N → Bool) (Gs : List (DNF N)) : Prop

Gs is a Π₃^k formula for f: an AND of DNFs, each of width at most k, that computes f.

Equations

• Complexity.IsPiThree k f Gs = ((∀ G ∈ Gs, G.width ≤ k) ∧ ∀ (x : Complexity.BitString N), f x = Gs.all fun (G : Complexity.DNF N) => G.eval x)

noncomputable def Complexity.sigmaThreeSize {N : ℕ} (k : ℕ) (f : BitString N → Bool) : ℕ

Σ₃^k(f): the least number of CNFs of width at most k whose OR computes f. For k ≥ 1 such formulas exist (Complexity.exists_isSigmaThree).

Equations

• Complexity.sigmaThreeSize k f = sInf {t : ℕ | ∃ (Fs : List (Complexity.CNF N)), Complexity.IsSigmaThree k f Fs ∧ Fs.length = t}

noncomputable def Complexity.piThreeSize {N : ℕ} (k : ℕ) (f : BitString N → Bool) : ℕ

Π₃^k(f): the least number of DNFs of width at most k whose AND computes f.

Equations

• Complexity.piThreeSize k f = sInf {t : ℕ | ∃ (Gs : List (Complexity.DNF N)), Complexity.IsPiThree k f Gs ∧ Gs.length = t}