Normal forms for parity

An input x of a Boolean function g is an isolated true input when g x is true and g is false at every neighbour of x. A term of a formula in disjunctive normal form computing g that holds at an isolated true input mentions every variable, since flipping an unmentioned variable would keep it true; so it holds at no other input. Hence such a formula has at least as many terms as g has isolated true inputs (DNF.card_isolatedInputs_le_length), and dually a formula in conjunctive normal form has at least as many clauses as isolated false inputs. Every input is isolated for parity, so its normal forms on n ≥ 1 bits have at least 2 ^ (n - 1) terms or clauses (DNF.two_pow_le_length_of_eval_eq_parity, CNF.two_pow_le_length_of_eval_eq_parity). The same flip shows that a formula in disjunctive normal form whose terms have fewer literals than a partial assignment has free bits does not compute the parity of the bits it fills in, up to negation (DNF.not_forall_eval_eq_parity_fill_bne); this ends Håstad's argument for circuits of constant depth.

ORs of formulas in conjunctive normal form for parity, of depth three, are in Complexity/Logics/Propositional/Parity/DepthThree.lean.

Main results

• Cslib.Logic.PL.DNF.card_isolatedInputs_le_length, Cslib.Logic.PL.CNF.card_isolatedInputs_le_length: normal forms have a term or clause per isolated input.
• Cslib.Logic.PL.DNF.two_pow_le_length_of_eval_eq_parity, Cslib.Logic.PL.CNF.two_pow_le_length_of_eval_eq_parity: normal forms of parity have at least 2 ^ (n - 1) terms or clauses.
• Cslib.Logic.PL.DNF.not_forall_eval_eq_parity_fill_bne: narrow formulas in disjunctive normal form do not compute restricted parity.

References

• S. Jukna, Boolean Function Complexity: Advances and Frontiers

theorem Cslib.Logic.PL.DNF.card_isolatedInputs_le_length {n : ℕ} {g : BitString n → Bool} {D : DNF (Fin n)} (hD : ∀ (x : Fin n → Bool), eval x D = g x) : (BitString.isolatedInputs g true).card ≤ List.length D

A formula in disjunctive normal form has a term per isolated true input of the function it computes.

theorem Cslib.Logic.PL.CNF.card_isolatedInputs_le_length {n : ℕ} {g : BitString n → Bool} {φ : CNF (Fin n)} (hφ : ∀ (x : Fin n → Bool), eval x φ = g x) : (BitString.isolatedInputs g false).card ≤ List.length φ

A formula in conjunctive normal form has a clause per isolated false input of the function it computes: its negation is a formula in disjunctive normal form for the negated function.

theorem Cslib.Logic.PL.DNF.two_pow_le_length_of_eval_eq_parity {n : ℕ} (hn : 1 ≤ n) {D : DNF (Fin n)} (hD : ∀ (x : Fin n → Bool), eval x D = parity n x) : 2 ^ (n - 1) ≤ List.length D

Formulas in disjunctive normal form for parity of n ≥ 1 bits have at least 2 ^ (n - 1) terms.

theorem Cslib.Logic.PL.CNF.two_pow_le_length_of_eval_eq_parity {n : ℕ} (hn : 1 ≤ n) {φ : CNF (Fin n)} (hφ : ∀ (x : Fin n → Bool), eval x φ = parity n x) : 2 ^ (n - 1) ≤ List.length φ

Formulas in conjunctive normal form for parity of n ≥ 1 bits have at least 2 ^ (n - 1) clauses.

theorem Cslib.Logic.PL.DNF.not_forall_eval_eq_parity_fill_bne {n : ℕ} {ρ : BitString.PartialAssignment (Fin n)} {D : DNF (Fin n)} (hD : ∀ t ∈ D, List.length t < ρ.free.card) (hρ : ρ.free.Nonempty) (c : Bool) : ¬∀ (y : Fin n → Bool), eval y D = (parity n (ρ.fill y) != c)

Narrow formulas in disjunctive normal form miss restricted parity. If every term of D has fewer literals than ρ has free bits, and ρ has a free bit, then D does not compute the parity of the bits filled in by ρ, up to negation: a satisfied term misses a free bit, and flipping it keeps the term satisfied but flips the parity.