Normal Forms: CNF/DNF Lower Bound for XOR

Any CNF or DNF formula computing the N-input XOR function requires at least 2^{N-1} clauses (respectively terms).

The proof shows that every DNF for a flip-sensitive function must have each satisfying term mention all N variables, making the terms injective on the 2^{N-1}-element true-set. The CNF case reduces to the DNF case via De Morgan duality (CNF.neg).

Definitions (from Complexitylib.Circuits.NormalForm.Defs)

• Literal — a Boolean variable with a polarity flag
• CNF — conjunction of clauses (disjunctions of literals)
• DNF — disjunction of terms (conjunctions of literals)
• CNF.complexity / DNF.complexity — clause/term count
• CNF.toCircuit / DNF.toCircuit — 2-level AON circuit embedding

Main results

• DNF.two_pow_le_complexity_of_xorBool — any DNF computing XOR has ≥ 2^{N-1} terms
• CNF.two_pow_le_complexity_of_xorBool — any CNF computing XOR has ≥ 2^{N-1} clauses

theorem Complexity.DNF.two_pow_le_complexity_of_xorBool {N : ℕ} (φ : DNF N) (hN : 1 ≤ N) (hcomp : ∀ (x : BitString N), φ.eval x = Schnorr.xorBool N x) : 2 ^ (N - 1) ≤ φ.complexity

Any DNF computing N-variable XOR requires at least 2^{N-1} terms.

theorem Complexity.CNF.two_pow_le_complexity_of_xorBool {N : ℕ} (φ : CNF N) (hN : 1 ≤ N) (hcomp : ∀ (x : BitString N), φ.eval x = Schnorr.xorBool N x) : 2 ^ (N - 1) ≤ φ.complexity

Any CNF computing N-variable XOR requires at least 2^{N-1} clauses.