Characterizing Tseitin-Formulas with Short Regular Resolution Refutations

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^{\varOmega (tw(G))}/|V(G)|\), thus essentially matching the known \(2^{O(tw(G))}\text {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^{\varOmega (tw(G))}\) which yields our lower bound for regular resolution.

Authors

• Alexis de Colnet
• Stefan Mengel

Keywords

No keywords are indexed for this paper.