On Tseitin Formulas, Read-Once Branching Programs and Treewidth
- PDF / 504,996 Bytes
- 21 Pages / 439.642 x 666.49 pts Page_size
- 78 Downloads / 177 Views
On Tseitin Formulas, Read-Once Branching Programs and Treewidth Ludmila Glinskih1,2 · Dmitry Itsykson1
© Springer Science+Business Media, LLC, part of Springer Nature 2020
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(tw(G) ) 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(tw(G) ) . 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 |2pw(G) + |TSG,c |2 ) on the size of OBDD(∧)-refutation of an unsatisifable Tseitin formula TSG,c , where pw(G) is the pathwidth of G. Keywords Tseitin formulas · Read-once branching program · Treewidth · grid
This article belongs to the Topical Collection: Special Issue on Computer Science Symposium in Russia (2019) Guest Editor: Gregory Kucherov Dmitry Itsykson
[email protected] Ludmila Glinskih [email protected] 1
St. Petersburg Department of V.A. Steklov, Institute of Mathematics of the Russian Academy of Sciences, Fontanka 27, St. Petersburg, Russia
2
Present address: Department of Computer Science, Boston University, Boston, MA, USA
Theory of Computing Systems
1 Introduction This paper continues the study of representation of satisfiable Tseitin formulas by read-once branching programs. A Tseitin formula TSG,c [21] is defined for every undirected graph G(V , E) and a labeling function c : V → {0, 1}. We introduce a propositional variable for every edge of G. The Tseitin formula TSG,c represents a linear system over the field GF(2) that for every vertex v ∈ V states that the sum of all edges adjacent to v equals c(v). It is well known that a Tseitin formula is satisfiable if and only if the sum of values of the labeling function for all vertices in every connected component is even [22]. In 2017 Itsykson et al. [14] showed that any OBDD representing satisfiable Tseitin formulas based on d-regular expanders on n vertices has size at least 2(n) . Then Glinskih and Itsykson [10] extended this lower bound to nondeterministic read-once branching programs (1-NBP). In this paper we consider an n × n grid and study the complexity of representation of Tseitin formulas based on it by read-once branching programs. In Theorem 3.1 we prove that any 1-NBP computing a satisfiable Tseitin formula based on an n × n grid has size 2(n) . Although an n × n grid graph has some edge-expansion properties, we coul
Data Loading...
