Characterizing Tseitin-formulas with short regular resolution refutations
share
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^Ω(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 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^Ω(tw(G)) which yields our lower bound for regular resolution.
READ FULL TEXT