Depth-three formulas for parity

Each formula in an OR of formulas in conjunctive normal form computing a function g has its solutions among the true inputs of g, so an isolated true input of g is an isolated solution of one of the formulas. The satisfiability coding lemma bounds those, and so the formulas in an OR for parity, whose 2 ^ (n - 1) true inputs are all isolated.

Bottom fan-in k. A formula of width k has at most 2 ^ ((1 - 1 / k) n) isolated solutions, so an OR of such formulas needs a formula per 2 ^ ((1 - 1 / k) n) isolated true inputs (CNF.card_isolatedInputs_mul_two_rpow_le_of_any), as in the proof of Paturi, Pudlák and Zane, Theorem 6. For parity this is 2 ^ (n / k - 1) (CNF.two_rpow_le_length_of_any_eval_eq_parity), and the bound is attained when k divides n: split the variables into blocks of k and take one formula for each pattern of block parities with odd total (CNF.exists_any_eval_eq_parity), as in the example after Paturi, Pudlák and Zane, Lemma 4.

Unbounded bottom fan-in Paturi, Pudlák and Zane, Theorem 6. Weigh a solution x of a formula by w(x) = ∑ᵢ 1 / ℓᵢ, where ℓᵢ is the number of variables of a shortest clause critical for the direction i at x. At most 2 ^ (n - μ) solutions of a formula have weight at least μ (CNF.card_filter_le_sum_inv_critWidth_mul_two_rpow_le). A clause with ℓ variables is critical for at most ℓ 2 ^ (n - ℓ) pairs of an input and a direction (CNF.card_filter_critical_prod_le), and t ↦ t 2 ^ (1 / t) is convex and decreasing up to log 2, so the shortest critical clauses of the inputs of weight below μ ≤ n log 2 number at least μ 2 ^ (n / μ) / 2 ^ n per input. So an OR of m formulas with K distinct clauses computing a function with s isolated true inputs has s min (2 ^ μ) (μ 2 ^ (n / μ)) ≤ 2 ^ n (m + K) (CNF.card_isolatedInputs_mul_min_le). With Paturi, Pudlák and Zane's μ = √n + (log₂ n) / 4, both 2 ^ μ and μ 2 ^ (n / μ) are at least n ^ (1 / 4) 2 ^ √n (CNF.card_isolatedInputs_mul_rpow_mul_two_rpow_sqrt_le), so ORs of formulas in conjunctive normal form for the parity of n ≥ 4 bits have m + K ≥ n ^ (1 / 4) 2 ^ (√n - 1) (CNF.rpow_mul_two_rpow_sqrt_sub_one_le_of_any_eval_eq_parity). Dually, ANDs of formulas in disjunctive normal form for parity negate to ORs for its negation, all of whose 2 ^ (n - 1) true inputs are isolated too, and need as many formulas and terms (DNF.rpow_mul_two_rpow_sqrt_sub_one_le_of_all_eval_eq_parity). The simpler μ = √n gives m + K ≥ 2 ^ (√n - 1) already for n ≥ 3 (CNF.two_rpow_sqrt_sub_one_le_of_any_eval_eq_parity).

Main results

• Cslib.Logic.PL.CNF.card_isolatedInputs_mul_two_rpow_le_of_any: ORs of formulas of width k need a formula per 2 ^ ((1 - 1 / k) n) isolated true inputs.
• Cslib.Logic.PL.CNF.two_rpow_le_length_of_any_eval_eq_parity, Cslib.Logic.PL.CNF.exists_any_eval_eq_parity: parity is an OR of 2 ^ (n / k - 1) but no fewer formulas of width k, when k divides n.
• Cslib.Logic.PL.CNF.card_isolatedInputs_mul_min_le, Cslib.Logic.PL.CNF.card_isolatedInputs_mul_rpow_mul_two_rpow_sqrt_le: ORs of formulas need n ^ (1 / 4) 2 ^ √n / 2 ^ n formulas and clauses per isolated true input.
• Cslib.Logic.PL.CNF.rpow_mul_two_rpow_sqrt_sub_one_le_of_any_eval_eq_parity, Cslib.Logic.PL.DNF.rpow_mul_two_rpow_sqrt_sub_one_le_of_all_eval_eq_parity: depth-three formulas for parity need n ^ (1 / 4) 2 ^ (√n - 1) gates.
• Cslib.Logic.PL.CNF.two_pow_mul_min_le_of_any_eval_eq_parity, Cslib.Logic.PL.CNF.two_rpow_sqrt_sub_one_le_of_any_eval_eq_parity: the bound for parity at every μ, and at μ = √n.

References

• R. Paturi, P. Pudlák, F. Zane, Satisfiability Coding Lemma

Bottom fan-in k

