The switching lemma

Håstad's switching lemma: if every term of a formula F in disjunctive normal form has at most k literals and reads each variable once, then few restrictions (partial assignments, BitString.PartialAssignment) leaving ℓ variables free make the canonical decision tree of F deep. Precisely, at most #R(ℓ - s) (4k)^s of them leave a query path of length at least s (DNF.card_filter_pathLength_le), and so at most that many leave F with decision tree complexity at least s (DNF.card_switching_le), where R(m) is the set of restrictions of the n variables ι leaving m of them free. Since #R(ℓ - s) / #R(ℓ) is about (2ℓ / n) ^ s, a random restriction leaving ℓ ≪ n / k variables free turns F into a function of decision tree complexity less than s, except with probability exponentially small in s [Has86]. Both statements hold more generally among the extensions of any fixed restriction, which is the form used to restrict a formula in several stages.

We follow Razborov's proof by encoding [Raz95], Jukna, Chapter 12. A restriction ρ with a query path of length at least s on the input x is encoded by an extension of ρ with s fewer free variables, which fixes each of the first s queried variables to the value that satisfies the term it was queried for, together with a word of s letters from an alphabet of size 4k: the position of each queried variable in its term, its value in x, and whether it ends its stage (DNF.encode). Since the terms queried in the encoding are again the first terms not falsified, the decoder can replay the path (DNF.decode, DNF.decode_encode).

Main definitions

• Cslib.Logic.PL.DNF.encode, Cslib.Logic.PL.DNF.decode: Razborov's encoding of a restriction with a long query path.

Main results

• Cslib.Logic.PL.DNF.decode_encode: the encoding is invertible.
• Cslib.Logic.PL.DNF.card_filter_pathLength_le: few restrictions leave long query paths.
• Cslib.Logic.PL.DNF.card_switching_le: the switching lemma, counting version.

References

• J. Håstad, Almost optimal lower bounds for small depth circuits
• A. A. Razborov, Bounded arithmetic and lower bounds in Boolean complexity
• S. Jukna, Boolean Function Complexity: Advances and Frontiers

theorem Cslib.Logic.PL.Term.FalsifiedBy.mono {ι : Type u_1} {t : Term ι} {ρ θ : BitString.PartialAssignment ι} (ht : t.FalsifiedBy ρ) (h : θ.Extends ρ) : t.FalsifiedBy θ

A restriction falsifies more terms than any restriction it extends.

def Cslib.Logic.PL.Term.satisfying {ι : Type u_1} [DecidableEq ι] (t : Term ι) : ι → Bool

The values of the variables making the literals of t true.

def Cslib.Logic.PL.Term.stageCode {ι : Type u_1} [DecidableEq ι] (t : Term ι) (x : ι → Bool) : List ι → List (ℕ × Bool × Bool)

The code of one stage of the canonical path: for each queried variable, its position in the term, its value in x, and whether it ends the stage.

@[simp]

theorem Cslib.Logic.PL.Term.length_stageCode {ι : Type u_1} [DecidableEq ι] {t : Term ι} (x : ι → Bool) (W : List ι) : (t.stageCode x W).length = W.length

theorem Cslib.Logic.PL.Term.stageCode_eq_nil_iff {ι : Type u_1} [DecidableEq ι] {t : Term ι} {x : ι → Bool} {W : List ι} : t.stageCode x W = [] ↔ W = []

def Cslib.Logic.PL.DNF.decodeAux {ι : Type u_1} (F : DNF ι) [DecidableEq ι] : Option (Term ι) → BitString.PartialAssignment ι → Finset ι → List (ℕ × Bool × Bool) → BitString.PartialAssignment ι

Replay the canonical path from the code: cur is the term of the current stage, if the stage has started, θ the restriction so far, and Q the variables replayed so far.

def Cslib.Logic.PL.DNF.decode {ι : Type u_1} (F : DNF ι) [DecidableEq ι] (θ : BitString.PartialAssignment ι) (c : List (ℕ × Bool × Bool)) : BitString.PartialAssignment ι

Razborov's decoding: recover the restriction from its encoding.

@[irreducible]

def Cslib.Logic.PL.DNF.encode {ι : Type u_1} (F : DNF ι) [DecidableEq ι] [Fintype ι] (s : ℕ) (ρ : BitString.PartialAssignment ι) (x : ι → Bool) : BitString.PartialAssignment ι × List (ℕ × Bool × Bool)

Razborov's encoding of the first s queries of the canonical path of x from ρ: the restriction fixing the queried variables to the values satisfying their terms, and the code of the path.

theorem Cslib.Logic.PL.DNF.decode_encode {ι : Type u_1} {F : DNF ι} {ρ : BitString.PartialAssignment ι} [DecidableEq ι] [Fintype ι] (hF : ∀ t ∈ F, (List.map Prod.fst t).Nodup) {s : ℕ} {x : ι → Bool} (hs : s ≤ F.pathLength ρ x) : F.decode (F.encode s ρ x).1 (F.encode s ρ x).2 = ρ

Razborov's decoding. The encoding of a restriction with a query path of length at least s determines the restriction.

theorem Cslib.Logic.PL.DNF.card_filter_pathLength_le {ι : Type u_1} {F : DNF ι} [DecidableEq ι] [Fintype ι] {k : ℕ} (hk : ∀ t ∈ F, List.length t ≤ k) (hnd : ∀ t ∈ F, (List.map Prod.fst t).Nodup) (ρ₀ : BitString.PartialAssignment ι) (ℓ s : ℕ) : {ρ ∈ ρ₀.extensions ℓ | ∃ (x : ι → Bool), s ≤ F.pathLength ρ x}.card ≤ (ρ₀.extensions (ℓ - s)).card * (4 * k) ^ s

Counting bad extensions. Among the extensions of ρ₀ leaving ℓ variables free, at most #E(ℓ - s) (4k)^s have a canonical query path of length at least s, where E(m) are the extensions of ρ₀ leaving m variables free, if every term of F has at most k literals and reads each variable once.

theorem Cslib.Logic.PL.DNF.card_switching_le {ι : Type u_1} {F : DNF ι} [DecidableEq ι] [Fintype ι] {k : ℕ} (hk : ∀ t ∈ F, List.length t ≤ k) (hnd : ∀ t ∈ F, (List.map Prod.fst t).Nodup) (ρ₀ : BitString.PartialAssignment ι) (ℓ s : ℕ) : {ρ ∈ ρ₀.extensions ℓ | s ≤ DecisionTree.complexity fun (x : ι → Bool) => eval (ρ.fill x) F}.card ≤ (ρ₀.extensions (ℓ - s)).card * (4 * k) ^ s

Håstad's switching lemma, counting version. If every term of F has at most k literals and reads each variable once, then at most #E(ℓ - s) (4k)^s of the extensions of ρ₀ leaving ℓ variables free leave F with decision tree complexity at least s, where E(m) are the extensions of ρ₀ leaving m variables free. For ρ₀ fixing nothing, these are all restrictions (PartialAssignment.withFree).