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 arbitrary graph G(V, E) any nondeterministic read-once branching program that computes a satisfiable Tseitin formula based on G has size at least (formula presented) for all (formula presented)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 also show an upper bound of (formula presented), where pw (G) is the pathwidth of G. 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 (formula presented).

Original languageEnglish
Title of host publicationComputer Science – Theory and Applications - 14th International Computer Science Symposium in Russia, CSR 2019, Proceedings
EditorsRené van Bevern, Gregory Kucherov
PublisherSpringer Nature
Pages143-155
Number of pages13
ISBN (Print)9783030199548
DOIs
StatePublished - 1 Jan 2019
Event14th International Computer Science Symposium in Russia, CSR 2019 - Novosibirsk, Russian Federation
Duration: 1 Jul 20195 Jul 2019

Publication series

NameLecture Notes in Computer Science
PublisherSPRINGER INTERNATIONAL PUBLISHING AG
Volume11532
ISSN (Print)0302-9743

Conference

Conference14th International Computer Science Symposium in Russia, CSR 2019
Country/TerritoryRussian Federation
CityNovosibirsk
Period1/07/195/07/19

    Research areas

  • Grid, Read-once branching program, Treewidth, Tseitin formula, WIDTH

    Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

ID: 49785149