theorem Cslib.Logic.PL.CNF.card_isolatedInputs_mul_two_rpow_le_of_any {n k : ℕ} (hk1 : 1 ≤ k) {g : BitString n → Bool} {Fs : List (CNF (Fin n))} (hk : ∀ φ ∈ Fs, ∀ c ∈ φ, List.length c ≤ k) (hFs : ∀ (x : Fin n → Bool), (Fs.any fun (φ : CNF (Fin n)) => eval x φ) = g x) : ↑(BitString.isolatedInputs g true).card * 2 ^ (↑n / ↑k) ≤ ↑Fs.length * 2 ^ n

ORs of formulas of width k in conjunctive normal form need many formulas, by the argument of Paturi, Pudlák and Zane, Theorem 6: if an OR of formulas whose clauses have at most k ≥ 1 literals computes g, then each isolated true input of g is a solution of one of them, isolated in every direction, and each of them has at most 2 ^ ((1 - 1 / k) n) such solutions (CNF.card_isolatedInputs_mul_two_rpow_le).

theorem Cslib.Logic.PL.CNF.two_rpow_le_length_of_any_eval_eq_parity {n : ℕ} (hn : 1 ≤ n) {k : ℕ} (hk1 : 1 ≤ k) {Fs : List (CNF (Fin n))} (hk : ∀ φ ∈ Fs, ∀ c ∈ φ, List.length c ≤ k) (hFs : ∀ (x : Fin n → Bool), (Fs.any fun (φ : CNF (Fin n)) => eval x φ) = parity n x) : 2 ^ (↑n / ↑k - 1) ≤ ↑Fs.length

ORs of formulas of width k in conjunctive normal form for parity of n ≥ 1 bits have at least 2 ^ (n / k - 1) formulas.

theorem Cslib.Logic.PL.CNF.exists_any_eval_eq_parity {n k : ℕ} (hk1 : 1 ≤ k) (hkn : k ∣ n) (hn : 1 ≤ n) : ∃ (Fs : List (CNF (Fin n))), Fs.length = 2 ^ (n / k - 1) ∧ (∀ φ ∈ Fs, ∀ c ∈ φ, List.length c ≤ k) ∧ ∀ (x : Fin n → Bool), (Fs.any fun (φ : CNF (Fin n)) => eval x φ) = parity n x

Parity is an OR of 2 ^ (n / k - 1) formulas of width k in conjunctive normal form when k divides n, after Paturi, Pudlák and Zane, Lemma 4: split the variables into n / k blocks of k; for each pattern of block parities with odd total, a formula of width k says that the blocks have these parities. So two_rpow_le_length_of_any_eval_eq_parity is attained.

Unbounded bottom fan-in

theorem Cslib.Logic.PL.CNF.card_isolatedInputs_mul_min_le {n : ℕ} {μ : ℝ} (hμ : 0 < μ) (hμn : μ ≤ ↑n * Real.log 2) {g : BitString n → Bool} {Fs : List (CNF (Fin n))} (hFs : ∀ (x : Fin n → Bool), (Fs.any fun (φ : CNF (Fin n)) => eval x φ) = g x) : ↑(BitString.isolatedInputs g true).card * min (2 ^ μ) (μ * 2 ^ (↑n / μ)) ≤ 2 ^ n * (↑Fs.length + ↑(List.map List.toFinset Fs.flatten).toFinset.card)

ORs of formulas in conjunctive normal form need many gates per isolated true input, by the argument of Paturi, Pudlák and Zane, Theorem 6: if an OR of m formulas with K distinct clauses (as sets of literals) computes g, then each isolated true input of g is a solution of one of them, isolated in every direction, and if there are s of them then s min (2 ^ μ) (μ 2 ^ (n / μ)) ≤ 2 ^ n (m + K) for every 0 < μ ≤ n log 2. A depth-three circuit with an OR at the top, AND gates in the middle and OR gates of literals at the bottom has at least m + K gates, as sharing bottom gates only lowers K.

theorem Cslib.Logic.PL.CNF.two_pow_mul_min_le_of_any_eval_eq_parity {n : ℕ} (hn : 1 ≤ n) {μ : ℝ} (hμ : 0 < μ) (hμn : μ ≤ ↑n * Real.log 2) {Fs : List (CNF (Fin n))} (hFs : ∀ (x : Fin n → Bool), (Fs.any fun (φ : CNF (Fin n)) => eval x φ) = parity n x) : 2 ^ (n - 1) * min (2 ^ μ) (μ * 2 ^ (↑n / μ)) ≤ 2 ^ n * (↑Fs.length + ↑(List.map List.toFinset Fs.flatten).toFinset.card)

