2021/03/17 by Alexis de Colnet, Stefan Mengel, de Colnet, Alexis +1
Computer Science · #Advanced Graph Theory Research #Complexity and Algorithms in Graphs #Computational Complexity (cs.CC) #FOS: Computer and information sciences #semigroups and automata theory
paper · doi:10.48550/arxiv.2103.09609
openalex publication_date 2021/03/17 · openalex created_date 2022/07/25 · openalex updated_date 2026/07/28
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 2O(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.