In this talk, we will discuss some bounds for regular resolution refutations of unsatisfiable Tseitin formulas. These bounds estimate the size of a proof via treewidth of the underlying graph.

Reducing the lower bounds for unsatisfiable formulas to the lower bounds for the satisfiable case and obtaining such bounds, we got the lower bound exp(Ω(tw(G) / log(V))) in [1].
Recently, de Colnet and Mengel [2] got the lower bound exp(Ω(tw(G) / Δ(G))) (up to polynomial factor) using the similar reduction concept. There is a known upper bound exp(O(tw(G) * Δ(G))), so the bound is tight for constant-degree graphs.

However, the question for all graphs is still open. Also, there are two lower bounds, and while the latter bound is stronger for graphs of small degrees, the former is better for graphs of large degrees.

Now we've got the new lower bound exp(Ω(tw(G))) (up to polynomial factor). It is stronger than both of the previous bounds and bring us closer to the tight bound for all Tseitin formulas.

[1] Itsykson D., Riazanov A., Sagunov D., Smirnov P. Near-Optimal Lower Bounds on Regular Resolution Refutations of Tseitin Formulas for All Constant-Degree Graphs. Comput. Complex. 30, 13 (2021).
[2] de Colnet A., Mengel S. (2021) Characterizing Tseitin-Formulas with Short Regular Resolution Refutations. In Proceedings of SAT 2021.