Characterizing Tseitin-formulas with short regular resolution refutations

TL;DR

This paper characterizes when Tseitin-formulas admit short regular resolution proofs, showing that polynomial-length refutations occur if and only if the underlying graph's treewidth is logarithmic in the number of vertices.

Contribution

It establishes a tight connection between the treewidth of the underlying graph and the length of regular resolution refutations for Tseitin-formulas, providing new lower bounds.

Findings

Regular resolution refutations are polynomial if and only if treewidth is logarithmic.

Refutations require exponential size in treewidth for bounded degree graphs.

Lower bounds are proved via DNNF representations of satisfiable Tseitin-formulas.

Abstract

Tseitin-formulas are systems of parity constraints whose structure is described by a graph. These formulas have been studied extensively in proof complexity as hard instances in many proof systems. In this paper, we prove that a class of unsatisfiable Tseitin-formulas of bounded degree has regular resolution refutations of polynomial length if and only if the treewidth of all underlying graphs $G$ for that class is in $O(\log|V(G)|)$. To do so, we show that any regular resolution refutation of an unsatisfiable Tseitin-formula with graph $G$ of bounded degree has length $2^{\Omega(tw(G))}/|V(G)|$, thus essentially matching the known $2^{O(tw(G))}poly(|V(G)|)$ upper bound up. Our proof first connects the length of regular resolution refutations of unsatisfiable Tseitin-formulas to the size of representations of \textit{satisfiable} Tseitin-formulas in decomposable negation normal form (DNNF). Then we prove that for every graph $G$ of bounded degree, every DNNF-representation of every satisfiable Tseitin-formula with graph $G$ must have size $2^{\Omega(tw(G))}$ which yields our lower bound for regular resolution.