Depth-three formulas of bottom fan-in k

A Σ₃^k formula for f is an OR of formulas in conjunctive normal form of width at most k computing f (IsSigmaThree), and Σ₃^k(f) is the least number of formulas in one (sigmaThreeSize); dually Π₃^k(f) = Σ₃^k(¬f) (IsPiThree, piThreeSize_eq_sigmaThreeSize_not). If the true inputs of f contain no subcube of dimension D, neither do the solutions of any formula in an OR computing f, so the bound on such formulas gives |f⁻¹(1)| ≤ Σ₃^k(f) · 2 ^ ((1 - 1 / k + ε) N + C D) (card_filter_le_sigmaThreeSize_mul). For a family of functions with 2 ^ (n - o(n)) true inputs containing no subcube of dimension o(n) (a subcube disperser), Σ₃^k(f) ≥ 2 ^ ((1 / k - ε) n) for all large n (eventually_two_rpow_le_sigmaThreeSize). The exponent 1 / k cannot be improved: parity has no subcube of dimension one among its true inputs, and is an OR of 2 ^ (n / k - 1) formulas of width k when k divides n (CNF.exists_any_eval_eq_parity).

Main definitions

• Cslib.Logic.PL.IsSigmaThree, Cslib.Logic.PL.IsPiThree: depth-three formulas of bottom fan-in k.
• Cslib.Logic.PL.sigmaThreeSize, Cslib.Logic.PL.piThreeSize: Σ₃^k(f) and Π₃^k(f).

Main results

• Cslib.Logic.PL.piThreeSize_eq_sigmaThreeSize_not: De Morgan duality.
• Cslib.Logic.PL.card_filter_le_sigmaThreeSize_mul: the finite bound.
• Cslib.Logic.PL.eventually_two_rpow_le_sigmaThreeSize, Cslib.Logic.PL.eventually_two_rpow_le_piThreeSize: subcube dispersers need 2 ^ ((1/k - ε) n) formulas.

References

• R. Paturi, P. Pudlák, F. Zane, Satisfiability coding lemma
• R. Impagliazzo, R. Paturi, F. Zane, Which problems have strongly exponential complexity?

def Cslib.Logic.PL.IsSigmaThree {N : ℕ} (k : ℕ) (f : BitString N → Bool) (Fs : List (CNF (Fin N))) : Prop

Fs is a Σ₃^k formula for f: an OR of formulas in conjunctive normal form of width at most k computing f.

def Cslib.Logic.PL.IsPiThree {N : ℕ} (k : ℕ) (f : BitString N → Bool) (Gs : List (DNF (Fin N))) : Prop

Gs is a Π₃^k formula for f: an AND of formulas in disjunctive normal form of width at most k computing f.

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

Σ₃^k(f): the least number of formulas in a Σ₃^k formula for f; there is one for k ≥ 1 (exists_isSigmaThree).

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

Π₃^k(f): the least number of formulas in a Π₃^k formula for f.

def Cslib.Logic.PL.CNF.minterm {N : ℕ} (x : BitString N) : CNF (Fin N)

The formula accepting exactly x: one unit clause per variable.

theorem Cslib.Logic.PL.CNF.eval_minterm_eq_true_iff {N : ℕ} (x y : BitString N) : eval y (minterm x) = true ↔ y = x

theorem Cslib.Logic.PL.exists_isSigmaThree {N k : ℕ} (hk : 1 ≤ k) (f : BitString N → Bool) : ∃ (Fs : List (CNF (Fin N))), IsSigmaThree k f Fs

Every function has a Σ₃^k formula for k ≥ 1: the OR of the minterms of its true inputs.

theorem Cslib.Logic.PL.exists_isSigmaThree_length_eq_sigmaThreeSize {N k : ℕ} (hk : 1 ≤ k) (f : BitString N → Bool) : ∃ (Fs : List (CNF (Fin N))), IsSigmaThree k f Fs ∧ Fs.length = sigmaThreeSize k f

