Haken's resolution lower bound for the pigeonhole principle

Haken proved that resolution refutations of the pigeonhole formula PHP^{n+1}_n (Cslib.Logic.PL.CNF.pigeonhole (n + 1) n) have exponential size. This file follows the simplified proof of Beame and Pitassi (see also [Jukna, Section 18.6] [Juk12]), replacing random restrictions by a greedy choice of one pigeon–hole pair at a time.

Let P ⊆ Fin m and H ⊆ Fin n be sets of remaining pigeons and holes with #P = #H + 1, and let pigeonholeOn P H be the pigeonhole formula restricted to P and H.

1. Critical assignments and the width of the monotone translation. A critical assignment (Cslib.Logic.PL.Pigeonhole.IsCrit) is an injection g : H → P; its truth assignment (Cslib.Logic.PL.Pigeonhole.critAssign) places g j in hole j for each j ∈ H and leaves a single pigeon i₀ ∈ P \ H.image g outside all holes. Let falsifiedPigeons P H c be the set of pigeons i₀ ∈ P that are left out by some critical assignment falsifying c. Each clause of pigeonholeOn P H has #(falsifiedPigeons P H c) ≤ 1, resolution steps are subadditive, and the empty clause has falsifiedPigeons P H [] = P, so every refutation contains a line c with #P ≤ 3 #(falsifiedPigeons P H c) ≤ 2 #P (for #H ≥ 1), giving 2 (#H)² ≤ 9 #(falsifiedPigeons P H c) (#P - #(falsifiedPigeons P H c)).

   For i₀ ∈ falsifiedPigeons P H c (witnessed by g) and j ∈ H with g j ∈ P \ falsifiedPigeons P H c, updating g at j to i₀ gives a critical assignment with missing pigeon g j, which must satisfy c. Any literal of c that flips from false to true under this swap lies in column j and is satisfied by the partial assignment matchPair i₀ j that matches i₀ to j. Thus (i₀, j) belongs to satPairs P H c, the set of pairs in P ×ˢ H whose matching assignment satisfies c, so #(falsifiedPigeons P H c) (#P - #(falsifiedPigeons P H c)) ≤ #(satPairs P H c) and every refutation of pigeonholeOn P H contains a line with 2 (#H)² ≤ 9 #(satPairs P H c) (Cslib.Logic.PL.Pigeonhole.exists_le_card_satPairs).

2. Eliminating wide lines by matching one pair at a time. Restricting a proof from pigeonholeOn P H by matchPair i₀ j₀ (Cslib.Logic.PL.CNF.IsProof.restrictBy) yields a proof from pigeonholeOn (P.erase i₀) (H.erase j₀) whose lines are subclauses of a sublist of the lines not satisfied by matchPair i₀ j₀. Since satPairs is monotone in P, H, and the clause, choosing (i₀, j₀) ∈ P ×ˢ H by averaging reduces the number f of lines with d ≤ #(satPairs P H c) to f' with C f' ≤ (C - 1) f whenever #P · #H ≤ C d. After t = n / 3 steps from PHP^{n+1}_n with d = 2 (n - n / 3)² / 9 and C = 12 (for n ≥ 8), a line with d ≤ #(satPairs P_t H_t c) still remains, so 12 ^ (n / 3) ≤ 11 ^ (n / 3) · s (Cslib.Logic.PL.CNF.pow_le_mul_of_refutableInSize_pigeonhole) and 2 ^ (n / 24) ≤ s for all n (Cslib.Logic.PL.CNF.two_pow_le_of_refutableInSize_pigeonhole).

Main definitions

• Cslib.Logic.PL.Pigeonhole.pigeonholeOn: the pigeonhole formula on subsets P and H.
• Cslib.Logic.PL.Pigeonhole.matchPair: the partial assignment matching a pigeon to a hole.
• Cslib.Logic.PL.Pigeonhole.satPairs: the pairs in P ×ˢ H whose matching assignment satisfies a clause (its monotone translation).
• Cslib.Logic.PL.Pigeonhole.IsCrit, Cslib.Logic.PL.Pigeonhole.critAssign, Cslib.Logic.PL.Pigeonhole.falsifiedPigeons: critical assignments and the missing pigeons of critical assignments falsifying a clause.

Main results

