Advertisement
Published in:
09-10-2020
On Tseitin Formulas, Read-Once Branching Programs and Treewidth
Published in: Theory of Computing Systems | Issue 3/2021
Log inActivate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
Abstract
We show that any nondeterministic read-once branching program that decides a satisfiable Tseitin formula based on an n × n grid graph has size at least 2Ω(n). Then using the Excluded Grid Theorem by Robertson and Seymour we show that for an arbitrary graph G(V, E) any nondeterministic read-once branching program that computes a satisfiable Tseitin formula based on G has size at least \(2^{\Omega (\text {tw}(G)^{\delta })}\) for all δ < 1/36, where tw(G) is the treewidth of G (for planar graphs and some other classes of graphs the statement holds for δ = 1). We apply the mentioned results to the analysis of the complexity of derivations in the proof system OBDD(∧,reordering) and show that any OBDD(∧,reordering)-refutation of an unsatisfiable Tseitin formula based on a graph G has size at least \(2^{\Omega (\text {tw}(G)^{\delta })}\). We also show an upper bound O(|E|2pw(G)) on the size of OBDD representations of a satisfiable Tseitin formula based on G and an upper bound \(O(|E||V| 2^{\text {pw}(G)}+|\text {TS}_{G,c}|^{2})\) on the size of OBDD(∧)-refutation of an unsatisifable Tseitin formula TSG, c, where pw(G) is the pathwidth of G.