Tseitin formulas on expanders are hard for resolution

A rotation map G (Cslib.RotationMap) is a multigraph with an edge for each pair of a dart and its reversal (Cslib.RotationMap.edgeEnds), and its edge expansion h(G) bounds the expansion e(G) of Ben-Sasson and Wigderson: h(G) |V| / 3 ≤ e(G) (Cslib.RotationMap.edgeExpansion_mul_card_div_three_le_minBalancedCut). If h(G) > 0, the multigraph is connected, and Tseitin formulas on it need resolution refutations of width at least h(G) |V| / 3 (Cslib.Logic.PL.Tseitin.edgeExpansion_mul_card_div_three_le_of_refutableInWidth) and, when |D| + 2 ≤ h(G) |V| / 3, of at least exp ((h(G) |V| / 3 - |D| - 2)² / (8 |V| |D|)) lines (Cslib.Logic.PL.Tseitin.exp_edgeExpansion_le_of_refutableInSize).

Constant-degree expanders (Cslib.RotationMap.expander) have 120 labels and edge expansion at least 1 / 6000 (Cslib.RotationMap.le_edgeExpansion_expander). Their Tseitin formulas with a single charged vertex form a family, with explicit constants, of unsatisfiable formulas with O(n) variables and clauses of constant width whose resolution refutations have 2 ^ Ω(n) lines (Cslib.Logic.PL.CNF.exists_forall_refutableInSize_exp_le) Urquhart Ben-Sasson and Wigderson. The expanders, and so the formulas, are obtained non-constructively, from a counting argument (Cslib.RotationMap.exists_spectralExpansion_le).

Main results

• Cslib.Logic.PL.Tseitin.edgeExpansion_mul_card_div_three_le_of_refutableInWidth, Cslib.Logic.PL.Tseitin.exp_edgeExpansion_le_of_refutableInSize: the width and size lower bounds for Tseitin formulas on rotation maps, in terms of edge expansion.
• Cslib.Logic.PL.CNF.exists_forall_refutableInSize_exp_le: for every n ≥ 4392000, an unsatisfiable formula with at most 120 n variables and 2 ^ 120 · n clauses of width at most 120 needs resolution refutations of exp (n / (960 · 36000²)) lines.

References

• A. Urquhart, Hard examples for resolution
• E. Ben-Sasson, A. Wigderson, Short proofs are narrow—resolution made simple
• S. Jukna, Boolean Function Complexity: Advances and Frontiers, Chapter 18

theorem Cslib.Logic.PL.Tseitin.edgeExpansion_mul_card_div_three_le_of_refutableInWidth {V : Type u_1} {D : Type u_2} [Fintype V] [DecidableEq V] [Fintype D] [DecidableEq D] (G : RotationMap V D) (hG : 0 < G.edgeExpansion) {χ : V → Bool} {w : ℕ} (h : (CNF.tseitinFormula G.edgeEnds χ).RefutableInWidth w) : G.edgeExpansion * ↑(Fintype.card V) / 3 ≤ ↑w

The width lower bound for Tseitin formulas on rotation maps Ben-Sasson and Wigderson: if h(G) > 0, every resolution refutation of a Tseitin formula on G has width at least h(G) |V| / 3.

theorem Cslib.Logic.PL.Tseitin.exp_edgeExpansion_le_of_refutableInSize {V : Type u_1} {D : Type u_2} [Fintype V] [DecidableEq V] [Fintype D] [DecidableEq D] (G : RotationMap V D) (hG : ↑(Fintype.card D) + 2 ≤ G.edgeExpansion * ↑(Fintype.card V) / 3) {χ : V → Bool} {s : ℕ} (hs : (CNF.tseitinFormula G.edgeEnds χ).RefutableInSize s) : Real.exp ((G.edgeExpansion * ↑(Fintype.card V) / 3 - ↑(Fintype.card D) - 2) ^ 2 / (8 * ↑(Fintype.card V) * ↑(Fintype.card D))) ≤ ↑s

The size lower bound for Tseitin formulas on rotation maps Ben-Sasson and Wigderson, Corollary 3.6: if |D| + 2 ≤ h(G) |V| / 3, every resolution refutation of a Tseitin formula on G has at least exp ((h(G) |V| / 3 - |D| - 2)² / (8 |V| |D|)) lines.

Hard formulas

theorem Cslib.Logic.PL.CNF.exists_forall_refutableInSize_exp_le (n : ℕ) : n ≥ 4392000 → ∃ m ≤ 120 * n, ∃ (φ : CNF (Fin m)), List.length φ ≤ 2 ^ 120 * n ∧ (∀ c ∈ φ, c.width ≤ 120) ∧ ¬φ.Satisfiable ∧ ∀ (s : ℕ), φ.RefutableInSize s → Real.exp (↑n / (960 * 36000 ^ 2)) ≤ ↑s

Unsatisfiable formulas with O(n) variables and clauses of constant width need resolution refutations of 2 ^ Ω(n) lines Urquhart Ben-Sasson and Wigderson Jukna, Chapter 18. For every n ≥ 4392000 there is an unsatisfiable formula with at most 120 n variables and at most 2 ^ 120 · n clauses, of width at most 120, whose resolution refutations all have at least exp (n / (960 · 36000²)) lines. It is the Tseitin formula, with a single charged vertex, of a 120-regular expander on n vertices (Cslib.RotationMap.expander), whose existence is proved non-constructively.