• Cslib.Logic.PL.Pigeonhole.exists_le_card_satPairs: every refutation of pigeonholeOn P H (with #P = #H + 1) has a line c with 2 (#H)² ≤ 9 #(satPairs P H c).
• Cslib.Logic.PL.CNF.pow_le_mul_of_refutableInSize_pigeonhole: for n ≥ 8, every resolution refutation of PHP^{n+1}_n of s lines satisfies 12 ^ (n / 3) ≤ 11 ^ (n / 3) · s.
• Cslib.Logic.PL.CNF.two_pow_le_of_refutableInSize_pigeonhole, Cslib.Logic.PL.CNF.not_refutableInSize_pigeonhole: Haken's theorem: every resolution refutation of PHP^{n+1}_n has at least 2 ^ (n / 24) lines.
• Cslib.Logic.PL.CNF.Derivation.two_pow_le_size_pigeonhole: the same lower bound for tree-like resolution refutations.

References

• A. Haken, The intractability of resolution
• P. Beame, T. Pitassi, Simplified and improved resolution lower bounds
• S. Jukna, Boolean Function Complexity: Advances and Frontiers, Section 18.6

Pigeonhole formulas on subsets of pigeons and holes

def Cslib.Logic.PL.Pigeonhole.pigeonClauseOn {m n : ℕ} (H : Finset (Fin n)) (i : Fin m) : Clause (Fin m × Fin n)

The pigeon clause of pigeon i restricted to the holes H.

def Cslib.Logic.PL.Pigeonhole.pigeonholeOn {m n : ℕ} (P : Finset (Fin m)) (H : Finset (Fin n)) : CNF (Fin m × Fin n)

The pigeonhole formula restricted to the pigeons P and holes H.

@[simp]

theorem Cslib.Logic.PL.Pigeonhole.pigeonClauseOn_univ {m n : ℕ} (i : Fin m) : pigeonClauseOn Finset.univ i = CNF.pigeonClause n i

@[simp]

theorem Cslib.Logic.PL.Pigeonhole.pigeonholeOn_univ {m n : ℕ} : pigeonholeOn Finset.univ Finset.univ = CNF.pigeonhole m n

theorem Cslib.Logic.PL.Pigeonhole.mem_pigeonholeOn {m n : ℕ} {P : Finset (Fin m)} {H : Finset (Fin n)} {c : Clause (Fin m × Fin n)} : c ∈ pigeonholeOn P H ↔ (∃ i ∈ P, c = pigeonClauseOn H i) ∨ ∃ i ∈ P, ∃ i' ∈ P, ∃ j ∈ H, i < i' ∧ c = CNF.holeClause i i' j

The clauses of pigeonholeOn P H are its pigeon clauses and its hole clauses on P and H.

@[simp]

theorem Cslib.Logic.PL.Pigeonhole.eval_pigeonClauseOn {m n : ℕ} (σ : Fin m × Fin n → Bool) (H : Finset (Fin n)) (i : Fin m) : Clause.eval σ (pigeonClauseOn H i) = true ↔ ∃ j ∈ H, σ (i, j) = true

Matching a pigeon to a hole

def Cslib.Logic.PL.Pigeonhole.matchPair {m n : ℕ} (i : Fin m) (j : Fin n) (v : Fin m × Fin n) : Option Bool

The partial assignment matching pigeon i to hole j: (i, j) is set to true, and all other variables in row i or column j are set to false.

@[simp]

theorem Cslib.Logic.PL.Pigeonhole.matchPair_self {m n : ℕ} (i : Fin m) (j : Fin n) : matchPair i j (i, j) = some true

theorem Cslib.Logic.PL.Pigeonhole.matchPair_eq_none {m n : ℕ} {i : Fin m} {j : Fin n} {v : Fin m × Fin n} : matchPair i j v = none ↔ v.1 ≠ i ∧ v.2 ≠ j

Critical assignments and the monotone width bound

def Cslib.Logic.PL.Pigeonhole.IsCrit {m n : ℕ} (P : Finset (Fin m)) (H : Finset (Fin n)) (g : Fin n → Fin m) : Prop

g is a critical assignment of the holes H into the pigeons P: it maps H injectively into P. When #P = #H + 1, this leaves out a single pigeon of P.

def Cslib.Logic.PL.Pigeonhole.critAssign {m n : ℕ} (H : Finset (Fin n)) (g : Fin n → Fin m) (v : Fin m × Fin n) : Bool

The truth assignment of a hole-to-pigeon map g on the holes H: (i, j) is true when j ∈ H and g j = i.

def Cslib.Logic.PL.Pigeonhole.satPairs {m n : ℕ} (P : Finset (Fin m)) (H : Finset (Fin n)) (c : Clause (Fin m × Fin n)) : Finset (Fin m × Fin n)

The pairs (i, j) ∈ P ×ˢ H whose matching assignment matchPair i j satisfies a literal of c. This is the monotone translation of c (together with row-negation pairs).

noncomputable def Cslib.Logic.PL.Pigeonhole.falsifiedPigeons {m n : ℕ} (P : Finset (Fin m)) (H : Finset (Fin n)) (c : Clause (Fin m × Fin n)) : Finset (Fin m)

The pigeons of P that can be the missing pigeon of a critical assignment falsifying c.

theorem Cslib.Logic.PL.Pigeonhole.mem_falsifiedPigeons {m n : ℕ} {P : Finset (Fin m)} {H : Finset (Fin n)} {c : Clause (Fin m × Fin n)} {i : Fin m} : i ∈ falsifiedPigeons P H c ↔ i ∈ P ∧ ∃ (g : Fin n → Fin m), IsCrit P H g ∧ i ∉ Finset.image g H ∧ Clause.eval (critAssign H g) c = false

theorem Cslib.Logic.PL.Pigeonhole.falsifiedPigeons_subset {m n : ℕ} (P : Finset (Fin m)) (H : Finset (Fin n)) (c : Clause (Fin m × Fin n)) : falsifiedPigeons P H c ⊆ P

theorem Cslib.Logic.PL.Pigeonhole.exists_le_card_satPairs {m n : ℕ} {P : Finset (Fin m)} {H : Finset (Fin n)} (hP : P.card = H.card + 1) {ls : List (Clause (Fin m × Fin n))} (h : (pigeonholeOn P H).IsProof ls) (hnil : [] ∈ ls) : ∃ c ∈ ls, 2 * H.card ^ 2 ≤ 9 * (satPairs P H c).card

Every refutation of pigeonholeOn P H has a wide monotone line Beame and Pitassi, Lemma 4 Jukna, Lemma 18.17. When #P = #H + 1, every resolution refutation of pigeonholeOn P H contains a line c with 2 (#H)² ≤ 9 #(satPairs P H c).

Eliminating wide lines by greedy matching restrictions

Haken's lower bound for PHP^{n+1}_n

theorem Cslib.Logic.PL.CNF.exists_le_card_satPairs_pigeonhole {n : ℕ} {ls : List (Clause (Fin (n + 1) × Fin n))} (h : (pigeonhole (n + 1) n).IsProof ls) (hnil : [] ∈ ls) : ∃ c ∈ ls, 2 * n ^ 2 ≤ 9 * (Pigeonhole.satPairs Finset.univ Finset.univ c).card

Every resolution refutation of PHP^{n+1}_n contains a line whose monotone translation has at least 2 n² / 9 variable pairs Beame and Pitassi, Lemma 4.

theorem Cslib.Logic.PL.CNF.pow_le_mul_of_refutableInSize_pigeonhole {n : ℕ} (hn : 8 ≤ n) {s : ℕ} (hs : (pigeonhole (n + 1) n).RefutableInSize s) : 12 ^ (n / 3) ≤ 11 ^ (n / 3) * s

Haken's theorem (recurrence form) Haken Beame and Pitassi, Theorem 2 Jukna, Theorem 18.15. For n ≥ 8, every resolution refutation of PHP^{n+1}_n of s lines satisfies 12 ^ (n / 3) ≤ 11 ^ (n / 3) · s.

theorem Cslib.Logic.PL.CNF.two_pow_le_of_refutableInSize_pigeonhole {n s : ℕ} (hs : (pigeonhole (n + 1) n).RefutableInSize s) : 2 ^ (n / 24) ≤ s

Haken's theorem: every resolution refutation of PHP^{n+1}_n has at least 2 ^ (n / 24) lines Haken Beame and Pitassi Jukna, Theorem 18.15.

theorem Cslib.Logic.PL.CNF.not_refutableInSize_pigeonhole {n s : ℕ} (hs : s < 2 ^ (n / 24)) : ¬(pigeonhole (n + 1) n).RefutableInSize s

Haken's theorem: PHP^{n+1}_n has no resolution refutation with fewer than 2 ^ (n / 24) lines Haken Beame and Pitassi.

theorem Cslib.Logic.PL.CNF.Derivation.two_pow_le_size_pigeonhole {n : ℕ} (d : (pigeonhole (n + 1) n).Derivation []) : 2 ^ (n / 24) ≤ d.size

Tree-like resolution lower bound for PHP^{n+1}_n: every tree-like resolution refutation of PHP^{n+1}_n has at least 2 ^ (n / 24) nodes.