ORs of formulas in conjunctive normal form for parity need many gates: if an OR of m formulas with K distinct clauses computes the parity of n ≥ 1 bits, all of whose 2 ^ (n - 1) true inputs are isolated, then 2 ^ (n - 1) min (2 ^ μ) (μ 2 ^ (n / μ)) ≤ 2 ^ n (m + K) for every 0 < μ ≤ n log 2.

theorem Cslib.Logic.PL.CNF.two_rpow_sqrt_sub_one_le_of_any_eval_eq_parity {n : ℕ} (hn : 3 ≤ n) {Fs : List (CNF (Fin n))} (hFs : ∀ (x : Fin n → Bool), (Fs.any fun (φ : CNF (Fin n)) => eval x φ) = parity n x) : 2 ^ (√↑n - 1) ≤ ↑Fs.length + ↑(List.map List.toFinset Fs.flatten).toFinset.card

ORs of formulas in conjunctive normal form for parity need 2 ^ (√n - 1) gates, taking μ = √n in CNF.two_pow_mul_min_le_of_any_eval_eq_parity: an OR of m formulas with K distinct clauses computing the parity of n ≥ 3 bits has 2 ^ (√n - 1) ≤ m + K. For n ≥ 4 this is weaker than CNF.rpow_mul_two_rpow_sqrt_sub_one_le_of_any_eval_eq_parity by the factor n ^ (1 / 4).

theorem Cslib.Logic.PL.CNF.card_isolatedInputs_mul_rpow_mul_two_rpow_sqrt_le {n : ℕ} (hn : 4 ≤ n) {g : BitString n → Bool} {Fs : List (CNF (Fin n))} (hFs : ∀ (x : Fin n → Bool), (Fs.any fun (φ : CNF (Fin n)) => eval x φ) = g x) : ↑(BitString.isolatedInputs g true).card * (↑n ^ (1 / 4) * 2 ^ √↑n) ≤ 2 ^ n * (↑Fs.length + ↑(List.map List.toFinset Fs.flatten).toFinset.card)

An OR of formulas in conjunctive normal form spends n ^ (1 / 4) 2 ^ √n / 2 ^ n gates per isolated true input, as in Paturi, Pudlák and Zane, Theorem 6: an OR of m formulas with K distinct clauses computing a function g of n ≥ 4 bits with s isolated true inputs has s n ^ (1 / 4) 2 ^ √n ≤ 2 ^ n (m + K). Take μ = √n + (log₂ n) / 4 in CNF.card_isolatedInputs_mul_min_le: then 2 ^ μ = n ^ (1 / 4) 2 ^ √n, and n / μ ≥ √n - (log₂ n) / 4 gives μ 2 ^ (n / μ) ≥ √n 2 ^ √n / n ^ (1 / 4) = n ^ (1 / 4) 2 ^ √n.

theorem Cslib.Logic.PL.CNF.rpow_mul_two_rpow_sqrt_sub_one_le_of_any_eval_eq_parity {n : ℕ} (hn : 4 ≤ n) {Fs : List (CNF (Fin n))} (hFs : ∀ (x : Fin n → Bool), (Fs.any fun (φ : CNF (Fin n)) => eval x φ) = parity n x) : ↑n ^ (1 / 4) * 2 ^ (√↑n - 1) ≤ ↑Fs.length + ↑(List.map List.toFinset Fs.flatten).toFinset.card

ORs of formulas in conjunctive normal form for parity need n ^ (1 / 4) 2 ^ (√n - 1) gates, Paturi, Pudlák and Zane, Theorem 6: an OR of m formulas with K distinct clauses computing the parity of n ≥ 4 bits has n ^ (1 / 4) 2 ^ (√n - 1) ≤ m + K, as all 2 ^ (n - 1) true inputs of parity are isolated.

theorem Cslib.Logic.PL.DNF.rpow_mul_two_rpow_sqrt_sub_one_le_of_all_eval_eq_parity {n : ℕ} (hn : 4 ≤ n) {Gs : List (DNF (Fin n))} (hGs : ∀ (x : Fin n → Bool), (Gs.all fun (ψ : DNF (Fin n)) => eval x ψ) = parity n x) : ↑n ^ (1 / 4) * 2 ^ (√↑n - 1) ≤ ↑Gs.length + ↑(List.map List.toFinset Gs.flatten).toFinset.card

ANDs of formulas in disjunctive normal form for parity need n ^ (1 / 4) 2 ^ (√n - 1) gates, the dual case of Paturi, Pudlák and Zane, Theorem 6: an AND of m formulas with K distinct terms computing the parity of n ≥ 4 bits has n ^ (1 / 4) 2 ^ (√n - 1) ≤ m + K. Negating it gives an OR of m formulas in conjunctive normal form with at most K distinct clauses computing the negation of parity, all of whose 2 ^ (n - 1) true inputs are isolated.