Near-optimal lower bounds on regular resolution refutations of Tseitin formulas for all constant-degree graphs (Q1983330): Difference between revisions

The article is well organized and written. It is worth noting that the introduction shows a good state-of-art in the subject, and the preliminaries section is very well written. The main result is the proof of the lower bound on the size of any regular resolution refutation of Tseitin formula \(T(G,c)\) base on a connected graph \(G=(V,E)\), in which they prove that that size is at least \(2^{\Omega(tw(G)/\log|V|)}\) where \(tw(G)\) is the treewidth of G; so, for constant-degree graphs, their lower bound is tight up to a logarithmic factor in the exponent. The proof which consists of two steps is well structured, mainly in Sections 3 and 4, and finally Section~5. In Section 3, the authors describe the transformation of a regular resolution refutation of an unsatisfiable Tseitin formula to a \textbf{1-BP} computing a satisfiable Tseitin formula. In Section 4 they prove the lower bound of an \textbf{1-NBP} computing a satisfiable Tseitin formula, and finally in Section 5 they prove the main result, that is, the lower bound for regular resolution refutation of Tseitin formula for all constant-degree graphs. Note. Page 13, at the end of paragraph 4 will be better to mention that the proof of Proposition 1.7 is in Section 4.2 for details. Just because the proof of the main result is extense. Finally, in Section 5, at the end of the proof of the central result there is a typo, instead of \(2^{\Omega(tw(G))/\log|V|}\) must be \(2^{\Omega(tw(G)/\log|V|)}\).