14:00
15:00

Title: 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 a recent paper, my student Alexis de Colnet and I showed 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 showed 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))}(|V(G)|) upper bound. In this talk, I will present some background and give an idea of how this result is shown.

178