ECCC-Report TR19-020https://eccc.weizmann.ac.il/report/2019/020Comments and Revisions published for TR19-020en-usMon, 25 Mar 2019 13:46:17 +0200
Revision 1
| On Tseitin formulas, read-once branching programs and treewidth |
Ludmila Glinskih,
Dmitry Itsykson
https://eccc.weizmann.ac.il/report/2019/020#revision1We show that any nondeterministic read-once branching program that computes a satisfiable Tseitin formula based on an $n\times n$ grid graph has size at least $2^{\Omega(n)}$. Then using the Excluded Grid Theorem by Robertson and Seymour we show that for 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(tw(G)^\delta)}$ for all $\delta <1/36$, where $tw(G)$ is the treewidth of $G$ (for planar graphs and some other classes of graphs the statement holds for $\delta=1$). We also show an upper bound $O(|E| 2^{pw(G)})$, where $pw(G)$ is the pathwidth of $G$.
We apply the mentioned results in the analysis of the complexity of derivation in the proof system $OBDD(\land, reordering)$ and show that any $OBDD(\land, reordering)$-refutation of an unsatisfiable Tseitin formula based on a graph $G$ has size at least $2^{\Omega(tw(G)^\delta)}$.Mon, 25 Mar 2019 13:46:17 +0200https://eccc.weizmann.ac.il/report/2019/020#revision1
Paper TR19-020
| On Tseitin formulas, read-once branching programs and treewidth |
Ludmila Glinskih,
Dmitry Itsykson
https://eccc.weizmann.ac.il/report/2019/020We show that any nondeterministic read-once branching program that computes a satisfiable Tseitin formula based on an $n\times n$ grid graph has size at least $2^{\Omega(n)}$. Then using the Excluded Grid Theorem by Robertson and Seymour we show that for 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(tw(G)^\delta)}$ for all $\delta <1/36$, where $tw(G)$ is the treewidth of $G$ (for planar graphs and some other classes of graphs the statement holds for $\delta=1$). We also show an upper bound $O(|E| 2^{pw(G)})$, where $pw(G)$ is the pathwidth of $G$.
We apply the mentioned results in the analysis of the complexity of derivation in the proof system $OBDD(\land, reordering)$ and show that any $OBDD(\land, reordering)$-refutation of an unsatisfiable Tseitin formula based on a graph $G$ has size at least $2^{\Omega(tw(G)^\delta)}$.Tue, 19 Feb 2019 20:23:06 +0200https://eccc.weizmann.ac.il/report/2019/020