Resolution lower bounds for Tseitin formulas

Tseitin formulas on graphs of good expansion are hard for resolution Urquhart. Ben-Sasson and Wigderson made this simple by going through width: on a connected multigraph G, every resolution refutation of a Tseitin formula has a line of width at least the expansion e(G) (Cslib.Multigraph.minBalancedCut), the least number of edges between a set of between a third and two thirds of the vertices and its complement (Cslib.Logic.PL.Tseitin.minBalancedCut_le_of_refutableInWidth). With the size–width tradeoff (Cslib.Logic.PL.CNF.exp_le_of_refutableInSize), a multigraph whose vertices have at most k ≤ e(G) - 2 edges other than self-loops, and with at most N edges, needs refutations of at least exp ((e(G) - k - 2)² / 8N) lines (Cslib.Logic.PL.Tseitin.exp_le_of_refutableInSize).

The width bound measures a clause c by the least number μ(c) of vertices whose constraints imply it (Cslib.Logic.PL.Tseitin.Implies).

• A clause of the formula is implied by the constraint of a single vertex, so μ ≤ 1 on it.
• The constraints implying the two premises of a resolution step together imply the resolvent, so μ is subadditive along resolution steps.
• The empty clause is implied by the constraints of all vertices only, since on a connected multigraph those of any other set are satisfiable (Cslib.Logic.PL.Tseitin.exists_forall_mem_parityOn_incidence_eq).

Hence the first line of a refutation with μ > |V| / 3 has μ ≤ 2 |V| / 3. If the constraints of S imply a clause c but those of S without any one vertex v do not, then c mentions every edge e between S and its complement: an assignment satisfying the constraints of S without v, and falsifying c, violates the constraint at v; flipping the value of e repairs it and changes no other constraint of S, and if c did not mention e it would still falsify c (Cslib.Logic.PL.Tseitin.exists_mem_of_mem_edgeCut). Taking S of size μ(c) for that line gives the bound.

Main definitions

• Cslib.Logic.PL.Tseitin.Implies: the constraints of a set of vertices imply a clause.

Main results

• Cslib.Logic.PL.Tseitin.exists_card_edgeCut_le_width: every refutation of a Tseitin formula on a connected multigraph has a line at least as wide as the number of edges leaving some set of more than a third and at most two thirds of the vertices.
• Cslib.Logic.PL.Tseitin.minBalancedCut_le_of_refutableInWidth: the width lower bound of Ben-Sasson and Wigderson, w ≥ e(G).
• Cslib.Logic.PL.Tseitin.exp_le_of_refutableInSize: the size lower bound, s ≥ exp ((e(G) - k - 2)² / 8N).

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

def Cslib.Logic.PL.Tseitin.Implies {V : Type u_1} {E : Type u_2} [DecidableEq V] [Fintype E] (ends : E → Sym2 V) (χ : V → Bool) (S : Finset V) (c : Clause E) : Prop

The constraints of the vertices in S imply the clause c: every assignment whose parity at each vertex of S is its charge satisfies c.

theorem Cslib.Logic.PL.Tseitin.Implies.mono {V : Type u_1} {E : Type u_2} [DecidableEq V] [Fintype E] {ends : E → Sym2 V} {χ : V → Bool} {S T : Finset V} {c : Clause E} (h : Implies ends χ S c) (hST : S ⊆ T) : Implies ends χ T c

More constraints imply more.

theorem Cslib.Logic.PL.Tseitin.Implies.resolvent {V : Type u_1} {E : Type u_2} [DecidableEq V] [Fintype E] [DecidableEq E] {ends : E → Sym2 V} {χ : V → Bool} {S₁ S₂ : Finset V} {c₁ c₂ : Clause E} (h₁ : Implies ends χ S₁ c₁) (h₂ : Implies ends χ S₂ c₂) (x : E) : Implies ends χ (S₁ ∪ S₂) (c₁.resolvent c₂ x)

The constraints implying the premises of a resolution step together imply the resolvent.

theorem Cslib.Logic.PL.Tseitin.exists_mem_of_mem_edgeCut {V : Type u_1} {E : Type u_2} [Fintype V] [DecidableEq V] [Fintype E] {ends : E → Sym2 V} {χ : V → Bool} {S : Finset V} {c : Clause E} (h : Implies ends χ S c) (hmin : ∀ v ∈ S, ¬Implies ends χ (S.erase v) c) {e : E} (he : e ∈ Multigraph.edgeCut ends S) : ∃ (b : Bool), (e, b) ∈ c

Minimal sets of constraints imply clauses mentioning their edge cut Ben-Sasson and Wigderson. If the constraints of S imply c, but those of S without any one of its vertices do not, then c mentions every edge between S and its complement.

theorem Cslib.Logic.PL.Tseitin.exists_card_edgeCut_le_width {V : Type u_1} {E : Type u_2} [Fintype V] [DecidableEq V] [Fintype E] [DecidableEq E] {ends : E → Sym2 V} {χ : V → Bool} [Nontrivial V] (hG : (Multigraph.toSimpleGraph ends).Connected) {ls : List (Clause E)} (h : (CNF.tseitinFormula ends χ).IsProof ls) (hnil : [] ∈ ls) : ∃ c ∈ ls, ∃ (S : Finset V), Fintype.card V < 3 * S.card ∧ 3 * S.card ≤ 2 * Fintype.card V ∧ (Multigraph.edgeCut ends S).card ≤ c.width

Refutations of Tseitin formulas have wide lines Ben-Sasson and Wigderson Jukna, Chapter 18. On a connected multigraph with at least two vertices, every resolution refutation of a Tseitin formula has a line at least as wide as the number of edges between some set S with |V| / 3 < |S| ≤ 2 |V| / 3 and its complement.

theorem Cslib.Logic.PL.Tseitin.minBalancedCut_le_of_refutableInWidth {V : Type u_1} {E : Type u_2} [Fintype V] [DecidableEq V] [Fintype E] [DecidableEq E] {ends : E → Sym2 V} {χ : V → Bool} (hG : (Multigraph.toSimpleGraph ends).Connected) {w : ℕ} (h : (CNF.tseitinFormula ends χ).RefutableInWidth w) : Multigraph.minBalancedCut ends ≤ w

The width lower bound for Tseitin formulas Ben-Sasson and Wigderson Jukna, Chapter 18: on a connected multigraph, every resolution refutation of a Tseitin formula has width at least the expansion e(G).

theorem Cslib.Logic.PL.Tseitin.exp_le_of_refutableInSize {V : Type u_1} {E : Type u_2} [Fintype V] [DecidableEq V] [Fintype E] [DecidableEq E] {ends : E → Sym2 V} {χ : V → Bool} (hG : (Multigraph.toSimpleGraph ends).Connected) {k N s : ℕ} (hk : ∀ (v : V), (Multigraph.incidence ends v).card ≤ k) (hN : Fintype.card E ≤ N) (hke : k + 2 ≤ Multigraph.minBalancedCut ends) (hs : (CNF.tseitinFormula ends χ).RefutableInSize s) : Real.exp ((↑(Multigraph.minBalancedCut ends) - ↑k - 2) ^ 2 / (8 * ↑N)) ≤ ↑s

The size lower bound for Tseitin formulas Ben-Sasson and Wigderson, Corollary 3.6 Jukna, Chapter 18. On a connected multigraph with at most N edges whose vertices have at most k edges other than self-loops, if k + 2 ≤ e(G), every resolution refutation of a Tseitin formula has at least exp ((e(G) - k - 2)² / 8N) lines.