Correction to: Near-Optimal Lower Bounds on Regular Resolution Refutations of Tseitin Formulas for All Constant-Degree Graphs

This paper is motivated by seeking the exact complexity of resolution refutation of Tseitin formulas. We prove that the size of any regular resolution refutation of a Tseitin formula T(G, c) based on a connected graph G =(V, E) is at least 2^Ω( tw(G)/ log |V|) , where tw(G) denotes the treewidth of a graph G . For constant-degree graphs, there is a known upper bound 2^𝒪( tw(G)) poly(|V|) (Alekhnovich Razborov Comput. Compl. 2011; Galesi, Talebanfard Torán ACM Trans. Comput. Theory 2020), so our lower bound is tight up to a logarithmic factor in the exponent. Our proof consists of two steps. First, we show that any regular resolution refutation of an unsatisfiable Tseitin formula T(G, c) of size S can be converted to a read-once branching program computing a satisfiable Tseitin formula T(G,c') of size S^𝒪( log |V|) and this bound is tight. Second, we give the exact characterization of the nondeterministic read-once branching program (1-NBP) complexity of satisfiable Tseitin formulas in terms of structural properties of underlying graphs. Namely, we introduce a new graph measure, the component width (compw) and show that the size of a minimal 1-NBP computing a satisfiable Tseitin formula T(G,c') based on a graph G = (V, E) equals 2^compw(G) up to a polynomial factor. Then we show that Ω( tw(G)) ≤ compw(G) ≤𝒪( tw(G) log(|V|)) and both of these bounds are tight. The lower bound improves the recent result by Glinskih Itsykson (Theory Comput. Syst. 2021).