theorem Cslib.Logic.PL.sigmaThreeSize_le_length {N k : ℕ} {f : BitString N → Bool} {Fs : List (CNF (Fin N))} (h : IsSigmaThree k f Fs) : sigmaThreeSize k f ≤ Fs.length

theorem Cslib.Logic.PL.isPiThree_iff_isSigmaThree_map_negate {N k : ℕ} {f : BitString N → Bool} (Gs : List (DNF (Fin N))) : IsPiThree k f Gs ↔ IsSigmaThree k (fun (x : BitString N) => !f x) (List.map DNF.negate Gs)

De Morgan duality: an AND of formulas in disjunctive normal form computes f exactly when the OR of their negations, of the same widths, computes ¬f.

theorem Cslib.Logic.PL.piThreeSize_eq_sigmaThreeSize_not {N : ℕ} (k : ℕ) (f : BitString N → Bool) : piThreeSize k f = sigmaThreeSize k fun (x : BitString N) => !f x

Π₃^k(f) = Σ₃^k(¬f).

theorem Cslib.Logic.PL.card_filter_le_sigmaThreeSize_mul (k : ℕ) (hk : 1 ≤ k) {ε : ℝ} (hε : 0 < ε) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (N : ℕ) (f : BitString N → Bool) (D : ℕ), ¬ContainsSubcube {x : BitString N | f x = true} D → ↑{x : BitString N | f x = true}.card ≤ ↑(sigmaThreeSize k f) * 2 ^ ((1 - 1 / ↑k + ε) * ↑N + C * ↑D)

The finite bound for Σ₃^k: for k ≥ 1 and ε > 0 there is C ≥ 0 such that every f whose true inputs contain no subcube of dimension D has |f⁻¹(1)| ≤ Σ₃^k(f) · 2 ^ ((1 - 1 / k + ε) N + C D).

theorem Cslib.Logic.PL.eventually_two_rpow_le_sigmaThreeSize {f : (n : ℕ) → BitString n → Bool} {D : ℕ → ℕ} (hD : (fun (n : ℕ) => ↑(D n)) =o[Filter.atTop] fun (n : ℕ) => ↑n) (hfree : ∀ᶠ (n : ℕ) in Filter.atTop, ¬ContainsSubcube {x : BitString n | f n x = true} (D n)) (hdense : (fun (n : ℕ) => ↑n * Real.log 2 - Real.log ↑{x : BitString n | f n x = true}.card) =o[Filter.atTop] fun (n : ℕ) => ↑n) {k : ℕ} (hk : 1 ≤ k) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, 2 ^ ((1 / ↑k - ε) * ↑n) ≤ ↑(sigmaThreeSize k (f n))

Subcube dispersers need many formulas: if the true inputs of f n eventually contain no subcube of dimension D n = o(n) and number 2 ^ (n - o(n)), then for every k ≥ 1 and ε > 0, Σ₃^k(f n) ≥ 2 ^ ((1 / k - ε) n) for all large n.

theorem Cslib.Logic.PL.eventually_two_rpow_le_piThreeSize {f : (n : ℕ) → BitString n → Bool} {D : ℕ → ℕ} (hD : (fun (n : ℕ) => ↑(D n)) =o[Filter.atTop] fun (n : ℕ) => ↑n) (hfree : ∀ᶠ (n : ℕ) in Filter.atTop, ¬ContainsSubcube {x : BitString n | f n x = false} (D n)) (hdense : (fun (n : ℕ) => ↑n * Real.log 2 - Real.log ↑{x : BitString n | f n x = false}.card) =o[Filter.atTop] fun (n : ℕ) => ↑n) {k : ℕ} (hk : 1 ≤ k) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, 2 ^ ((1 / ↑k - ε) * ↑n) ≤ ↑(piThreeSize k (f n))

Dually for Π₃^k: if the false inputs of f n eventually contain no subcube of dimension o(n) and number 2 ^ (n - o(n)), then Π₃^k(f n) ≥ 2 ^ ((1 / k - ε) n) for all large n.